From 49bf401fa3857b3c4f3faf9f338f1c62f4a771a3 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Tue, 3 Dec 2024 14:19:28 -0800 Subject: [PATCH] More renames of syl5bb to bitrid (#4464) This is the next 150 or so occurences in set.mm. --- set.mm | 310 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 155 insertions(+), 155 deletions(-) diff --git a/set.mm b/set.mm index 2eeba18298..fefabef76f 100644 --- a/set.mm +++ b/set.mm @@ -44969,7 +44969,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). certain conditions. (Contributed by NM, 27-Mar-2007.) $) opthpr $p |- ( A =/= D -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) ) $= - ( cpr wceq wa wo wne preq12b idd wn wi df-ne pm2.21 sylbi impd orc syl5bb + ( cpr wceq wa wo wne preq12b idd wn wi df-ne pm2.21 sylbi impd orc bitrid jaod impbid1 ) ABICDIJACJBDJKZADJZBCJZKZLZADMZUFABCDEFGHNUKUJUFUKUFUFUIUK UFOUKUGUHUFUKUGPUGUHUFQZQADRUGULSTUAUDUFUIUBUEUC $. $} @@ -45060,7 +45060,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). 13-Jun-2022.) (Revised by AV, 16-Aug-2024.) $) preqsnd $p |- ( ph -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) ) $= ( cvv wcel cpr csn wceq wa wb adantl wn c0 wi syl simpl dfsn2 wo preq12bg - eqeq2i oridm bitrdi syl5bb syl22anc snprc biimpi adantr wne prnzg syl5com + eqeq2i oridm bitrdi bitrid syl22anc snprc biimpi adantr wne prnzg syl5com eqeq2d eqneqall sylbid eleq1 eqcoms notbid pm2.24 elex syl11 syl6bi com13 impcom impd impbid pm2.61ian ) DIJZABCKZDLZMZBDMZCDMZNZOZVKANBEJZCFJZVKVK VRAVSVKGPAVTVKHPVKAUAZWAVNVLDDKZMZVSVTNVKVKNNZVQVMWBVLDUBUEWDWCVQVQUCVQBC @@ -45366,7 +45366,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). csbopg $p |- ( A e. V -> [_ A / x ]_ <. C , D >. = <. [_ A / x ]_ C , [_ A / x ]_ D >. ) $= ( wcel cvv wa csn cpr c0 cif csb cop wsbc csbif sbcan sbcel1g csbprg dfopif - anbi12d syl5bb csbsng preq12d csbconstg ifbieq12d eqtrid csbeq2i 3eqtr4g + anbi12d bitrid csbsng preq12d csbconstg ifbieq12d eqtrid csbeq2i 3eqtr4g eqtrd ) BEFZABCGFZDGFZHZCIZCDJZJZKLZMZABCMZGFZABDMZGFZHZUTIZUTVBJZJZKLZABCD NZMUTVBNUKUSUNABOZABUQMZABKMZLVHUNABUQKPUKVJVDVKVLVGKVJULABOZUMABOZHUKVDULU MABQUKVMVAVNVCABCGERABDGERUAUBUKVKABUOMZABUPMZJVGAUOUPBESUKVOVEVPVFABCEUCAC @@ -45396,7 +45396,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). (Revised by Mario Carneiro, 23-Apr-2015.) $) ralunsn $p |- ( B e. C -> ( A. x e. ( A u. { B } ) ph <-> ( A. x e. A ph /\ ps ) ) ) $= - ( csn cun wral wa wcel ralunb ralsng anbi2d syl5bb ) ACDEHZIJACDJZACQJZKE + ( csn cun wral wa wcel ralunb ralsng anbi2d bitrid ) ACDEHZIJACDJZACQJZKE FLZRBKACDQMTSBRABCEFGNOP $. $} @@ -45697,7 +45697,7 @@ there is another (different) element of the class ` V ` which is an ~ unipr to prove it from ~ uniprg . (Revised by BJ, 1-Sep-2024.) $) uniprg $p |- ( ( A e. V /\ B e. W ) -> U. { A , B } = ( A u. B ) ) $= ( vx vy wcel wa wel cv cpr wex cab wo cuni wceq bitri wb clel3g bicomd - cun vex elpr anbi2i ancom andir exbii adantr adantl orbi12d syl5bb abbidv + cun vex elpr anbi2i ancom andir exbii adantr adantl orbi12d bitrid abbidv 19.43 df-uni df-un 3eqtr4g ) ACGZBDGZHZEFIZFJZABKZGZHZFLZEMEJZAGZVFBGZNZE MVBOABUAUSVEVIEVEVAAPZUTHZFLZVABPZUTHZFLZNZUSVIVEVKVNNZFLVPVDVQFVDUTVJVMN ZHZVQVCVRUTVAABFUBUCUDVSVRUTHVQUTVRUEVJVMUTUFQQUGVKVNFUMQUSVLVGVOVHUQVLVG @@ -45832,7 +45832,7 @@ there is another (different) element of the class ` V ` which is an (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 22-Aug-2018.) $) csbuni $p |- [_ A / x ]_ U. B = U. [_ A / x ]_ B $= - ( vz vy cvv wcel cuni csb wceq wel cv wa wex wsbc syl5bb df-uni c0 csbprc + ( vz vy cvv wcel cuni csb wceq wel cv wa wex wsbc bitrid df-uni c0 csbprc cab csbab sbcex2 anbi1d sbcel2 anbi2i bitrdi exbidv abbidv eqtrid csbeq2i sbcan sbcg 3eqtr4g wn unieqd uni0 eqtr2di eqtrd pm2.61i ) BFGZABCHZIZABCI ZHZJUTABDEKZELZCGZMZENZDTZIZVEVFVCGZMZENZDTZVBVDUTVKVIABOZDTVOVIADBUAUTVP @@ -46231,7 +46231,7 @@ either the empty set or a singleton ( ~ uniintsn ). (Contributed by NM, 27-Apr-2008.) (Proof shortened by BJ, 1-Sep-2024.) $) intprg $p |- ( ( A e. V /\ B e. W ) -> |^| { A , B } = ( A i^i B ) ) $= ( vx vy wcel wa cv cpr cint cin wb wal wceq wel wi vex elint clel4g bitri - wo elpr imbi1i jaob albii 19.26 3bitri elin bitr2id syl5bb alrimiv dfcleq + wo elpr imbi1i jaob albii 19.26 3bitri elin bitr2id bitrid alrimiv dfcleq bi2anan9 sylibr ) ACGZBDGZHZEIZABJZKZGZUSABLZGZMZENVAVCOURVEEVBFIZAOZEFPZ QZFNZVFBOZVHQZFNZHZURVDVBVFUTGZVHQZFNVIVLHZFNVNFUSUTERSVPVQFVPVGVKUBZVHQV QVOVRVHVFABFRUCUDVGVHVKUEUAUFVIVLFUGUHVDUSAGZUSBGZHURVNUSABUIUPVSVJUQVTVM @@ -46709,7 +46709,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and ( vw vz wcel wral cv cab wceq wrex wi wal df-ral wb eqeq1 albii bitr4i ciin cint eleq2 biimprcd alrimiv eqid imbi12d mpii impbid2 imim2i pm5.74d spcgv alimi albi syl sylbi alcom r19.23v vex rexbidv elab imbi1i 3bitr3ri - 19.21v bitrdi syl5bb abbidv df-iin df-int 3eqtr4g ) DEHZACIZFJZDHZACIZFKG + 19.21v bitrdi bitrid abbidv df-iin df-int 3eqtr4g ) DEHZACIZFJZDHZACIZFKG JZBJZDLZACMZBKZHZVMVPHZNZGOZFKACDUAVTUBVLVOWDFVOAJCHZVNNZAOZVLWDVNACPVLWG WEVPDLZWBNZGOZNZAOZWDVLWEVKNZAOZWGWLQZVKACPWNWFWKQZAOWOWMWPAWMWEVNWJVKVNW JQWEVKVNWJVNWIGWHWBVNVPDVMUCZUDUEVKWJDDLZVNDUFWIWRVNNGDEWHWHWRWBVNVPDDRWQ @@ -47268,7 +47268,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and $( A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.) $) iunxsng $p |- ( A e. V -> U_ x e. { A } B = C ) $= - ( vy wcel csn ciun cv wrex eliun wceq eleq2d rexsng syl5bb eqrdv ) BEHZGA + ( vy wcel csn ciun cv wrex eliun wceq eleq2d rexsng bitrid eqrdv ) BEHZGA BIZCJZDGKZUAHUBCHZATLSUBDHZAUBTCMUCUDABEAKBNCDUBFOPQR $. $} @@ -47292,7 +47292,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and Arnoux, 2-May-2020.) Avoid ~ ax-13 . (Revised by Gino Giotto, 19-May-2023.) $) iunxsngf $p |- ( A e. V -> U_ x e. { A } B = C ) $= - ( vy wcel csn ciun cv wrex eliun nfcri wceq eleq2d rexsngf syl5bb eqrdv ) + ( vy wcel csn ciun cv wrex eliun nfcri wceq eleq2d rexsngf bitrid eqrdv ) BEIZHABJZCKZDHLZUCIUDCIZAUBMUAUDDIZAUDUBCNUEUFABEAHDFOALBPCDUDGQRST $. $( $j usage 'iunxsngf' avoids 'ax-13'; $) $} @@ -47426,7 +47426,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and $( Relationship for power class and union. (Contributed by NM, 18-Jul-2006.) $) elpwuni $p |- ( B e. A -> ( A C_ ~P B <-> U. A = B ) ) $= - ( cpw wss cuni wcel wceq sspwuni unissel expcom eqimss impbid1 syl5bb ) ABC + ( cpw wss cuni wcel wceq sspwuni unissel expcom eqimss impbid1 bitrid ) ABC DAEZBDZBAFZNBGZABHPOQOPQABIJNBKLM $. ${ @@ -47898,7 +47898,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and impr syl anbi2d ralunb ralbii nfcv nfcsb1v nfin nfeq1 nfor nfralw equequ2 nfv csbhypf ineq2d cbvralvw equequ1 csbeq1a ineq1d ralbidv bitr3id r19.26 cbvralw 3bitr3i disjor anbi1i 3bitr4g equcom bitrdi eqtrdi ralcom disjors - incom syl5bb anbi1d anbi2ci anbi12d df-3an anandir ) CDJKLZHIMZAHNZEUAZAI + incom bitrid anbi1d anbi2ci anbi12d df-3an anandir ) CDJKLZHIMZAHNZEUAZAI NZEUAZJZKLZOZICDUDZPZHCPZXEHDPZQZACEUBZEFJZKLZBDPACPZQZADEUBZXLQZQZAXDEUB ZXIXNXLUEZWOXFXMXGXOWOABMZXKOZBCPZACPZXTBDPZACPZQZYBXLQXFXMWOYDXLYBWOXTXK ABCDWOANZCUCZBNZDUCZQQZXKXTYJXSUFZXKXTUGWOYGYIYKWOYGQZXSYIYLYFDUCZUFXSYIU @@ -48403,7 +48403,7 @@ proper class (see for example ~ iprc ). (Contributed by NM, 13-Dec-2005.) $) sbcbr12g $p |- ( A e. V -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R [_ A / x ]_ C ) ) $= - ( wbr wsbc csb wcel sbcbr123 csbconstg breqd syl5bb ) CDEGABHABCIZABDIZAB + ( wbr wsbc csb wcel sbcbr123 csbconstg breqd bitrid ) CDEGABHABCIZABDIZAB EIZGBFJZOPEGABCDEKRQEOPABEFLMN $. $} @@ -51377,7 +51377,7 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with opthneg $p |- ( ( A e. V /\ B e. W ) -> ( <. A , B >. =/= <. C , D >. <-> ( A =/= C \/ B =/= D ) ) ) $= ( cop wne wceq wn wcel wa wo df-ne opthg notbid ianor orbi12i bitr4i bitrdi - syl5bb ) ABGZCDGZHUBUCIZJZAEKBFKLZACHZBDHZMZUBUCNUFUEACIZBDIZLZJZUIUFUDULAB + bitrid ) ABGZCDGZHUBUCIZJZAEKBFKLZACHZBDHZMZUBUCNUFUEACIZBDIZLZJZUIUFUDULAB CDEFOPUMUJJZUKJZMUIUJUKQUGUNUHUOACNBDNRSTUA $. ${ @@ -51416,7 +51416,7 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with -> ( <. A , B , C >. = <. D , E , F >. <-> ( A = D /\ B = E /\ C = F ) ) ) $= ( cotp wceq cop wcel w3a df-ot eqeq12i wb wa cvv opthg anbi1d bitr4di 3impa - opex mpan df-3an sylan9bbr syl5bb ) ABCJZDFGJZKABLZCLZDFLZGLZKZAEMZBHMZCIMZ + opex mpan df-3an sylan9bbr bitrid ) ABCJZDFGJZKABLZCLZDFLZGLZKZAEMZBHMZCIMZ NADKZBFKZCGKZNZUIULUJUNABCODFGOPUPUQURUOVBQURUOUKUMKZVARZUPUQRZVBUKSMURUOVD QABUDUKCUMGSITUEVEVDUSUTRZVARVBVEVCVFVAABDFEHTUAUSUTVAUFUBUGUCUH $. @@ -51531,7 +51531,7 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with copsex2g $p |- ( ( A e. V /\ B e. W ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) ) $= ( cop cv wceq wa wex wcel eqcom vex opth bitri anbi1i 2exbii id cgsex2g - syl5bb ) EFJZCKZDKZJZLZAMZDNCNUFELUGFLMZAMZDNCNEGOFHOMBUJULCDUIUKAUIUHUEL + bitrid ) EFJZCKZDKZJZLZAMZDNCNUFELUGFLMZAMZDNCNEGOFHOMBUJULCDUIUKAUIUHUEL UKUEUHPUFUGEFCQDQRSTUAABUKCDEFGHUKUBIUCUD $. $( $j usage 'copsex2g' avoids 'ax-10' 'ax-11' 'ax-12'; $) @@ -51633,7 +51633,7 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with opeqsng $p |- ( ( A e. V /\ B e. W ) -> ( <. A , B >. = { C } <-> ( A = B /\ C = { A } ) ) ) $= ( wcel wa cop csn wceq cpr dfopg eqeq1d wb snex prex a1i eqcom simpr bitrdi - preqsn simpl preqsnd eqid impbii bitri syl5bb anbi1d wi dfsn2 preq2 eqtr2id + preqsn simpl preqsnd eqid impbii bitri bitrid anbi1d wi dfsn2 preq2 eqtr2id jctl pm5.32d bitrd 3bitrd ) ADFZBEFZGZABHZCIZJAIZABKZKZVAJZVBVCJZVCCJZGZABJ ZCVBJZGZUSUTVDVAABDELMVEVHNUSVBVCCAOABPUAQUSVHVIVGGVKUSVFVIVGVFVCVBJZUSVIVB VCRUSVLAAJZBAJZGZVIUSABADEUQURUBUQURSUCVOVNVIVOVNVMVNSVNVMAUDUMUEBARUFTUGUH @@ -51673,7 +51673,7 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with snopeqop $p |- ( { <. A , B >. } = <. C , D >. <-> ( A = B /\ C = D /\ C = { A } ) ) $= ( cvv wcel cop csn wceq wb wa a1i wn wi c0 eqeq2d syl6bi eleq1 w3a ancoms - eqcom opeqsng syl5bb opeqsn anbi2d 3anan12 bicomi 3bitrd opprc2 opex snnz + eqcom opeqsng bitrid opeqsn anbi2d 3anan12 bicomi 3bitrd opprc2 opex snnz eqneqall adantr notbid eqcoms pm2.21 impd 3ad2ant2 com12 impbid pm2.61ian wne mpi opprc1 snex pm2.24i 3ad2ant3 pm2.61i ) CGHZABIZJZCDIZKZABKZCDKZCA JZKZUAZLZDGHZVKWAWBVKMZVOVQVLCJKZMZVQVPVSMZMZVTVOVNVMKZWCWEVMVNUCVKWBWHWE @@ -51981,7 +51981,7 @@ necessary if all involved classes exist as sets (i.e. are not proper Arnoux, 23-Sep-2023.) $) brsnop $p |- ( ( A e. V /\ B e. W ) -> ( X { <. A , B >. } Y <-> ( X = A /\ Y = B ) ) ) $= - ( cop csn wbr wcel wa wceq df-br opex elsn opthg2 syl5bb ) EFABGZHZIEFGZSJZ + ( cop csn wbr wcel wa wceq df-br opex elsn opthg2 bitrid ) EFABGZHZIEFGZSJZ ACJBDJKZEALFBLKZEFSMUATRLUBUCTREFNOEFABCDPQQ $. @@ -52088,7 +52088,7 @@ necessary if all involved classes exist as sets (i.e. are not proper /\ ( A e. V /\ B e. W ) ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) ) $= ( cop copab wcel cv wceq wa wex wb wi wal w3a elopab anim12 2alimi sylbir - 19.26-2 bitr syl6 copsex2t stoic3 syl5bb ) FGJZADEKLUKDMZEMZJNAOEPDPZULFN + 19.26-2 bitr syl6 copsex2t stoic3 bitrid ) FGJZADEKLUKDMZEMZJNAOEPDPZULFN ZABQZRZESDSZUMGNZBCQZRZESDSZFHLGILOZTCADEUKUAURVBUOUSOZACQZRZESDSZVCUNCQU RVBOUQVAOZESDSVGUQVADEUEVHVFDEVHVDUPUTOVEUOUPUSUTUBABCUFUGUCUDACDEFGHIUHU IUJ $. @@ -52101,7 +52101,7 @@ necessary if all involved classes exist as sets (i.e. are not proper Mario Carneiro, 19-Dec-2013.) $) opelopabga $p |- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ps ) ) $= - ( cop copab wcel cv wceq wa wex elopab copsex2g syl5bb ) EFJZACDKLTCMDMJN + ( cop copab wcel cv wceq wa wex elopab copsex2g bitrid ) EFJZACDKLTCMDMJN AODPCPEGLFHLOBACDTQABCDEFGHIRS $. ${ @@ -52109,7 +52109,7 @@ necessary if all involved classes exist as sets (i.e. are not proper $( The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) $) brabga $p |- ( ( A e. V /\ B e. W ) -> ( A R B <-> ps ) ) $= - ( wbr cop copab wcel wa df-br eleq2i bitri opelopabga syl5bb ) EFGLZEFM + ( wbr cop copab wcel wa df-br eleq2i bitri opelopabga bitrid ) EFGLZEFM ZACDNZOZEHOFIOPBUBUCGOUEEFGQGUDUCKRSABCDEFHIJTUA $. $} @@ -52174,7 +52174,7 @@ necessary if all involved classes exist as sets (i.e. are not proper opelopabgf $p |- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) ) $= ( cop copab wcel wsbc wa opelopabsb sbciegf nfcv cv wceq sbcbidv sylan9bb - nfsbcw syl5bb ) FGNADEOPAEGQZDFQZFHPZGIPZRCADEFGSUJUIBEGQZUKCUHULDFHBDEGD + nfsbcw bitrid ) FGNADEOPAEGQZDFQZFHPZGIPZRCADEFGSUJUIBEGQZUKCUHULDFHBDEGD GUAJUFDUBFUCABEGLUDTBCEGIKMTUEUG $. $} @@ -52368,7 +52368,7 @@ necessary if all involved classes exist as sets (i.e. are not proper 26-Sep-2019.) $) csbmpt12 $p |- ( A e. V -> [_ A / x ]_ ( y e. Y |-> Z ) = ( y e. [_ A / x ]_ Y |-> [_ A / x ]_ Z ) ) $= - ( vz wcel cv wceq copab csb cmpt wsbc csbopab sbcan sbcel12 syl5bb df-mpt + ( vz wcel cv wceq copab csb cmpt wsbc csbopab sbcan sbcel12 bitrid df-mpt wa csbconstg eleq1d sbceq2g anbi12d opabbidv eqtrid csbeq2i 3eqtr4g ) CDH ZACBIZEHZGIZFJZTZBGKZLZUJACELZHZULACFLZJZTZBGKZACBEFMZLBUQUSMUIUPUNACNZBG KVBUNABGCOUIVDVABGVDUKACNZUMACNZTUIVAUKUMACPUIVEURVFUTVEACUJLZUQHUIURACUJ @@ -52419,7 +52419,7 @@ necessary if all involved classes exist as sets (i.e. are not proper Alexander van der Vekens, 30-Oct-2017.) $) rbropapd $p |- ( ph -> ( ( F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ch ) ) ) ) $= - ( wcel wa wbr wb cop cv wceq copab df-br eleq2d syl5bb anbi12d opelopabga + ( wcel wa wbr wb cop cv wceq copab df-br eleq2d bitrid anbi12d opelopabga breq12 sylan9bb ex ) AFINDJNOZFDGPZFDHPZCOZQAUKFDRZESZKSZHPZBOZEKUAZNZUJU MUKUNGNAUTFDGUBAGUSUNLUCUDURUMEKFDIJUOFTUPDTOUQULBCUOFUPDHUGMUEUFUHUI $. @@ -52602,7 +52602,7 @@ necessary if all involved classes exist as sets (i.e. are not proper dfid3 $p |- _I = { <. x , y >. | x = y } $= ( vz vw weq copab cv cop wa wex cab wb exbii opeq2 eqeq2d equequ2 anbi12d wceq nfnae nfcvd cid df-id wal equcom anbi1ci equsexvw equid biantru nfe1 - 3bitri 19.9 bitr4i sps drex1 drex2 syl5bb wn nfcvf2 nfopd nfeqd nfand a1i + 3bitri 19.9 bitr4i sps drex1 drex2 bitrid wn nfcvf2 nfopd nfeqd nfand a1i wi cbvexd exbid pm2.61i abbii df-opab 3eqtr4i eqtri ) UAACEZACFZABEZABFZA CUBDGZAGZCGZHZRZVKIZCJZAJZDKVOVPBGZHZRZVMIZBJZAJZDKVLVNWBWHDVMAUCZWBWHLWB VOVPVPHZRZAAEZIZAJZAJZWIWHWBWNWOWAWMAWACAEZVSIZCJWKWMVTWQCVKWPVSACUDUEMVS @@ -53362,7 +53362,7 @@ dummy variables (but note that their equivalence uses ~ ax-sep ). (Revised by Mario Carneiro, 22-Jun-2015.) $) frirr $p |- ( ( R Fr A /\ B e. A ) -> -. B R B ) $= ( vx vy vz wfr wcel wa cv wbr csn crab c0 wceq adantl wral breq1 notbid - wn wrex wss wne simpl snssi snnzg snex frc syl3anc rabeq0w ralbidv syl5bb + wn wrex wss wne simpl snssi snnzg snex frc syl3anc rabeq0w ralbidv bitrid wb breq2 rexsng ralsng bitrd mpbid ) ACGZBAHZIZDJZEJZCKZDBLZMNOZEVEUAZBBC KZTZVAUSVEAUBZVENUCZVGUSUTUDUTVJUSBAUEPUTVKUSBAUFPEDAVECBUGUHUIUTVGVIUMUS UTVGFJZBCKZTZFVEQZVIVFVOEBAVFVLVCCKZTZFVEQVCBOZVOVDVPDFVEVBVLVCCRUJVRVQVN @@ -53567,7 +53567,7 @@ dummy variables (but note that their equivalence uses ~ ax-sep ). E! x e. B A. y e. B -. y R x ) $= ( vz vw wa c0 cv wbr wn wral wrex wcel wi breq1 syl5bi sylc ad2antrr wrmo wwe wse wss wne wreu wex n0 crab rabeq0 weq notbid cbvralvw breq2 ralbidv - wceq syl5bb rspcev ex ad2antll cvv wfr simprl simplr sess2 simprr syl2anc + wceq bitrid rspcev ex ad2antll cvv wfr simprl simplr sess2 simprr syl2anc seex wefr ssrab2 sstrid fri expr syl21anc rexrab wor weso soss simpr sotr ralrab syl13anc ancomsd expdimp an32s con3d idd ralimdva expimpd reximdva jad syld pm2.61dne exlimdv impr somo syl reu5 sylanbrc ) CEUBZCEUCZHZDCUD @@ -54125,7 +54125,7 @@ of the restricted converse (see ~ cnvrescnv ). (Contributed by NM, ( x e. A /\ C e. B ) ) $= ( vy vz cv cop csn cxp ciun wcel wrex wa wceq eleq2d anbi12d bitri 3bitri wex cab wsb csb df-iun eleq2i opex nfv nfs1v nfcv nfcsb1v nfxp nfcri nfan - df-rex sbequ12 csbeq1a xpeq12d cbvexv1 anbi2d exbidv syl5bb opelxp anbi2i + df-rex sbequ12 csbeq1a xpeq12d cbvexv1 anbi2d exbidv bitrid opelxp anbi2i sneq eleq1 elab an12 velsn equcom anbi1i sbequ12r equcoms eqcomd equsexvw exbii ) AGZDHZABVPIZCJZKZLVQEGZVSLZABMZEUAZLVPBLZAFUBZVQFGZIZAWGCUCZJZLZN ZFTZWEDCLZNZVTWDVQAEBVSUDUEWCWMEVQVPDUFWCWFWAWJLZNZFTZWAVQOZWMWCWEWBNZATW @@ -54295,7 +54295,7 @@ of the restricted converse (see ~ cnvrescnv ). (Contributed by NM, posn $p |- ( Rel R -> ( R Po { A } <-> -. A R A ) ) $= ( vx vy vz cvv wpo wbr wn wb wa c0 wceq cv wi breq2 anbi2d ralsng ralbidv wral wrel wcel csn po0 snprc poeq2 mpbiri adantl brrelex1 stoic1a 2thd ex - sylbi df-po imbi12d simpl syl5ib bicomd bitrd breq12 anidms notbid syl5bb + sylbi df-po imbi12d simpl syl5ib bicomd bitrd breq12 anidms notbid bitrid biantrud pm2.61d2 ) BUAZAFUBZAUCZBGZAABHZIZJZVFVGIZVLVFVMKVIVKVMVIVFVMVIL BGZBUDVMVHLMVIVNJAUEVHLBUFUMUGUHVFVJVGAABUIUJUKULVICNZVOBHZIZVODNZBHZVREN ZBHZKZVOVTBHZOZKZEVHTZDVHTZCVHTZVGVKCDEVHBUNVGWHVQCVHTVKVGWGVQCVHVGWGVQVS @@ -54307,7 +54307,7 @@ of the restricted converse (see ~ cnvrescnv ). (Contributed by NM, 28-Dec-2014.) $) sosn $p |- ( Rel R -> ( R Or { A } <-> -. A R A ) ) $= ( vx vy csn wor wpo wrel wbr wn cv weq wral wcel wa elsni eqcomd sylan9eq - w3o 3mix2d rgen2 df-so mpbiran2 posn syl5bb ) AEZBFZUFBGZBHAABIJUGUHCKZDK + w3o 3mix2d rgen2 df-so mpbiran2 posn bitrid ) AEZBFZUFBGZBHAABIJUGUHCKZDK ZBIZCDLZUJUIBIZSZDUFMCUFMUNCDUFUFUIUFNZUJUFNZOULUKUMUOUPUIAUJUIAPUPUJAUJA PQRTUACDUFBUBUCABUDUE $. @@ -54317,7 +54317,7 @@ of the restricted converse (see ~ cnvrescnv ). (Contributed by NM, ( vz vy vx cvv wfr wbr wn wa c0 wceq adantl cv wral wrex wne wi wal imp wrel wcel csn wb snprc fr0 freq2 mpbiri sylbi brrelex1 stoic1a 2thd df-fr ex wss wo sssn neor sylbb eqimss snnzg neeq1 syl5ibrcom jca imbi1d albidv - impbida snex raleq rexeqbi1dv ceqsalv bitrdi syl5bb notbid ralbidv rexsng + impbida snex raleq rexeqbi1dv ceqsalv bitrdi bitrid notbid ralbidv rexsng breq2 breq1 ralsng 3bitrd pm2.61d2 ) BUAZAFUBZAUCZBGZAABHZIZUDZWBWCIZWHWB WIJWEWGWIWEWBWIWDKLZWEAUEWJWEKBGBUFWDKBUGUHUIMWBWFWCAABUJUKULUNWCWECNZDNZ BHZIZCWDOZDWDPZWKABHZIZCWDOZWGWEENZWDUOZWTKQZJZWNCWTOZDWTPZRZESZWCWPEDCWD @@ -54372,7 +54372,7 @@ of the restricted converse (see ~ cnvrescnv ). (Contributed by NM, an ordered pair class abstraction. (Contributed by Mario Carneiro, 28-Apr-2015.) $) brab2a $p |- ( A R B <-> ( ( A e. C /\ B e. D ) /\ ps ) ) $= - ( wbr wcel wa cv copab cxp opabssxp eqsstri brel eleq2i opelopab2a syl5bb + ( wbr wcel wa cv copab cxp opabssxp eqsstri brel eleq2i opelopab2a bitrid cop df-br bitri biadanii ) EFILZEGMFHMNZBEFGHIICOGMDOHMNANCDPZGHQKACDGHRS TUHEFUDZUJMZUIBUHUKIMULEFIUEIUJUKKUAUFABCDEFGHJUBUCUG $. $} @@ -54439,7 +54439,7 @@ of the restricted converse (see ~ cnvrescnv ). (Contributed by NM, opbrop $p |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. R <. C , D >. <-> ps ) ) $= ( wcel wa cv wex cop wbr cxp opelxpi anim12i wceq opex eleq1 anbi1d eqeq1 - 4exbidv anbi12d anbi2d brab copsex4g syl5bb mpbirand ) INQJNQRZKNQLNQRZRZ + 4exbidv anbi12d anbi2d brab copsex4g bitrid mpbirand ) INQJNQRZKNQLNQRZRZ IJUAZKLUAZMUBZVANNUCZQZVBVDQZRZBURVEUSVFIJNNUDKLNNUDUEVCVGVAESFSUAZUFZVBG SHSUAZUFZRZARZHTGTFTETZRZUTVGBRCSZVDQZDSZVDQZRZVPVHUFZVRVJUFZRZARZHTGTFTE TZRVEVSRZVIWBRZARZHTGTFTETZRVOCDVAVBMIJUGKLUGVPVAUFZVTWFWEWIWJVQVEVSVPVAV @@ -55477,7 +55477,7 @@ ordered pairs as classes (in set.mm, the Kuratowski encoding). A more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (New usage is discouraged.) (Proof modification is discouraged.) $) csbcnvgALT $p |- ( A e. V -> `' [_ A / x ]_ F = [_ A / x ]_ `' F ) $= - ( vz vy wcel csb ccnv cv wbr copab wsbc sbcbr123 csbconstg breq12d syl5bb + ( vz vy wcel csb ccnv cv wbr copab wsbc sbcbr123 csbconstg breq12d bitrid opabbidv csbopabgALT df-cnv wceq a1i 3eqtr4rd csbeq2i eqtr4di ) BDGZABCHZ IZABEJZFJZCKZFELZHZABCIZHUFUKABMZFELUIUJUGKZFELZUMUHUFUOUPFEUOABUIHZABUJH ZUGKUFUPABUIUJCNUFURUIUSUJUGABUIDOABUJDOPQRUKAFEBDSUHUQUAUFFEUGTUBUCABUNU @@ -55762,7 +55762,7 @@ ordered pairs as classes (in set.mm, the Kuratowski encoding). A more abstraction. (Contributed by AV, 19-Oct-2023.) $) dmopabelb $p |- ( X e. V -> ( X e. dom { <. x , y >. | ph } <-> E. y ps ) ) $= - ( copab cdm wcel wex cab dmopab eleq2i cv wceq exbidv eqid elab2g syl5bb + ( copab cdm wcel wex cab dmopab eleq2i cv wceq exbidv eqid elab2g bitrid ) FACDHIZJFADKZCLZJFEJBDKZUAUCFACDMNUBUDCFUCECOFPABDGQUCRST $. $} @@ -56111,7 +56111,7 @@ of the relation (see ~ op1stb ). (Contributed by NM, 28-Jul-2004.) $) elrnmpt1 $p |- ( ( x e. A /\ B e. V ) -> B e. ran F ) $= ( vz vy wcel cv crn csb wceq wa wex vex wb id csbeq1a nfcsb1v bitr2d wrex eleq12d biantrud equcoms spcev df-rex nfv nfcri nfeq2 nfan eqeq2d anbi12d - cbvexv1 bitri eqeq1 anbi2d exbidv syl5bb rnmpt elab2g syl5ibr impcom ) CE + cbvexv1 bitri eqeq1 anbi2d exbidv bitrid rnmpt elab2g syl5ibr impcom ) CE IZAJZBIZCDKZIZVFVHVDGJZAVIBLZIZCAVICLZMZNZGOZVNVFGVEAPVNVFQAGVEVIMZVFVKVN VPVEVIBVJVPRAVIBSUCZVPVMVKAVICSZUDUAUEUFHJZCMZABUBZVOHCVGEWAVKVSVLMZNZGOZ VTVOWAVFVTNZAOWDVTABUGWEWCAGWEGUHVKWBAAGVJAVIBTUIAVSVLAVICTUJUKVPVFVKVTWB @@ -56122,7 +56122,7 @@ of the relation (see ~ op1stb ). (Contributed by NM, 28-Jul-2004.) $) elrnmptg $p |- ( A. x e. A B e. V -> ( C e. ran F <-> E. x e. A C = B ) ) $= ( vy crn wcel cv wceq wrex cab wral rnmpt eleq2i cvv wa syl wi wb rexbidv - r19.29 eleq1 biimparc elexd rexlimivw ex eqeq1 elab3g syl5bb ) DEIZJDHKZC + r19.29 eleq1 biimparc elexd rexlimivw ex eqeq1 elab3g bitrid ) DEIZJDHKZC LZABMZHNZJZCFJZABOZDCLZABMZUMUQDAHBCEGPQUTVBDRJZUAURVBUBUTVBVCUTVBSUSVASZ ABMVCUSVAABUDVDVCABVDDFVADFJUSDCFUEUFUGUHTUIUPVBHDRUNDLUOVAABUNDCUJUCUKTU L $. @@ -56364,7 +56364,7 @@ of the relation (see ~ op1stb ). (Contributed by NM, 28-Jul-2004.) $) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022.) $) opelres $p |- ( C e. V -> ( <. B , C >. e. ( R |` A ) <-> ( B e. A /\ <. B , C >. e. R ) ) ) $= - ( cop cres wcel cvv cxp wa df-res elin2 opelxp elex biantrud bitr4id syl5bb + ( cop cres wcel cvv cxp wa df-res elin2 opelxp elex biantrud bitr4id bitrid anbi1cd ) BCFZDAGZHTDHZTAIJZHZKCEHZBAHZUBKTDUCUADALMUEUDUFUBUEUDUFCIHZKUFBC AINUEUGUFCEOPQSR $. @@ -57314,7 +57314,7 @@ the restriction (of the relation) to the singleton containing this $( Eliminate the class existence constraint in ~ eliniseg . (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 17-Nov-2015.) $) eliniseg2 $p |- ( Rel A -> ( C e. ( `' A " { B } ) <-> C A B ) ) $= - ( ccnv csn cima wcel wbr wrel wb relcnv elrelimasn ax-mp relbrcnvg syl5bb ) + ( ccnv csn cima wcel wbr wrel wb relcnv elrelimasn ax-mp relbrcnvg bitrid ) CADZBEFGZBCPHZAICBAHPIQRJAKBCPLMBCANO $. ${ @@ -57545,7 +57545,7 @@ the restriction (of the relation) to the singleton containing this $( Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.) $) poleloe $p |- ( B e. V -> ( A ( R u. _I ) B <-> ( A R B \/ A = B ) ) ) $= - ( cid cun wbr wo wcel wceq brun ideqg orbi2d syl5bb ) ABCEFGABCGZABEGZHBDIZ + ( cid cun wbr wo wcel wceq brun ideqg orbi2d bitrid ) ABCEFGABCGZABEGZHBDIZ OABJZHABCEKQPROABDLMN $. $( Transitive law for general strict orders. (Contributed by Stefan O'Rear, @@ -57858,7 +57858,7 @@ the restriction (of the relation) to the singleton containing this velsn vp cxp ciun cop elxp rexbii rexcom4 exbii 3bitri eliun eldif opelxp wbr df-br vex ideq bitr3i anbi12i bitri anbi2i 2exbii eldifi elxpi 2eximi simpl 3syl ancli 19.42vv sylibr ancom eleq1 adantl pm5.32da 2exbidv mpbid - syl5bb biimpar impbii r19.42v simprl sylib eqeltrd simprr eldifad eldifbd + bitrid biimpar impbii r19.42v simprl sylib eqeltrd simprr eldifad eldifbd wb exlimivv necomd eqnetrd jca31 adantll difeq2d anbi12d cbvrexvw r19.29a biimpi simpll vsnid a1i simplr simpr eldifd rspcev syl12anc 3bitr4i eqriv sneq ) UAABAGZHZCXIIZUBZUCZBCUBZJIZUAGZXKKZABLZXODGZEGZUDZMZXRXIKZXSXJKZN @@ -58886,7 +58886,7 @@ singleton of the first member (with no sethood assumptions on ` B ` ). 15-Jun-2005.) $) cnvpo $p |- ( R Po A <-> `' R Po A ) $= ( vx vy vz cv wbr wn wa wi wral wpo r19.26 brcnv ralbii bitr2i c0 3bitr4i - vex ralcom weq id breq12d syl5bb notbid cbvralvw anbi12ci imbi12i anbi12i + vex ralcom weq id breq12d bitrid notbid cbvralvw anbi12ci imbi12i anbi12i ccnv ralidm wb wceq rzal 2thd wne r19.3rzv ralbidv pm2.61ine anbi1i bitri df-po ) CFZVCBGZHZVCDFZBGZVFEFZBGZIZVCVHBGZJZIEAKZDAKCAKZVHVHBUJZGZHZVHVF VOGZVFVCVOGZIZVHVCVOGZJZIZCAKZDAKEAKZABLAVOLVMCAKZDAKWDEAKZDAKVNWEWFWGDAV @@ -58952,7 +58952,7 @@ singleton of the first member (with no sethood assumptions on ` B ` ). /\ E. x e. X E. y e. Y A. a e. X A. b e. Y ( ch -> <. x , y >. = <. a , b >. ) ) ) $= ( vq wrex wi wral wa cv cop wceq rexxp wcel cxp wreu eqeq2 imbi2d ralbidv - weq reu3 eqeq1 imbi12d ralxp wb eqcom a1i 2ralbidva syl5bb 2rexbiia bitri + weq reu3 eqeq1 imbi12d ralxp wb eqcom a1i 2ralbidva bitrid 2rexbiia bitri anbi12i ) AGEFUAZUBAGUSLZAGKUFZMZGUSNZKUSLZOBIFLHELZBCPZDPZQZHPZIPZQZRZMZ IFNHENZDFLCELZOAGKUSUGUTVEVDVOABGHIEFJSVDAGPZVHRZMZGUSNZDFLCELVOVCVSKCDEF KPZVHRZVBVRGUSWAVAVQAVTVHVPUCUDUESVSVNCDEFVSBVKVHRZMZIFNHENVFETVGFTOZVNVR @@ -59185,7 +59185,7 @@ singleton of the first member (with no sethood assumptions on ` B ` ). 16-Oct-2024.) $) elpredgg $p |- ( ( X e. V /\ Y e. W ) -> ( Y e. Pred ( R , A , X ) <-> ( Y e. A /\ Y R X ) ) ) $= - ( cpred wcel ccnv csn cima wa wbr df-pred elin2 elinisegg anbi2d syl5bb ) F + ( cpred wcel ccnv csn cima wa wbr df-pred elin2 elinisegg anbi2d bitrid ) F ABEGZHFAHZFBIEJKZHZLECHFDHLZTFEBMZLFAUASABENOUCUBUDTBEFCDPQR $. $( Membership in a predecessor class. (Contributed by Scott Fenton, @@ -59450,7 +59450,7 @@ singleton of the first member (with no sethood assumptions on ` B ` ). ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x ) $= ( vz vw c0 cv wbr wn wral wrex wcel wa wi breq1 syl5bi expr ad2antrr crab wfr wpo wse w3a wss wne wex n0 wceq rabeq0 simprr notbid cbvralvw ralbidv - weq breq2 syl5bb rspcev ex syl cvv simprl simpl3 sylc seex syl2anc simpl1 + weq breq2 bitrid rspcev ex syl cvv simprl simpl3 sylc seex syl2anc simpl1 sess2 ssrab2 sstrid syl21anc rexrab ralrab simplr simplrl simpll2 simpllr fri poss simplrr potr syl13anc mp2and con3d idd ralimdva expimpd reximdva jad syld pm2.61dne exlimdv impr ) CEUBZCEUCZCEUDZUEZDCUFZDHUGZBIZAIZEJZKZ @@ -60089,7 +60089,7 @@ with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] shortened by Andrew Salmon, 25-Jul-2011.) $) ordtri4 $p |- ( ( Ord A /\ Ord B ) -> ( A = B <-> ( A C_ B /\ -. A e. B ) ) ) $= - ( wceq wss wa word wcel wn eqss wb ordtri1 ancoms anbi2d syl5bb ) ABCABDZBA + ( wceq wss wa word wcel wn eqss wb ordtri1 ancoms anbi2d bitrid ) ABCABDZBA DZEAFZBFZEZOABGHZEABISPTORQPTJBAKLMN $. $( An ordinal class and its singleton are disjoint. (Contributed by NM, @@ -60213,7 +60213,7 @@ with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] oneqmini $p |- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A = |^| B ) ) $= ( con0 wss wcel cv wn wral wa cint wceq ssint wi ssel anim12d ontri1 syl6 - wb expdimp pm5.74d con2b bitrdi syl5bb biimprd expimpd intss1 a1i adantrd + wb expdimp pm5.74d con2b bitrdi bitrid biimprd expimpd intss1 a1i adantrd ralbidv2 jcad eqss syl6ibr ) CDEZBCFZAGZCFZHZABIZJZBCKZEZVABEZJBVALUNUTVB VCUNUOUSVBUNUOJZVBUSVBBUPEZACIVDUSABCMVDVEURACBVDUQVENUQUPBFZHZNVFURNVDUQ VEVGUNUOUQVEVGSZUNUOUQJBDFZUPDFZJVHUNUOVIUQVJCDBOCDUPOPBUPQRTUAUQVFUBUCUJ @@ -60304,13 +60304,13 @@ with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] $( Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.) $) elsucg $p |- ( A e. V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) ) $= - ( csuc wcel csn wo wceq cun df-suc eleq2i elun bitri elsng orbi2d syl5bb ) + ( csuc wcel csn wo wceq cun df-suc eleq2i elun bitri elsng orbi2d bitrid ) ABDZEZABEZABFZEZGZACEZSABHZGRABTIZEUBQUEABJKABTLMUCUAUDSABCNOP $. $( Variant of membership in a successor, requiring that ` B ` rather than ` A ` be a set. (Contributed by NM, 28-Oct-2003.) $) elsuc2g $p |- ( B e. V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) ) $= - ( csuc wcel csn cun wceq wo df-suc eleq2i elun elsn2g orbi2d syl5bb ) ABDZE + ( csuc wcel csn cun wceq wo df-suc eleq2i elun elsn2g orbi2d bitrid ) ABDZE ABBFZGZEZBCEZABEZABHZIZPRABJKSUAAQEZITUCABQLTUDUBUAABCMNOO $. ${ @@ -61384,7 +61384,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). $( Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.) $) sbcfung $p |- ( A e. V -> ( [. A / x ]. Fun F <-> Fun [_ A / x ]_ F ) ) $= - ( vw vz vy wrel cv wbr wi wal wex wa wsbc csb wfun sbcal csbconstg syl5bb + ( vw vz vy wrel cv wbr wi wal wex wa wsbc csb wfun sbcal csbconstg bitrid wcel weq sbcan sbcrel sbcex2 sbcimg sbcbr123 breq12d imbi12d bitrd albidv sbcg exbidv anbi12d dffun3 sbcbii 3bitr4g ) BDUAZCHZEIZFIZCJZFGUBZKZFLZGM ZELZNZABOZABCPZHZUTVAVJJZVCKZFLZGMZELZNZCQZABOVJQVIUSABOZVGABOZNURVQUSVGA @@ -61428,7 +61428,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) $) dffun8 $p |- ( Fun A <-> ( Rel A /\ A. x e. dom A E! y x A y ) ) $= ( wfun wrel cv wbr wmo cdm wral wa weu dffun7 wex wi wcel moeu vex eldm - wb pm5.5 sylbi syl5bb ralbiia anbi2i bitri ) CDCEZAFZBFCGZBHZACIZJZKUGUIB + wb pm5.5 sylbi bitrid ralbiia anbi2i bitri ) CDCEZAFZBFCGZBHZACIZJZKUGUIB LZAUKJZKABCMULUNUGUJUMAUKUJUIBNZUMOZUHUKPZUMUIBQUQUOUPUMTBUHCARSUOUMUAUBU CUDUEUF $. @@ -61897,7 +61897,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). A. y e. B E! x e. A x R y ) $= ( cxp cin ccnv wfn wfun cdm wceq wa cv wbr wral wmo wcel wi 3bitr4i df-fn crn wreu df-rn eqeq1i anbi2i wrex wrmo rninxp anbi1i funcnv raleq moanimv - brinxp2 an21 bitri mobii df-rmo imbi2i biimt bitr4id bitrdi syl5bb r19.26 + brinxp2 an21 bitri mobii df-rmo imbi2i biimt bitr4id bitrdi bitrid r19.26 ralbiia pm5.32i ancom reu5 ralbii 3bitr2i ) ECDFGZHZDIVLJZVLKZDLZMVMVKUBZ DLZMZANZBNZEOZACUCZBDPZVLDUAVQVOVMVPVNDVKUDUEUFVQVMMZWAACUGZWAACUHZMZBDPZ VRWCVQWFBDPZMWEBDPZWIMWDWHVQWJWIABCDEUIUJVQVMWIVMVSVTVKOZAQZBVPPZVQWIABVK @@ -61936,7 +61936,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). ( vx vy vz vw vv cv wfun wss wo wral wa wrel wcel weq wi wal wex cuni cop funrel adantr ralimi reluni sylibr r19.28v anim1d dffun4 simprbi 19.21bbi ssel 19.21bi syl9r adantl anim2d jaod 2ralimi funeq sseq1 orbi12d anbi12d - sseq2 anbi2d cbvral2vw ralcom orcom syl5bb bitri anbi12i anandir r19.26-2 + sseq2 anbi2d cbvral2vw ralcom orcom bitrid bitri anbi12i anandir r19.26-2 imp anidm 2ralbii bitr2i 3bitr3i eluni exdistrv an4 2exbii 3bitr2i imbi1i biancomi 19.23v impexp 2albii albii 3bitr2ri 3imtr4i alrimiv alrimivv syl r2al sylanbrc ) BIZJZWQCIZKZWSWQKZLZCAMZNZBAMZAUAZOZDIZEIUBZXFPZXHFIUBZXF @@ -62333,7 +62333,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). NM, 10-Oct-2007.) $) fnssresb $p |- ( F Fn A -> ( ( F |` B ) Fn B <-> B C_ A ) ) $= ( cres wfn wfun cdm wceq wa wss df-fn funresd biantrurd ssdmres fndm sseq2d - fnfun bitr3id bitr3d syl5bb ) CBDZBEUAFZUAGBHZIZCAEZBAJZUABKUEUCUDUFUEUBUCU + fnfun bitr3id bitr3d bitrid ) CBDZBEUAFZUAGBHZIZCAEZBAJZUABKUEUCUDUFUEUBUCU EBCACQLMUCBCGZJUEUFBCNUEUGABACOPRST $. $( Restriction of a function with a subclass of its domain. (Contributed by @@ -62420,7 +62420,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). fnimaeq0 $p |- ( ( F Fn A /\ B C_ A ) -> ( ( F " B ) = (/) <-> B = (/) ) ) $= ( cima c0 wceq cdm cin wfn wa imadisj incom fndm sseq2d biimpar df-ss sylib - wss eqtrid eqeq1d syl5bb ) CBDEFCGZBHZEFCAIZBARZJZBEFCBKUFUCBEUFUCBUBHZBUBB + wss eqtrid eqeq1d bitrid ) CBDEFCGZBHZEFCAIZBARZJZBEFCBKUFUCBEUFUCBUBHZBUBB LUFBUBRZUGBFUDUHUEUDUBABACMNOBUBPQSTUA $. ${ @@ -64453,7 +64453,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). NM, 11-Nov-2005.) (Revised by NM, 20-Aug-2018.) $) csbfv12 $p |- [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) $= ( vy cvv wcel cfv csb wceq cv wbr cio csbiota sbcbr123 csbconstg df-fv c0 - wsbc csbprc breq2d syl5bb iotabidv eqtrid csbeq2i 3eqtr4g wn fveq1d eqtrd + wsbc csbprc breq2d bitrid iotabidv eqtrid csbeq2i 3eqtr4g wn fveq1d eqtrd 0fv eqtr2di pm2.61i ) BFGZABCDHZIZABCIZABDIZHZJUMABCEKZDLZEMZIZUPUSUQLZEM ZUOURUMVBUTABSZEMVDUTAEBNUMVEVCEVEUPABUSIZUQLUMVCABCUSDOUMVFUSUPUQABUSFPU AUBUCUDABUNVAECDQUEEUPUQQUFUMUGZUORURABUNTVGURUPRHRVGUPUQRABDTUHUPUJUKUIU @@ -64549,7 +64549,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). FL, 14-Sep-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) $) dffn5 $p |- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) ) $= ( vy wfn cv cfv cmpt wceq wcel wa copab wbr wrel fnrel dfrel4v sylib fnbr - ex pm4.71rd eqcom fnbrfvb syl5bb pm5.32da bitr4d opabbidv eqtrd fvex eqid + ex pm4.71rd eqcom fnbrfvb bitrid pm5.32da bitr4d opabbidv eqtrd fvex eqid df-mpt eqtr4di fnmpti fneq1 mpbiri impbii ) CBEZCABAFZCGZHZIZUPCUQBJZDFZU RIZKZADLZUSUPCUQVBCMZADLZVEUPCNCVGIBCOADCPQUPVFVDADUPVFVAVFKVDUPVFVAUPVFV ABUQVBCRSTUPVAVCVFVCURVBIUPVAKVFVBURUABUQVBCUBUCUDUEUFUGADBURUJUKUTUPUSBE @@ -64601,7 +64601,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). subclass. (Contributed by Raph Levien, 20-Nov-2006.) $) funimass4 $p |- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) ) $= - ( vy cdm wss wfun cima cv cfv wcel wral wb wi wal wa wceq wrex syl5bb wbr + ( vy cdm wss wfun cima cv cfv wcel wral wb wi wal wa wceq wrex bitrid wbr dfss2 vex elima eqcom ssel funbrfvb ex syl9 imp31 rexbidva bitr4id imbi1d r19.23v bitr4di albidv ralcom4 eleq1 ceqsalv ralbii bitr3i bitrdi ancoms fvex ) BDFZGZDHZDBIZCGZAJZDKZCLZABMZNVIEJZVHLZVNCLZOZEPZVFVGQZVMEVHCUBVSV @@ -64662,7 +64662,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). 8-Jan-2015.) (Revised by Thierry Arnoux, 10-May-2017.) $) feqmptdf $p |- ( ph -> F = ( x e. A |-> ( F ` x ) ) ) $= ( vy wf wfn cv cfv cmpt wceq ffn wcel wa copab wbr wrel fnrel nfcv dfrel4 - sylib nffn nfv fnbr pm4.71rd eqcom fnbrfvb syl5bb pm5.32da bitr4d opabbid + sylib nffn nfv fnbr pm4.71rd eqcom fnbrfvb bitrid pm5.32da bitr4d opabbid ex eqtrd df-mpt eqtr4di 3syl ) ACDEJECKZEBCBLZEMZNZOHCDEPVAEVBCQZILZVCOZR ZBISZVDVAEVBVFETZBISZVIVAEUAEVKOCEUBBIEGIEUCUDUEVAVJVHBIBCEGFUFVAIUGVAVJV EVJRVHVAVJVEVAVJVECVBVFEUHUPUIVAVEVGVJVGVCVFOVAVERVJVFVCUJCVBVFEUKULUMUNU @@ -64752,7 +64752,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). (Proof modification is discouraged.) $) fnsnfvOLD $p |- ( ( F Fn A /\ B e. A ) -> { ( F ` B ) } = ( F " { B } ) ) $= - ( vy wfn wcel wa cv cfv wceq cab wbr csn cima eqcom fnbrfvb syl5bb abbidv + ( vy wfn wcel wa cv cfv wceq cab wbr csn cima eqcom fnbrfvb bitrid abbidv df-sn a1i wrel fnrel relimasn syl adantr 3eqtr4d ) CAEZBAFZGZDHZBCIZJZDKZ BUJCLZDKZUKMZCBMNZUIULUNDULUKUJJUIUNUJUKOABUJCPQRUPUMJUIDUKSTUGUQUOJZUHUG CUAURACUBDBCUCUDUEUF $. @@ -64963,7 +64963,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). $( Domains of a function composition. (Contributed by NM, 27-Jan-1997.) $) dmfco $p |- ( ( Fun G /\ A e. dom G ) -> ( A e. dom ( F o. G ) <-> ( G ` A ) e. dom F ) ) $= - ( vx vy wfun cdm wcel wa ccom cv cop wex cfv wb eldm2g exbidv wceq syl5bb + ( vx vy wfun cdm wcel wa ccom cv cop wex cfv wb eldm2g exbidv wceq bitrid cvv opelco2g elvd bitrd adantl eldm2 opeq1 eleq1d ceqsexv funopfvb anbi1d fvex eqcom bitr3id bitr4d ) CFZACGZHZIZABCJZGHZADKZLCHZVAEKZLZBHZIZDMZEMZ ACNZBGHZUQUTVHOUOUQUTAVCLUSHZEMVHEAUSUPPUQVKVGEUQVKVGOEDAVCBCUPTUAUBQUCUD @@ -65654,7 +65654,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). (Contributed by Stefan O'Rear, 17-Jan-2015.) $) fndmdif $p |- ( ( F Fn A /\ G Fn A ) -> dom ( F \ G ) = { x e. A | ( F ` x ) =/= ( G ` x ) } ) $= - ( vy wfn wa cdm cv cfv wss wceq wcel wbr wex wn wb eqcom fnbrfvb syl5bb + ( vy wfn wa cdm cv cfv wss wceq wcel wbr wex wn wb eqcom fnbrfvb bitrid cdif cin wne crab difss dmss ax-mp fndm adantr sseqtrid sseqin2 sylib vex eldm adantll necon3abid breq2 notbid ceqsexv bitr4di adantlr anbi1d brdif fvex exbidv bitr2d rabbi2dva eqtr3d ) CBFZDBFZGZBCDUAZHZUBZVMAIZCJZVODJZU @@ -65750,7 +65750,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). 4-May-2007.) $) fvimacnvi $p |- ( ( Fun F /\ A e. ( `' F " B ) ) -> ( F ` A ) e. B ) $= ( wfun ccnv cima wcel cfv csn wss snssi funimass2 sylan2 fvex snss cdm wceq - wa cnvimass sseli wfn funfn fnsnfv sylanb sseq1d syl5bb mpbird ) CDZACEBFZG + wa cnvimass sseli wfn funfn fnsnfv sylanb sseq1d bitrid mpbird ) CDZACEBFZG ZRZACHZBGZCAIZFZBJZUJUHUNUIJUPAUIKUNBCLMUMULIZBJUKUPULBACNOUKUQUOBUJUHACPZG ZUQUOQZUIURACBSTUHCURUAUSUTCUBURACUCUDMUEUFUG $. @@ -65805,7 +65805,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). fvimacnvALT $p |- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) ) $= ( wfun cdm wcel wa csn cima wss ccnv cfv wb snssi funimass3 sylan2 fvex wfn - snss wceq eqid df-fn biimpri mpan2 fnsnfv sylan sseq1d syl5bb snssg 3bitr4d + snss wceq eqid df-fn biimpri mpan2 fnsnfv sylan sseq1d bitrid snssg 3bitr4d adantl ) CDZACEZFZGZCAHZIZBJZUPCKBIZJZACLZBFZAUSFZUNULUPUMJURUTMAUMNUPBCOPV BVAHZBJUOURVABACQSUOVDUQBULCUMRZUNVDUQTULUMUMTZVEUMUAVEULVFGCUMUBUCUDUMACUE UFUGUHUNVCUTMULAUSUMUIUKUJ $. @@ -65860,7 +65860,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). unpreima $p |- ( Fun F -> ( `' F " ( A u. B ) ) = ( ( `' F " A ) u. ( `' F " B ) ) ) $= ( vx wfun cdm wfn ccnv cun cima wceq funfn cv wcel cfv wa elpreima anbi2i - wo elun andi bitri orbi12d syl5bb bitr4id bitrd eqrdv sylbi ) CECCFZGZCHZ + wo elun andi bitri orbi12d bitrid bitr4id bitrd eqrdv sylbi ) CECCFZGZCHZ ABIZJZUKAJZUKBJZIZKCLUJDUMUPUJDMZUMNUQUINZUQCOZULNZPZUQUPNZUIUQULCQUJVAUR USANZPZURUSBNZPZSZVBVAURVCVESZPVGUTVHURUSABTRURVCVEUAUBVBUQUNNZUQUONZSUJV GUQUNUOTUJVIVDVJVFUIUQACQUIUQBCQUCUDUEUFUGUH $. @@ -65885,7 +65885,7 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ). = ( ( `' F " A ) i^i B ) ) $= ( vx wfun cres ccnv cima cin cdm wfn cv wb funfn cfv wa biancomi elpreima wcel elin anbi1i fvres eleq1d adantl pm5.32i bitri an32 bitrdi wceq fnfun - a1i funresd dmres df-fn sylanblrc syl anbi1d syl5bb 3bitr4d sylbi eqrdv ) + a1i funresd dmres df-fn sylanblrc syl anbi1d bitrid 3bitr4d sylbi eqrdv ) CEZDCBFZGAHZCGAHZBIZVBCCJZKZDLZVDSZVIVFSZMCNVHVIBVGIZSZVIVCOZASZPZVIVGSZV ICOZASZPZVIBSZPZVJVKVHVPVQWAPZVSPZWBVPWDMVHVPWCVOPWDVMWCVOVMVQWAVIBVGTQUA WCVOVSWAVOVSMVQWAVNVRAVIBCUBUCUDUEUFUKVQWAVSUGUHVHVCVLKZVJVPMVHVCEVCJVLUI @@ -66611,7 +66611,7 @@ in the range of the function (the implication "to the right" is always fveq1d breq123d wi nfcv nfv nffvmpt1 nfbr nfcsb1v nfeq2 nfbi fveq2 breq1d nfim csbeq1a eqeq2d bibi12d imbi2d cvv vex simpl eleq1d eqeqan12rd df-mpt id brabga sylancl fvmpt2 syl2an2 biantrurd 3bitr4d expcom vtoclgaf impcom - eqid pm5.32da bitrd syl5bb opelco copab eleq2i nfan eqeq1 opelopabf bitri + eqid pm5.32da bitrd bitrid opelco copab eleq2i nfan eqeq1 opelopabf bitri eleq1w anbi2d 3bitr4g eqrelrdv ) AUAUBJIUDZBDHUEZJIUFBDHUGAUAPZOPZIQZYGUB PZJQZRZOUHZYFDSZYIBYFHUIZTZRZYFYIUJZYDSYQYESZAYLYGYFIULZTZYKRZOUHZYPAYKUU AOAYKYTAYHYJYTAYHRZYTYJUUCYSYGAIUKZYHYSYGTZADEIABDFEILKUMZUNZUUDYHUUEYFYG @@ -67027,7 +67027,7 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more ( ( F |` { B } ) : { B } --> C <-> ( F ` B ) e. C ) ) $= ( vx wcel wfn csn cres wf cfv wb cv wi wceq sneq reseq2 syl wa cop eleq1d feq1d feq2 bitrd fveq2 bibi12d imbi2d fnressn vsnid fvres ax-mp sneqi vex - opeq2i eqeq2i fsn2 iba eleq1i bitr3di syl5bb sylbir expcom vtoclga impcom + opeq2i eqeq2i fsn2 iba eleq1i bitr3di bitrid sylbir expcom vtoclga impcom ) BAFDAGZBHZCDVFIZJZBDKZCFZLZVEEMZHZCDVMIZJZVLDKZCFZLZNVEVKNEBAVLBOZVRVKV EVSVOVHVQVJVSVMVFOZVOVHLVLBPVTVOVMCVGJVHVTVMCVNVGVMVFDQUBVMVFCVGUCUDRVSVP VICVLBDUEUAUFUGVEVLAFZVRVEWASVNVLVPTZHZOZVRAVLDUHWDVNVLVLVNKZTZHZOZVRWGWC @@ -67135,7 +67135,7 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more ~ fmptsng . (Contributed by AV, 4-Aug-2019.) $) fmptsnd $p |- ( ph -> { <. A , C >. } = ( x e. { A } |-> B ) ) $= ( vy vp cv wceq wa copab wcel cop wsbc wb csn velsn bicomi anbi1i opabbii - cmpt eqidd sbcan eqsbc1 anbi12d syl5bb sbcbidv eqeq1 adantl eqeq2d sbcied + cmpt eqidd sbcan eqsbc1 anbi12d bitrid sbcbidv eqeq1 adantl eqeq2d sbcied sbcg syl bitrd mpbir2and opelopabsb sylibr eleq1 syl5ibrcom syl5bi elopab wex wi opeq12 adantrr opeq2d opex snid eqeltrdi sylbid ex exlimdvv impbid impcomd eqrdv df-mpt a1i 3eqtr4a ) ABMZCNZKMZDNZOZBKPZWDCUAZQZWGOZBKPZCER @@ -67244,7 +67244,7 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more fnnfpeq0 $p |- ( F Fn A -> ( dom ( F \ _I ) = (/) <-> F = ( _I |` A ) ) ) $= ( vx wfn cv cfv wne crab c0 wceq cid cres wral cdif cdm wn rabeq0 wcel wa - wb nne fvresi eqeq2d adantl ralbidva syl5bb fndifnfp eqeq1d fnresi eqfnfv + wb nne fvresi eqeq2d adantl ralbidva bitrid fndifnfp eqeq1d fnresi eqfnfv bitr4id mpan2 3bitr4d ) BADZCEZBFZUOGZCAHZIJZUPUOKALZFZJZCAMZBKNOZIJBUTJZ USUQPZCAMUNVCUQCAQUNVFVBCAUNUOARZSVFUPUOJZVBUPUOUAVGVBVHTUNVGVAUOUPAUOUBU CUDUKUEUFUNVDURICABUGUHUNUTADVEVCTAUICABUTUJULUM $. @@ -67533,7 +67533,7 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more wne eqneqall com12 impd syl5bi adantr sylbid ex sylbi impcom exlimdvv orc a1d olc 3jaoi elpr expd 3mix2 3mix3 jaoi bitrdi mpbird elexd jca31 anim2i syl6ibr opeq12 eqeq2d eleq1 neeq1 anbi12d bi2anan9 spc2egv syl2anc jaoian - mpd anbi1i 2exbii sylibr jca impbid syl5bb eqrdv eqtrid ) AFQBUDUEZUFFXMQ + mpd anbi1i 2exbii sylibr jca impbid bitrid eqrdv eqtrid ) AFQBUDUEZUFFXMQ UGZUHZCGUIZDHUIZUJZFXMUKAUAXOXRUAUNZXORXSFRZXSXNRZSZAXSXRRZXSFXNULYBXTXSU BUNZUCUNZUIZTZYDXMRZYEQRZSZSZUCUMUBUMZSZAYCYAYLXTUBUCXSXMQUOUPAYMYCAXTYLY CAXTXSBEUIZXPXQUQZRZYLYCURZAFYOXSJUSZYPAYQYPAYLYCYPAYLSZXSXPTZXSXQTZUTZYC @@ -68102,7 +68102,7 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more ( A e. U. ran F <-> E. x e. dom F A e. ( F ` x ) ) ) $= ( vy crn cuni wcel cv wa wex wfun cfv cdm wrex eluni wceq wfn funfn eleq2 wb fvelrnb sylbi anbi2d r19.42v bitr4di biimparc reximi syl6bi fvelrn a1d - exlimdv ancld fvex eleq1 anbi12d spcev syl6 rexlimdva impbid syl5bb ) BCE + exlimdv ancld fvex eleq1 anbi12d spcev syl6 rexlimdva impbid bitrid ) BCE ZFGBDHZGZVBVAGZIZDJZCKZBAHZCLZGZACMZNZDBVAOVGVFVLVGVEVLDVGVEVCVIVBPZIZAVK NZVLVGVEVCVMAVKNZIVOVGVDVPVCVGCVKQVDVPTCRAVKVBCUAUBUCVCVMAVKUDUEVNVJAVKVM VJVCVIVBBSUFUGUHUKVGVJVFAVKVGVHVKGIZVJVJVIVAGZIZVFVQVJVRVQVRVJVHCUIUJULVE @@ -68148,7 +68148,7 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more dff13 $p |- ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) $= ( vz cv wbr wal wa cfv wceq wi wral wb wcel vex breldm eleq2d bitri dff12 - wf1 wf wmo wfn ffn cdm fndm syl5ib anim12d pm4.71rd eqcom syl5bb bi2anan9 + wf1 wf wmo wfn ffn cdm fndm syl5ib anim12d pm4.71rd eqcom bitrid bi2anan9 fnbrfvb anandis pm5.32da bitr4d imbi1d impexp bitrdi albidv 19.21v 19.23v wex fvex eqvinc imbi1i bitr4i imbi2i 2albidv breq1 mo4 albii r2al 3bitr4g alrot3 syl pm5.32i ) CDEUBCDEUCZAGZFGZEHZAUDZFIZJVTWAEKZBGZEKZLZWAWGLZMZB @@ -68400,7 +68400,7 @@ more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021.) ( vx vy cfv wne csn cdif wral wa wb wceq fveq2 adantr wf1 wcel dff14b cpr wf cv raleqi sneq difeq2d neeq1d raleqbidv ralprg difeq1i difprsn1 eqtrid adantl raleqdv neeq2d ralsng bitrd difprsn2 anbi12d necom pm4.71i bitr4di - biimpi syl5bb anbi2d ) ABDUAABDUEZIUFZDKZJUFZDKZLZJAVJMZNZOZIAOZPFCUBZGEU + biimpi bitrid anbi2d ) ABDUAABDUEZIUFZDKZJUFZDKZLZJAVJMZNZOZIAOZPFCUBZGEU BZPZFGLZPZVIFDKZGDKZLZPIJABDUCWCVRWFVIVRVQIFGUDZOZWCWFVQIAWGHUGWCWHWDVMLZ JAFMZNZOZWEVMLZJAGMZNZOZPZWFWAWHWQQWBVQWLWPIFGCEVJFRZVNWIJVPWKWRVOWJAVJFU HUIWRVKWDVMVJFDSUJUKVJGRZVNWMJVPWOWSVOWNAVJGUHUIWSVKWEVMVJGDSUJUKULTWCWQW @@ -68424,7 +68424,7 @@ more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021.) wf cv raleqi wb sneq difeq2d neeq1d raleqbidv raltpg adantr difeq1i tprot cpr anbi12i biimpi 3adant3 diftpsn3 syl eqtrid adantl neeq2d ralprg bitrd raleqdv 3adant1 tpcomb anim2i 3adant2 3anbi123d ancom 3anbi2i 3an6 3anrot - bicomi 3anbi123i anidm 3ancoma bitri 3bitri bitrdi syl5bb anbi2d ) ABDUAA + bicomi 3anbi123i anidm 3ancoma bitri 3bitri bitrdi bitrid anbi2d ) ABDUAA BDUGZKUHZDUBZLUHZDUBZMZLAWJUCZNZOZKAOZPGCUDZHEUDZIFUDZQZGHMZGIMZHIMZQZPZW IGDUBZHDUBZMZXHIDUBZMZXIXKMZQZPKLABDUEXGWRXNWIWRWQKGHIUFZOZXGXNWQKAXOJUIX GXPXHWMMZLAGUCZNZOZXIWMMZLAHUCZNZOZXKWMMZLAIUCZNZOZQZXNXBXPYIUJXFWQXTYDYH @@ -68889,7 +68889,7 @@ more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021.) 23-Dec-2016.) $) fliftel $p |- ( ph -> ( C F D <-> E. x e. X ( C = A /\ D = B ) ) ) $= ( wbr cop wceq wrex wa wcel cmpt crn df-br eleq2i eqid elrnmpti 3bitri cv - opex wb opthg2 syl2anc rexbidva syl5bb ) EFINZEFOZCDOZPZBJQZAECPFDPRZBJQU + opex wb opthg2 syl2anc rexbidva bitrid ) EFINZEFOZCDOZPZBJQZAECPFDPRZBJQU NUOISUOBJUPTZUAZSUREFIUBIVAUOKUCBJUPUOUTUTUDCDUHUEUFAUQUSBJABUGJSRCGSDHSU QUSUILMEFCDGHUJUKULUM $. @@ -69315,7 +69315,7 @@ H Isom ( R i^i ( A X. A ) ) , S ( A , B ) ) $= ( B i^i ( `' S " { ( H ` D ) } ) ) ) $= ( vx vy wcel wa ccnv csn cima cin cv wbr wrex cfv wb bitrdi wiso cab elin dfima2 wceq crn wf1o wfo isof1o f1ofo forn eleq2d 3syl wfn fvelrnb bitr3d - f1ofn cvv fvex vex eliniseg mp1i adantr anbi2d syl5bb anbi1d anass adantl + f1ofn cvv fvex vex eliniseg mp1i adantr anbi2d bitrid anbi1d anass adantl anbi12d isorel syl fnbrfvb bicomd sylan adantrr ancom breq1 pm5.32i bitri wi exp32 com23 imp pm5.32d bitrd rexbidv2 r19.41v bitr4d abbi2dv eqtr4id ) ABDEFUAZCAIZJZFADKCLMZNZMGOZHOZFPZGWOQZHUBBEKCFRZLMZNZGHFWOUDWMWSHXBWQX @@ -69498,7 +69498,7 @@ H Isom ( R i^i ( A X. A ) ) , S ( A , B ) ) $= H Isom R , S ( A , B ) ) $= ( vv vu cv cfv wceq wa wbr wrex wb wcel anbi1d wf1o copab wral wiso simpl wf1 f1of1 cop df-br eleq2 eqeq1 2rexbidv anbi2d opelopab weq anass f1fveq - fvex equcom bitrdi anassrs syl5bb rexbidv r19.42v rexbidva breq1 ceqsrexv + fvex equcom bitrdi anassrs bitrid rexbidv r19.42v rexbidva breq1 ceqsrexv adantl bitrd breq2 sylan9bb anandis sylan9bbr an32s bitr2id sylan df-isom ralrimivva sylanbrc ) EFIUAZHCLZALZIMZNZDLZBLZIMZNZOZWBWFGPZOZBEQAEQZCDUB ZNZOVTJLZKLZGPZWOIMZWPIMZHPZRZKEUCJEUCZEFGHIUDVTWNUEVTEFIUFZWNXBEFIUGXCWN @@ -69996,7 +69996,7 @@ Restricted iota (description binder) riotaeqimp $p |- ( ( ph /\ I = J ) -> X = Y ) $= ( wceq wa crio csb wb wcel nfcvd adantl eqcomi eqeq2i bicomd wreu riotacl a1i biimpa eqeq1i syl eqeltrid nfcsb1d nfeqd id cv csbeq1a eqeq2d syl2anc - nfv riota2df syl5bb wi bitrdi adantr csbeq1 eqcoms eqeq12 syl5ibrcom expd + nfv riota2df bitrid wi bitrdi adantr csbeq1 eqcoms eqeq12 syl5ibrcom expd eqcom ancoms sylbird mp2d ) ACDMZNZCGBMZHEOZMZFHDBPZMZFGMZAVMVQAVQVMVQVMQ AVPDCDVPJUAUBUFUCUGAVMVSVMFBMZHEOZDMZAVSCWBDIUHADERZWAHEUDZWCVSQADVPEJAVO HEUDZVPERLVOHEUEUIUJKWDWENVSWCWDWAVSHEDWDHURWDHDSZWDHFVRWDHFSWDHDBWGUKULW @@ -70651,7 +70651,7 @@ ordered pairs (for use in defining operations). This is a special case 15-Feb-2022.) $) fnbrovb $p |- ( ( F Fn ( V X. W ) /\ ( A e. V /\ B e. W ) ) -> ( ( A F B ) = C <-> <. A , B >. F C ) ) $= - ( co wceq cop cfv cxp wfn wcel wa wbr df-ov eqeq1i fnbrfvb2 syl5bb ) ABDGZC + ( co wceq cop cfv cxp wfn wcel wa wbr df-ov eqeq1i fnbrfvb2 bitrid ) ABDGZC HABIZDJZCHDEFKLAEMBFMNNUACDOTUBCABDPQABCDEFRS $. $( Equivalence of operation value and ordered triple membership, analogous to @@ -71336,7 +71336,7 @@ result of an operator (deduction version). (Contributed by Paul ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> ps ) ) $= ( vw wcel cvv cop cv wceq wa wex coprab wb elex w3a wi simpr eqeq1d eqcom opex vex otth2 bitri bitrdi anbi1d pm5.32i 3exbidv df-oprab eleq2i bitr2i - cab eleq1 syl5bb adantl 19.41vvv elisset 3anim123i 3exdistr 19.41v anbi2i + cab eleq1 bitrid adantl 19.41vvv elisset 3anim123i 3exdistr 19.41v anbi2i 3bitri 3anass bitr4i sylibr biantrurd bitr4id adantr expcom vtocle syl3an abid 3bitr3d ) FINFONZGJNGONZHKNHONZFGPZHPZACDEUAZNZBUBZFIUCGJUCHKUCWBWCW DUDZWIUEMWFWEHUIWJMQZWFRZWIWJWLSZWKCQZDQZPEQZPZRZASZETDTCTZWNFRZWOGRZWPHR @@ -71357,7 +71357,7 @@ result of an operator (deduction version). (Contributed by Paul ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> ps ) ) $= ( vw wcel cvv cop cv wceq wa wex coprab wb elex w3a wi simpr eqeq1d eqcom opex vex otth2 bitri bitrdi anbi1d pm5.32i 3exbidv df-oprab eleq2i bitr2i - cab abid syl5bb adantl 19.41vvv elisset 3anim123i eeeanv sylibr biantrurd + cab abid bitrid adantl 19.41vvv elisset 3anim123i eeeanv sylibr biantrurd eleq1 bitr4id adantr 3bitr3d expcom vtocle syl3an ) FINFONZGJNGONZHKNHONZ FGPZHPZACDEUAZNZBUBZFIUCGJUCHKUCVQVRVSUDZWDUEMWAVTHUIWEMQZWARZWDWEWGSZWFC QZDQZPEQZPZRZASZETDTCTZWIFRZWJGRZWKHRZUDZBSZETDTCTZWCBWHWNWTCDEWHWNWSASWT @@ -71473,7 +71473,7 @@ result of an operator (deduction version). (Contributed by Paul ( ( x e. A /\ y e. B ) /\ ph ) } |` ( C X. D ) ) = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ ph ) } ) $= ( wss wa cv wcel coprab cxp cres resoprab anass ssel pm4.71d bicomd an4 - bi2anan9 syl5bb anbi1d bitr3id oprabbidv eqtrid ) GEIZHFIZJZBKZELZCKZFLZJ + bi2anan9 bitrid anbi1d bitr3id oprabbidv eqtrid ) GEIZHFIZJZBKZELZCKZFLZJ ZAJZBCDMGHNOUKGLZUMHLZJZUPJZBCDMUSAJZBCDMUPBCDGHPUJUTVABCDUTUSUOJZAJUJVAU SUOAQUJVBUSAVBUQULJZURUNJZJUJUSUQURULUNUAUHVCUQUIVDURUHUQVCUHUQULGEUKRSTU IURVDUIURUNHFUMRSTUBUCUDUEUFUG $. @@ -71671,7 +71671,7 @@ result of an operator (deduction version). (Contributed by Paul elrnmpores $p |- ( D e. V -> ( D e. ran ( F |` R ) <-> E. x e. A E. y e. B ( D = C /\ x R y ) ) ) $= ( vz vp wcel cres cv wa wceq wex anbi2d copab crn wbr wrex eqeq1 anbi1d - 2exbidv coprab cab cop ancom eleq1 df-br bitr4di bitr3id syl5bb pm5.32i + 2exbidv coprab cab cop ancom eleq1 df-br bitr4di bitr3id bitrid pm5.32i an12 bitri 2exbii 19.42vv bitr3i opabbii dfoprab2 df-mpo 3eqtri reseq1i cmpo resopab eqtri 3eqtr4ri rneqi rnoprab elab2g r2ex ) FIMFHGNZUAZMAOZ CMBOZDMPZFEQZVQVRGUBZPZPZBRARZWBBDUCACUCVSKOZEQZWAPZPZBRARZWDKFVPIWEFQZ @@ -71690,7 +71690,7 @@ result of an operator (deduction version). (Contributed by Paul ( A. z e. ran F ph <-> A. x e. A A. y e. B ps ) ) $= ( vw wral cv wceq wrex wi wal wb crn wcel cab rnmpo raleqi eqeq1 2rexbidv ralab ralcom4 r19.23v albii bitr2i 3bitri bitri nfv ceqsalg ralbi bitr3id - ralimi syl syl5bb ) AEIUAZNZEOZHPZDGQZARZESZCFNZHJUBZDGNZCFNZBDGNZCFNZVCA + ralimi syl bitrid ) AEIUAZNZEOZHPZDGQZARZESZCFNZHJUBZDGNZCFNZBDGNZCFNZVCA EMOZHPZDGQCFQZMUCZNVFCFQZARZESZVIAEVBVRCDMFGHIKUDUEVQVSAEMVOVDPVPVECDFGVO VDHUFUGUHVIVGCFNZESWAVGCEFUIWBVTEVFACFUJUKULUMVLVHVMTZCFNVIVNTVKWCCFVHVEA RZESZDGNZVKVMWFWDDGNZESVHWDDEGUIWGVGEVEADGUJUKUNVKWEBTZDGNWFVMTVJWHDGABEH @@ -71715,7 +71715,7 @@ result of an operator (deduction version). (Contributed by Paul ovid $p |- ( ( x e. R /\ y e. S ) -> ( ( x F y ) = z <-> ph ) ) $= ( cv co wceq cop cfv wcel wa df-ov eqeq1i copab wfn coprab fnoprab fneq1i wb mpbir opabidw biimpri fnopfvb sylancr eleq2i oprabidw bitri baib bitrd - syl5bb ) BJZCJZGKZDJZLUPUQMZGNZUSLZUPEOUQFOPZAURVAUSUPUQGQRVCVBUTUSMZGOZA + bitrid ) BJZCJZGKZDJZLUPUQMZGNZUSLZUPEOUQFOPZAURVAUSUPUQGQRVCVBUTUSMZGOZA VCGVCBCSZTZUTVFOZVBVEUDVGVCAPZBCDUAZVFTVCABCDHUBVFGVJIUCUEVHVCVCBCUFUGVFU TUSGUHUIVEVCAVEVDVJOVIGVJVDIUJVIBCDUKULUMUNUO $. $} @@ -71760,7 +71760,7 @@ result of an operator (deduction version). (Contributed by Paul ov $p |- ( ( A e. R /\ B e. S ) -> ( ( A F B ) = C <-> th ) ) $= ( wcel wa co wceq cop cv coprab cfv df-ov fveq1i eqtri eqeq1i wfn fnoprab copab eleq1 anbi1d anbi2d opelopabg ibir fnopfvb sylancr anbi12d eloprabg - wb cvv mp3an3 bitrd syl5bb bianabs ) HKTZILTZUAZHIMUBZJUCZDVNHIUDZEUEZKTZ + wb cvv mp3an3 bitrd bitrid bianabs ) HKTZILTZUAZHIMUBZJUCZDVNHIUDZEUEZKTZ FUEZLTZUAZAUAZEFGUFZUGZJUCZVLVLDUAZVMWCJVMVOMUGWCHIMUHVOMWBSUIUJUKVLWDVOJ UDWBTZWEVLWBVTEFUNZULVOWGTZWDWFVDVTAEFGRUMVLWHVTVJVSUAZVLEFHIKLVPHUCZVQVJ VSVPHKUOUPZVRIUCZVSVKVJVRILUOUQZURUSWGVOJWBUTVAVJVKJVETWFWEVDNWAWIBUAVLCU @@ -72096,7 +72096,7 @@ result of an operator (deduction version). (Contributed by Paul ( vc wcel w3a wa co wceq cop cv coprab df-ov fveq1i eqtri eqeq1i wb eqeq2 cfv wi opeq2 eleq1d bibi12d imbi2d copab wfn weu wal ex alrimivv fnoprabg syl eleq1 anbi1d anbi2d opelopabg fnopfvb syl2an vtoclg com12 exp32 3imp2 - ibir anbi12d eloprabg adantl bitrd syl5bb biidd bianabs 3adant3 ) EIMUBZJ + ibir anbi12d eloprabg adantl bitrd bitrid biidd bianabs 3adant3 ) EIMUBZJ NUBZKLUBZUCZUDZIJOUEZKUFZWIWJUDZDUDZDWOIJUGZFUHZMUBZGUHZNUBZUDZAUDZFGHUIZ UPZKUFZWMWQWNXFKWNWROUPXFIJOUJWROXETUKULUMWMXGWRKUGZXEUBZWQEWIWJWKXGXIUNZ EWIWJWKXJUQWKEWPUDZXJXKXFUAUHZUFZWRXLUGZXEUBZUNZUQXKXJUQUAKLXLKUFZXPXJXKX @@ -73499,7 +73499,7 @@ result of an operator (deduction version). (Contributed by Paul ofrfval2 $p |- ( ph -> ( F oR R G <-> A. x e. A B R C ) ) $= ( vy wbr wral wceq cofr cmpt cfv wfn wcel ralrimiva eqid fnmpt syl fneq1d cv mpbird inidm wa adantr fveq1d ofrfval nffvmpt1 nfcv nfbr fveq2 breq12d - nfv cbvralw simpr fvmpt2 syl2anc ralbidva syl5bb bitrd ) AGHFUARQUKZBCDUB + nfv cbvralw simpr fvmpt2 syl2anc ralbidva bitrid bitrd ) AGHFUARQUKZBCDUB ZUCZVKBCEUBZUCZFRZQCSZDEFRZBCSZAQCCVMVOFCGHIIAGCUDVLCUDZADJUEZBCSVTAWABCM UFBCDVLJVLUGZUHUIACGVLOUJULAHCUDVNCUDZAEKUEZBCSWCAWDBCNUFBCEVNKVNUGZUHUIA CHVNPUJULLLCUMAVKCUEZUNZVKGVLAGVLTWFOUOUPWGVKHVNAHVNTWFPUOUPUQVQBUKZVLUCZ @@ -74341,7 +74341,7 @@ result of an operator (deduction version). (Contributed by Paul wwe wfr wor df-we df-so simpr ax-1 fr2nr 3adantr3 anbi2d notbid syl5ibcom wpo pm2.21 syl6 fr3nr df-3an biimpri ancoms nsyl pm2.21d expd 3jaod frirr a1i 3ad2antr1 jctild ex a2d alimdv 2alimdv equequ2 breq1 ralidmw cbvralvw - 3orbi123d bitr3i df-po ancrd impbid2 syl5bb pm5.32i bitri ) CDUACDUBZCDUC + 3orbi123d bitr3i df-po ancrd impbid2 bitrid pm5.32i bitri ) CDUACDUBZCDUC ZFWDAGZBGZDHZABIZWGWFDHZJZBCKZACKZFCDUDWDWEWMWECDUMZWMFZWDWMABCDUEWDWOWMW NWMUFWDWMWNWDWFEGZDHZAEIZWPWFDHZJZECKZBCKZACKZWFWFDHLZWHWGWPDHZFZWQMZFZEC KBCKACKZWMWNWDWFCNZWGCNZWPCNZOZWTMZEPZBPAPXMXHMZEPZBPAPXCXIWDXOXQABWDXNXP @@ -74460,7 +74460,7 @@ be a set (so instead it is a proper class). Here we prove the denial of Mario Carneiro, 8-Jun-2013.) $) ssonprc $p |- ( A C_ On -> ( A e/ _V <-> U. A = On ) ) $= ( cvv wnel wcel wn con0 wss cuni wceq df-nel word ssorduni ordeleqon orcomd - wo sylib ord uniexr syl6 con1d onprc uniexg eleq1 syl5ib impbid1 syl5bb + wo sylib ord uniexr syl6 con1d onprc uniexg eleq1 syl5ib impbid1 bitrid mtoi ) ABCABDZEZAFGZAHZFIZABJUJUIULUJULUHUJULEUKFDZUHUJULUMUJUMULUJUKKUMULO ALUKMPNQAFRSTULUHFBDZUAUHUKBDULUNABUBUKFBUCUDUGUEUF $. @@ -74680,7 +74680,7 @@ be a set (so instead it is a proper class). Here we prove the denial of ordpwsuc $p |- ( Ord A -> ( ~P A i^i On ) = suc A ) $= ( vx word cpw con0 cin csuc cv wcel wss elin velpw anbi2ci bitri ordsssuc wa wb expcom pm5.32d simpr wi ordsuc ordelon ex sylbi ancrd impbid2 bitrd - syl5bb eqrdv ) ACZBADZEFZAGZBHZUMIZUOEIZUOAJZPZUKUOUNIZUPUOULIZUQPUSUOULE + bitrid eqrdv ) ACZBADZEFZAGZBHZUMIZUOEIZUOAJZPZUKUOUNIZUPUOULIZUQPUSUOULE KVAURUQBALMNUKUSUQUTPZUTUKUQURUTUQUKURUTQUOAORSUKVBUTUQUTTUKUTUQUKUNCZUTU QUAAUBVCUTUQUNUOUCUDUEUFUGUHUIUJ $. @@ -75367,7 +75367,7 @@ also define a subset of the complex numbers ( ~ df-nn ) with analogous ~ nlimon ). (Contributed by NM, 1-Nov-2004.) $) dfom2 $p |- _om = { x e. On | suc x C_ { y e. On | -. Lim y } } $= ( vz com cv wlim wcel wi wal con0 crab csuc wn wss df-om wa cvv impexp wb - vex limelon mpan pm4.71ri imbi1i con34b ibar imbi2d syl5bb pm5.74i 3bitri + vex limelon mpan pm4.71ri imbi1i con34b ibar imbi2d bitrid pm5.74i 3bitri onsssuc ontri1 bitr3d ancoms weq limeq elrab a1i imbi12d pm5.74da bitr4id notbid simpr suceloni onelon ex ancrd impbid2 imbi1d bitr3id bitrd albidv syl dfss2 bitr4di rabbiia eqtri ) DCEZFZAEZVRGZHZCIZAJKVTLZBEZFZMZBJKZNZA @@ -76524,7 +76524,7 @@ as a separate axiom in an axiom system (such as Kunen's) that uses this imassrn sseq1 neeq1 anbi12d raleq rexeqbi1dv imbi12d spcgv syl7 syl com23 expd anabsi5 impd cres wb fores fveq2 breq1d breq2d brab fvres breqan12rd bitr4id notbid ralbidva rexbiia breq1 cbvfo rexbidv breq2 ralbidv cbvexfo - bitrd syl5bb sylibrd exp4b com34 imp4a alrimdv syl6ibr biimpd sylan9r wf1 + bitrd bitrid sylibrd exp4b com34 imp4a alrimdv syl6ibr biimpd sylan9r wf1 sylan9 sylbi df-f1o f1fveq bicomd 3orbi123d 2ralbidva eqeq1 eqeq2 anim12d a1i sylan9bb dfwe2 3imtr4g ) CDGUBZDFUCZIMZJMZFNZYPYQOZYQYPFNZUDZJDPZIDPZ QCEUCZKMZLMZENZUUEUUFOZUUFUUEENZUDZLCPKCPZQDFUECEUEYNYOUUDUUCUUKYNCDGUFZY @@ -77204,7 +77204,7 @@ Power Set ( ~ ax-pow ). (Contributed by Mario Carneiro, 20-May-2013.) /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) <-> A = <. X , Y , Z >. ) ) $= ( wcel w3a cxp c1st cfv wceq c2nd wa cop ad2antrl adantl jca sylan9eqr cotp - xp1st 3simpa eqopi syl2anc simprr3 df-ot eqeq2i eqop syl5bb opelxpi 3adant3 + xp1st 3simpa eqopi syl2anc simprr3 df-ot eqeq2i eqop bitrid opelxpi 3adant3 wb mpbird simp3 opelxpd eqeltrid adantr eleq1 2fveq3 ot1stg ot2ndg 3ad2ant3 fveq2 ot3rdg 3jca impbida ) EBHZFCHZGDHZIZABCJZDJZHZAKLZKLZEMZVONLZFMZANLZG MZIZOZAEFGUAZMZVKWCOZWEVOEFPZMZWAOZWFWHWAWFVOVLHZVQVSOZWHVNWJVKWBAVLDUBQWCW @@ -77280,7 +77280,7 @@ Power Set ( ~ ax-pow ). (Contributed by Mario Carneiro, 20-May-2013.) releldmdifi $p |- ( ( Rel A /\ B C_ A ) -> ( C e. ( dom A \ dom B ) -> E. x e. ( A \ B ) ( 1st ` x ) = C ) ) $= ( wrel wss wa cdm cdif wcel cv c1st wceq wrex wn eldif wb releldm2 adantr - cfv anbi1d syl5bb wral simprl relss 1stdm sylan eleq1 syl5ibcom rexlimdva + cfv anbi1d bitrid wral simprl relss 1stdm sylan eleq1 syl5ibcom rexlimdva impcom con3d ralnex syl6ibr adantld imp rexdifi syl2anc ex sylbid ) BEZCB FZGZDBHZCHZIJZAKZLTZDMZABNZDVEJZOZGZVIABCINZVFDVDJZVLGVCVMDVDVEPVCVOVJVLV AVOVJQVBABDRSUAUBVCVMVNVCVMGVJVIOACUCZVNVCVJVLUDVCVMVPVCVLVPVJVCVLVIACNZO @@ -77588,7 +77588,7 @@ Power Set ( ~ ax-pow ). (Contributed by Mario Carneiro, 20-May-2013.) cxp cfv cop vex op1std csbeq1d op2ndd csbeq2dv eqtrd raliunxp cmpo coprab wf cmpt nfcri nfan nfeq2 nfcsbw wb eleq1w adantr csbeq1a eleq2d sylan9bbr nfcv anbi12d sylan9eqr eqeq2d cbvoprab12 df-mpo 3eqtr4i fmpt bitr3i nfel1 - mpomptx nfralw cbvralw raleqbidv syl5bb nfxp xpeq12d cbviun feq2i 3bitr4i + mpomptx nfralw cbvralw raleqbidv bitrid nfxp xpeq12d cbviun feq2i 3bitr4i sneq ) AILZBJLZEMZMZFNZJAWJDMZOZICOZICWJUAZWOUEZUBZFGUQZEFNZBDOZACOACALZU AZDUEZUBZFGUQWQAKLZUCUFZBXHUDUFZEMZMZFNZKWTOXAXMWNKIJCWOXHWJWKUGPZXLWMFXN XLAWJXKMWMXNAXIWJXKWJWKXHIUHZJUHZUIUJXNAWJXKWLXNBXJWKEWJWKXHXOXPUKUJULUMZ @@ -77983,7 +77983,7 @@ Power Set ( ~ ax-pow ). (Contributed by Mario Carneiro, 20-May-2013.) ( vz vu vv cv cfv csb wss wral sseq1d nfcv c1st c2nd csn cxp ciun co cmpo cop cmpt mpomptsx eqtri fvmptss wceq op1std csbeq1d op2ndd csbeq2dv eqtrd vex raliunxp nfcsb1v nfxp weq sneq csbeq1a xpeq12d cbviun raleqi nfv nfss - nfralw cbvralw raleqbidv syl5bb 3bitr4ri df-ov sseq1i 3imtr4i ) AKNZUAOZB + nfralw cbvralw raleqbidv bitrid 3bitr4ri df-ov sseq1i 3imtr4i ) AKNZUAOZB VSUBOZEPZPZIQZKACANZUCZDUDZUEZRZFHUHZGOZIQEIQZBDRZACRZFHGUFZIQKWHWCIWJGGA BCDEUGKWHWCUIJABKCDEUJUKULWDKLCLNZUCZAWPDPZUDZUEZRAWPBMNZEPZPZIQZMWRRZLCR WIWNWDXDKLMCWRVSWPXAUHUMZWCXCIXFWCAWPWBPXCXFAVTWPWBWPXAVSLUSZMUSZUNUOXFAW @@ -78089,7 +78089,7 @@ Power Set ( ~ ax-pow ). (Contributed by Mario Carneiro, 20-May-2013.) ccnv wfun wf1o c0 snnzg fo1stres syl wal cop moeq moani brresi fo1st fofn wfn wb ax-mp fnbrfvb mp2an c2nd elxp7 eleq1 biimpac adantlr adantll elsni anbi2i eqopi anass1rs sylanl2 adantlrl sylanb adantl simprr simprl adantr - snidg opelxpd eqeltrd fveq2d op1stg syl2anc impbida bitr3id syl5bb mobidv + snidg opelxpd eqeltrd fveq2d op1stg syl2anc impbida bitr3id bitrid mobidv simpl eqtrd mpbiri alrimiv funcnv2 sylibr dff1o3 sylanbrc ) BCFZABGZHZAIW RJZKZWSUBUCZWRAWSUDWPWQUEUAWTBCUFAWQUGUHWPDLZELZWSMZDNZEUIXAWPXEEWPXEXCAF ZXBXCBUJZOZPZDNXHXFDDXGUKULWPXDXIDXDXBWRFZXBXCIMZPZWPXIWRXBXCIEQUMXLXJXBI @@ -78108,7 +78108,7 @@ Power Set ( ~ ax-pow ). (Contributed by Mario Carneiro, 20-May-2013.) cres ccnv wfun wf1o c0 wne snnzg fo2ndres syl wal cop moani brresi wfn wb moeq fo2nd fofn ax-mp fnbrfvb mp2an anbi2i c1st elxp7 eleq1 biimpac elsni eqopi anassrs sylanl2 adantlrr sylanb adantl simprr adantr simprl opelxpd - snidg eqeltrd op2ndg elvd sylan9eqr adantrl impbida bitr3id syl5bb mobidv + snidg eqeltrd op2ndg elvd sylan9eqr adantrl impbida bitr3id bitrid mobidv fveq2 mpbiri alrimiv funcnv2 sylibr dff1o3 sylanbrc ) ACFZAGZBHZBIWQUAZJZ WRUBUCZWQBWRUDWOWPUEUFWSACUGWPBUHUIWODKZEKZWRLZDMZEUJWTWOXDEWOXDXBBFZXAAX BUKZNZOZDMXGXEDDXFUPULWOXCXHDXCXAWQFZXAXBILZOZWOXHWQXAXBIEPUMXKXIXAIQZXBN @@ -79338,7 +79338,7 @@ any sets (which usually are functions) and any element (even not ( va cun wfn wcel wa wceq w3a cfv crab wss wral sseq1d wn wb cin wne cres c0 cv cdm csn cxp csupp fndm rabeqdv 3ad2ant1 unss ssrab2 biantrur rabun2 co sseq1i 3bitr4ri wi rabss fvres adantl simp2r fvconst2g eqeq12d nne a1i - sylan id simp3 minel syl2anr mtt syl 3bitr2rd ralbidva syl5bb bitrd fnfun + sylan id simp3 minel syl2anr mtt syl 3bitr2rd ralbidva bitrid bitrd fnfun wfun 3anim1i 3expb suppval1 3adant3 simp1 ssun2 fnssres fnconstg 3ad2ant2 syl2anc eqfnfv 3bitr4d ) CABHZIZCEJZFDJZKZABUAUDLZMZGUEZCNZFUBZGCUFZOZAPZ XACBUCZNZXABFUGUHZNZLZGBQZCFUIUQZAPXGXILZWTXFXCGWNOZAPZXLWTXEXOAWOWRXEXOL @@ -79618,7 +79618,7 @@ any sets (which usually are functions) and any element (even not ` B ` . (Contributed by SN, 25-May-2024.) $) suppcoss $p |- ( ph -> ( ( F o. G ) supp Z ) C_ ( G supp Y ) ) $= ( vk wcel cfv wceq wn wa crn ccom csupp co wfn wf dffn3 sylib fcod cv wne - cdif eldif ffnd elsuppfn syl3anc notbid anbi2d annotanannot bitrdi syl5bb + cdif eldif ffnd elsuppfn syl3anc notbid anbi2d annotanannot bitrdi bitrid wb nne anbi2i adantr simprl fvco3d simprr fveq2d 3eqtrd syl5bi sylbid imp ex suppss ) ACDUAZODEUBZEHUCUDZIACBVPDEADBUEBVPDUFJBDUGUHKUIAOUJZCVRULPZV SVQQZIRZAVTVSCPZVSEQZHUKZSZTZWBVTWCVSVRPZSZTZAWGVSCVRUMAWJWCWCWETZSZTWGAW @@ -79941,7 +79941,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and brtpos2 $p |- ( B e. V -> ( A tpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) ) $= ( vy vx wcel cvv wbr cdm ccnv csn cuni wa wi a1i wb cv wceq bitri reltpos - ctpos c0 cun brrelex1i elex adantr cmpt wex ccom df-tpos breqi syl5bb cfv + ctpos c0 cun brrelex1i elex adantr cmpt wex ccom df-tpos breqi bitrid cfv brcog wfun funmpt funbrfv2b ax-mp cnvex uniex dmmpti eleq2i eqcom anbi12i snex cnveqd unieqd fvmpt eqeq2d pm5.32i biancomi anbi1i anass exbii breq1 eqid sneq anbi2d ceqsexv bitrdi expcom pm5.21ndd ) BDGZAHGZABCUBZIZACJKUC @@ -80318,7 +80318,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and mpofun mp1i adantr eleq2d opelxp bitrdi anbi1d an21 ibar bicomd adantl co df-ov csb cmpo nfcv nfcsb1v nfcsbw csbeq1a sylan9eq cbvmpo eqcomd equcoms eqtri a1i csbeq2dv simpr wi rsp2 impl ovmpod eqtr3id eqcom bitrd pm5.32da - eqeq1d syl5bb 3bitrrd opabbidv eqtr2id mpteq2dva eqtrid ) AEUABEUBZUBZBOZ + eqeq1d bitrid 3bitrrd opabbidv eqtr2id mpteq2dva eqtrid ) AEUABEUBZUBZBOZ COZUCZLOZEUDZCLUEZPZBGCHDPZPZBCLEUFAXLBGXKPXNABXEGXKAXEGHUHZUBZGAXDXOADFQ ZCHUIBGUIZXDXORZJBCGHDEFIUGUJZUKAHULUMXPGRKGHUNUJUOUPABGXKXMAXFGQZSZXMXGH QZXIDRZSZCLUEXKCLHDUQYBYEXJCLYBXJXHXDQZXHEURZXIRZSZYAYCSZYHSZYEEUSXJYIUTY @@ -80503,7 +80503,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and frecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ F ) ) $= ( vf vz vy cv wss cpred wral wa wceq csb wsbc csbconstg bitrd eqtrid wcel wfn cfv cres co w3a wex cuni cfrecs csbuni csbab sbcex2 sbc3an sbcg sbcan - cab sbcssg sseq1d sbcralg csbpredg predeq3 sseq12d ralbidv anbi12d syl5bb + cab sbcssg sseq1d sbcralg csbpredg predeq3 sseq12d ralbidv anbi12d bitrid syl eqtrd sbceqg csbov123 csbres reseq12d oveq12d 3anbi123d exbidv abbidv eqeq12d unieqd df-frecs csbeq2i 3eqtr4g ) BFUAZABGJZHJZUBZWCCKZCDIJZLZWCK ZIWCMZNZWFWBUCZWFWBWGUDZEUEZOZIWCMZUFZHUGZGUPZUHZPZWDWCABCPZKZXAABDPZWFLZ @@ -81917,7 +81917,7 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $= A. y e. x ( F ` y ) e. ( F ` x ) ) ) $= ( wsmo cdm con0 wf word wel cfv wcel wral w3a df-smo ralcom impexp 3anass cv wi wa simpr ordtr1 3impib 3com23 simp3 3expia impbid2 bitr3id ralbidv2 - jca imbi1d ralbidva syl5bb pm5.32i anbi2i 3bitr4i bitri ) CDCEZFCGZURHZBA + jca imbi1d ralbidva bitrid pm5.32i anbi2i 3bitr4i bitri ) CDCEZFCGZURHZBA IZBRZCJARZCJKZSZAURLBURLZMZUSUTVDBVCLZAURLZMZBACNUSUTVFTZTUSUTVITZTVGVJVK VLUSUTVFVIVFVEBURLZAURLUTVIVEBAURUROUTVMVHAURUTVCURKZTZVEVDBURVCVBURKZVES VPVATZVDSVOVEVPVAVDPVOVQVAVDVOVQVAVPVAUAUTVNVAVQUTVNVAMVPVAUTVAVNVPUTVAVN @@ -83080,7 +83080,7 @@ other applications (for instance in intuitionistic set theory) need it. U. { y | E. x e. B y = ( rec ( F , A ) ` x ) } ) $= ( wcel wlim wa crdg cfv cima cuni cv wceq cab wex con0 wb word rdglim cop wrex dfima3 df-rex wi limord ordelord ex vex elon syl6ibr syl wfn rdgfnon - eqcom fnopfvb mpan syl5bb syl6 pm5.32d exbidv abbidv eqtrid unieqd adantl + eqcom fnopfvb mpan bitrid syl6 pm5.32d exbidv abbidv eqtrid unieqd adantl bitr2id eqtrd ) DEGZDHZIDFCJZKVKDLZMZBNZANZVKKZOZADUCZBPZMZCDEFUAVJVMVTOV IVJVLVSVJVLVODGZVOVNUBVKGZIZAQZBPVSABVKDUDVJWDVRBVRWAVQIZAQVJWDVQADUEVJWE WCAVJWAVQWBVJWAVORGZVQWBSVJDTZWAWFUFDUGWGWAVOTZWFWGWAWHDVOUHUIVOAUJUKULUM @@ -83384,7 +83384,7 @@ other applications (for instance in intuitionistic set theory) need it. reseq1i eqtrd fvex opelxpi mpan2 eqeltrd rgen ffnfv mpbir2an frn ax-mp wb wal wex wrex df-br fvelrnb eqeq1d rexbiia 3bitri adantl vex opth1 fveqeq2 syl6bi biimpd syli fveq2 op2nd eqtr2di syl6 rexlimdva rspcev mpdan eqeq2d - wa opeq2 rexbidv syl5ibrcom impbid syl5bb alrimiv eqeq2 bibi2d albidv syl + wa opeq2 rexbidv syl5ibrcom impbid bitrid alrimiv eqeq2 bibi2d albidv syl spcev eu6 sylibr dff3 df-ima feq1i dffn2 ) BJUEZJKJLXLMZXMJLBJUFZUAZMZXPX OJLUBZUCZGNZHNZXOUDZHUGZGJUHJXQXNMZXRYCXNJKZXTXNOZXQPZHJUHYDCAJLCNZUIYGAN DUJQUKZULEUMOQZUNZJUFZJKYIYHUOJXNYKBYJJFUSUPRZYFHJXTJPZYEXTXTBOZSOZQZXQYM @@ -84901,7 +84901,7 @@ A C_ ( B .o A ) ) $= c0 sylib simp3rl simp2rr simp3rr eqtr4d wb simp11 simp2ll simp2lr simp3ll simp13 simp3lr omopth2 syl222anc mpbid opeq12 3expia exp4b expd rexlimdvv syl imp expimpd alrimivv opeq1 eqeq2d oveq2 oveq1d eqeq1d opeq2 cbvrex2vw - anbi12d eqeq1 anbi1d 2rexbidv syl5bb eu4 sylanbrc ) DIJZEIJZDUOUCZUDZCKZA + anbi12d eqeq1 anbi1d 2rexbidv bitrid eu4 sylanbrc ) DIJZEIJZDUOUCZUDZCKZA KZBKZLZMZDWSNOZWTPOZEMZQZBDRZAIRZCSZXHFKZGKZHKZLZMZDXKNOZXLPOZEMZQZHDRGIR ZQWRXJMZTZFUECUEXHCUFWQXEBDRZAIRZXIABDEUAYCXGCSZAIRXIYBYDAIYBXFCSZBDRYDYE XEBDYEXBCSXECXAWSWTUBUGXBXECUHUIUJXFBCDUKULUJXGACIUKUMUPWQYACFWQXHXSXTWQX @@ -85299,7 +85299,7 @@ A C_ ( B .o A ) ) $= eqssd suceq eqtr3d eleqtrd omord2 wn oveq1d oveq2 eleq1d 3anass eqeq1d cv eqsstrd cop wrex cio weq eqeq2d anbi12d adantl ontri1 om0 oa0r syl5ibrcom eqtrd sylibd necon3bd sylanbrc impbida ex pm5.32rd bitrdi eleq2d 3anbi23d - anass bitr3id ne0d weu opeq1 opeq2 cbvrex2vw eqeq1 anbi1d 2rexbidv syl5bb + anass bitr3id ne0d weu opeq1 opeq2 cbvrex2vw eqeq1 anbi1d 2rexbidv bitrid omeu cbviotavw eqtri opiota sylan9bbr pm5.32da bitrd 3an4anass 3bitr4g ) ERUDUESZFRUFUESZUGZGRSZHEUFUESZUGZJEGUHTZSZUWBHUITZJUJTZFUKZUGZUGZGKUKZHL UKZJMUKZUGZUGZUVSUVTUWCULUWFUGUWIUWJUWKULUVRUWHUWIHRSZUWGUGZUGZUWMUVRUWHU @@ -86490,7 +86490,7 @@ general ordinal versions of these theorems (in this case ~ oa0r ) so brdifun $p |- ( ( A e. X /\ B e. X ) -> ( A R B <-> -. ( A .< B \/ B .< A ) ) ) $= ( wcel wa wbr ccnv cun wn wo cxp wb cop opelxpi df-br sylibr cdif brcnvg - breqi brdif bitri baib syl brun orbi2d syl5bb notbid bitrd ) AEGBEGHZABCI + breqi brdif bitri baib syl brun orbi2d bitrid notbid bitrd ) AEGBEGHZABCI ZABDDJZKZIZLZABDIZBADIZMZLULABEENZIZUMUQOULABPVAGVBABEEQABVARSUMVBUQUMABV AUOTZIVBUQHABCVCFUBABVAUOUCUDUEUFULUPUTUPURABUNIZMULUTABDUNUGULVDUSURABEE DUAUHUIUJUK $. @@ -86571,7 +86571,7 @@ general ordinal versions of these theorems (in this case ~ oa0r ) so by Mario Carneiro, 6-Dec-2016.) $) eqerlem $p |- ( z R w <-> [_ z / x ]_ A = [_ w / x ]_ A ) $= ( cv wbr wceq wsbc csb wb cvv nfcsb1v weq sbciegf elv brabsb nfeq nfv vex - csbie csbeq1 eqtr3id eqeq2d csbeq1a eqeq1d syl5bb bitri ) CJZDJZGKEFLZBUN + csbie csbeq1 eqtr3id eqeq2d csbeq1a eqeq1d bitrid bitri ) CJZDJZGKEFLZBUN MZAUMMZAUMENZAUNENZLZUOABUMUNGIUAUQUTOCUPUTAUMPAURUSAUMEQAUNEQUBUPEUSLZAC RZUTUPVAODUOVABUNPVABUCBDRZFUSEVCFABJZENUSAVDEFBUDHUEAVDUNEUFUGUHSTVBEURU SAUMEUIUJUKSTUL $. @@ -87276,7 +87276,7 @@ general ordinal versions of these theorems (in this case ~ oa0r ) so brecop $p |- ( ( ( A e. G /\ B e. G ) /\ ( C e. G /\ D e. G ) ) -> ( [ <. A , B >. ] .~ .<_ [ <. C , D >. ] .~ <-> ps ) ) $= ( wcel wa cop cec wbr cv wceq wex ecopqsi copab df-br eleq2i bitri anbi1d - wb eqeq1 4exbidv anbi2d opelopab2 syl5bb syl2an opeq12 eceq1d anim12i cxp + wb eqeq1 4exbidv anbi2d opelopab2 bitrid syl2an opeq12 eceq1d anim12i cxp wi opelxpi opelxp wer a1i id ereldm bitr3id syl5ibr im2anan9 an4s ex mpdd com13 pm5.74d cgsex4g eqcom anbi12i biimt anbi12d 3bitr4d bitrd ) INUBJNU BUCZKNUBLNUBUCZUCZIJUDZMUEZKLUDZMUEZPUFZWMEUGZFUGZUDZMUEZUHZWOGUGZHUGZUDZ @@ -87380,7 +87380,7 @@ general ordinal versions of these theorems (in this case ~ oa0r ) so ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) ) ) $= ( vw cv cec wceq wa wrex coprab wcel cio cmpo simpl reximi cqs eleq2i vex co elqs bitri anbi12i reeanv bitr4i sylibr pm4.71ri wb eroveu iota1 eqcom - weu syl bitrdi pm5.32da syl5bb oprabbidv df-mpo nfiota1 nfeq2 nfan anbi2d + weu syl bitrdi pm5.32da bitrid oprabbidv df-mpo nfiota1 nfeq2 nfan anbi2d nfv eqeq1 cbvoprab3 eqtr4i 3eqtr4g ) ABURZUDURZLUSUTZCURZUCURZMUSUTZVAZDU RZXAXDJVLNUSUTZVAZUCHVBZUDGVBZBCDVCWTPVDZXCQVDZVAZXGXKDVEZUTZVAZBCDVCZKBC PQXOVFZAXKXQBCDXKXNXKVAAXQXKXNXKXFUCHVBZUDGVBZXNXJXTUDGXIXFUCHXFXHVGVHVHX @@ -87574,7 +87574,7 @@ the cancellation property (fifth hypothesis), show that the relation simpr mpbid opelxp2 syl ex caovcl syl5ibr ndmovrcl simprd syl6com adantll eleq1 wbr adantr erth bitr3d expr pm5.21ndd an32s eqcom erdm ax-mp eleq2i wne cdm ecdmn0 opelxp 3bitr3i simplbi2 ad2antlr necon2bd ndmov nsyl5 syl6 - mtbiri simprbi necon1bd impbid syl5bb necon1bi adantl eqeq1d simpl eqeq2d + mtbiri simprbi necon1bd impbid bitrid necon1bi adantl eqeq1d simpl eqeq2d syl5 3bitr4d pm2.61dan ) CIOZEIOZPZDIOZCDUAZHUBZEFUAZHUBZQZCFGUCZDEGUCZQZ UDZWRXAWSXJWRXAPZWSPZFIOZXFXIXLXFXMXLXFPZXDIIUEZOZXMXNXBXOOZXPXKXQWSXFCDI IUFZUGXNXBXDHXOXOHUHZXNJUIXLXFUKUJULEFIIUMUNUOXAWSXIXMRWRXIXAWSPZXGIOZXMX @@ -87938,7 +87938,7 @@ the first case of his notation (simple exponentiation) and subscript it 8-Aug-2024.) $) mapfset $p |- ( B e. V -> { f | f : A --> B } = ( B ^m A ) ) $= ( vm wcel cv wf cab cmap co vex feq1 elab wa cvv simpr dmfex mpan adantr - elmapd exbiri pm2.43b elmapi impbid1 syl5bb eqrdv ) BDFZEABCGZHZCIZBAJKZE + elmapd exbiri pm2.43b elmapi impbid1 bitrid eqrdv ) BDFZEABCGZHZCIZBAJKZE GZUKFABUMHZUHUMULFZUJUNCUMELZABUIUMMNUHUNUOUHUNUOUNUHUOUNUNUHOBAUMDPUNUHQ UNAPFZUHUMPFUNUQUPABPUMRSTUAUBUCUMBAUDUEUFUG $. $} @@ -88281,7 +88281,7 @@ the first case of his notation (simple exponentiation) and subscript it ) $= ( cv csn wceq wcel wf cvv wa wex syl wb mpbid cop wrex cmap co a1i elmapd snex crn wbr weu wfn ffn snidg fneu syl2anr cab euabsn cima wrel relimasn - frel cdm imaeq2d imadmrn eqtr3di eqtr3d eqeq1d exbidv syl5bb adantl sseld + frel cdm imaeq2d imadmrn eqtr3di eqtr3d eqeq1d exbidv bitrid adantl sseld fdm frn vsnid eleq2 mpbiri impel adantll ffrn feq3 syl5ibcom imp ad2antrr vex fsng sylancl jca ex eximdv mpd df-rex sylibr w3a f1osng adantr f1oeq1 wf1o bicomd f1of 3adant2 wss snssi 3ad2ant2 fssd rexlimdv3a bitrd abbi2dv @@ -88468,7 +88468,7 @@ the first case of his notation (simple exponentiation) and subscript it ixpsnval $p |- ( X e. V -> X_ x e. { X } B = { f | ( f Fn { X } /\ ( f ` X ) e. [_ X / x ]_ B ) } ) $= ( wcel csn cixp cv wfn cfv wral wa cab dfixp wsbc ralsnsg sbcel12 csbfv2g - csb csbvarg fveq2d eqtrd eleq1d syl5bb bitrd anbi2d abbidv eqtrid ) EDFZA + csb csbvarg fveq2d eqtrd eleq1d bitrid bitrd anbi2d abbidv eqtrid ) EDFZA EGZBHCIZUKJZAIZULKZBFZAUKLZMZCNUMEULKZAEBTZFZMZCNAUKBCOUJURVBCUJUQVAUMUJU QUPAEPZVAUPAEDQVCAEUOTZUTFUJVAAEUOBRUJVDUSUTUJVDAEUNTZULKUSAEUNDULSUJVEEU LAEDUAUBUCUDUEUFUGUHUI $. @@ -88855,7 +88855,7 @@ the first case of his notation (simple exponentiation) and subscript it csb w3a nfcv nfcsb1v csbeq1a cbvixp eleq2i elixp2 3anass eqid fnmpt simpr 3bitri eqeltrd jca dffn2 fmpt eleq1d biimpd ralim sylbir sylbi imp impbii nfv nffvmpt1 nfel weq fveq2 eleq12d cbvralw anbi2i bitri mptexg biantrurd - wf bitr2id syl5bb ) BEGBHGZABCIZABDJZGZCDGZABKZLBEMWCWAHGZWABUAZFNZWAOZAW + wf bitr2id bitrid ) BEGBHGZABCIZABDJZGZCDGZABKZLBEMWCWAHGZWABUAZFNZWAOZAW HDUBZGZFBKZPZPZVTWEWCWAFBWJJZGWFWGWLUCWNWBWOWAAFBDWJFDUDAWHDUEZAWHDUFZUGU HFBWJWAUIWFWGWLUJUNWEWMVTWNWEWGANZWAOZDGZABKZPZWMWEXBWEWGXAABCWADWAUKZULW DWTABWRBGZWDPWSCDABCDWAXCQXDWDUMUORUPWGXAWEWGBHWAVQZXAWESZBWAUQXECHGZABKZ @@ -90077,7 +90077,7 @@ the Axiom of Power Sets (unlike ~ enrefg ). (Contributed by ( vy vx vz cv cint cop wcel wceq wex cvv inteq inteqd vex op1stb adantr wa csn cxp snex xpex elxp eqtrdi eqeltrdi exlimivv sylbi opex wb eqvisset a1i ancom anass velsn anbi1i 3bitr3i exbii eqeq2d anbi1d ceqsexv pm4.71ri - opeq2 eqtr2di bitri 3bitri opeq1 anbi12d ceqsexgv syl5bb pm5.32ri pm4.71i + opeq2 eqtr2di bitri 3bitri opeq1 anbi12d ceqsexgv bitrid pm5.32ri pm4.71i eleq1 syl bitr2i en2i ) EFABUAZUBZAEHZIZIZFHZBJZAVRCBUCUDCVTVSKZVTWCGHZJZ LZWCAKZWFVRKZTZTZGMZFMZWBNKZFGVTAVRUEZWLWOFGWHWOWKWHWBWCNWHWBWGIZIWCWHWAW QVTWGOPWCWFFQZGQRUFWRUGSUHUIWDNKWIWCBUJUMWEWCWBLZTVTWBBJZLZWBAKZTZWSTZVTW @@ -90256,7 +90256,7 @@ the Axiom of Power Sets (unlike ~ enrefg ). (Contributed by ( vz vw vv vu cdom cv wa csn cdm cuni cop cvv wcel wi wceq wb wbr wf1 cxp vf vx vy brdomi crn cfv wf f1f ffvelrn ex syl anim2d adantld elxp4 opelxp 3imtr4g adantl wrex elxp2 vex fvex opth f1fveq ancoms anbi2d ad2ant2l imp - syl5bb adantlr dmeqd unieqd op1sta eqtrdi op2nda fveq2d opeq12d eqeqan12d + bitrid adantlr dmeqd unieqd op1sta eqtrdi op2nda fveq2d opeq12d eqeqan12d sneq rneqd ad2antlr eqeq12 bitrdi 3bitr4d exp53 com23 rexlimivv rexlimdvv syl2anb com12 reldom brrelex1i xpexg sylancr adantr brrelex2i exlimddv dom3d ) ABIUAZABUDJZUBZCAUCZCBUCZIUAUDABUDUGXAXCKUEUFXDXEUEJZLZMZNZXGUHZN @@ -90366,7 +90366,7 @@ the Axiom of Power Sets (unlike ~ enrefg ). (Contributed by simpr ad2antrr ontr2 mp2and simpllr on0eln0 mpbird om00el simpld syl31anc ne0d omord2 impbid expr pm5.32rd sylan2 anbi2i bitrdi anbi2d an12 2exbidv eqcom copab cmpo coprab df-mpo dfoprab2 3eqtri breqi df-br opabidw 3bitri - r2ex 3bitr4g syl5bb eubidv ralrimiva fnres sylibr wrel cdm crn df-rn frnd + r2ex 3bitr4g bitrid eubidv ralrimiva fnres sylibr wrel cdm crn df-rn frnd relcnv eqsstrrid relssres sylancr fneq1d dff1o4 sylanbrc ) CIJZDIJZKZEDCU AZUBEUCZCDLMZUBZUURUUTEUEUUQUURUUTEUUQCANZLMZBNZUFMZUUTJZBCUGADUGUURUUTEU DUUQUVFABDCUUQUVBDJZUVDCJZKZKZCUVBUHZLMZUUTUVEUVJUVKDOZUVLUUTOZUVJDUIZUVG @@ -91173,7 +91173,7 @@ excluded middle (LEM), and in ILE the LEM is not accepted as necessarily nfel1 eleq1d rspc sylc opelxpd ralrimiva weq wb wrex simprd r19.21bi reu6 xp2nd anim12dan reeanv pm4.38 ralimdv impcom reximi sylbir syl vex op1std ex com12 csbeq1d eqeq2d op2ndd anbi12d eqeq1 bibi12d ralxp nfv nfcv nfeq2 - nfan nfbi nfralw anbi2d opeq2 eqeq1d cbvralw anbi1d ralbidv syl5bb bitr4i + nfan nfbi nfralw anbi2d opeq2 eqeq1d cbvralw anbi1d ralbidv bitrid bitr4i opeq1 eqeq2 bitrdi bibi2d 2ralbidv rexxp sylibr ralrimivva reubidv opeq12 opth nfop syl2an cbvmpo opeq12d mpompt eqtr4i sylanbrc ) ABLUJZUBUCZHUDZC YFUEUCZIUDZUFZEGUGZQZLDFUGZRUAUJZYKSZLYNUHZUAYLRZYNYLBCDFHIUFZUIZUKAYMLYN @@ -91355,7 +91355,7 @@ excluded middle (LEM), and in ILE the LEM is not accepted as necessarily ( C ^m ( A u. B ) ) ~~ ( ( C ^m A ) X. ( C ^m B ) ) ) $= ( vx wcel c0 wceq wa cun cmap co cres cop cvv ovexd wf elmapi w3a cin cxp vy cv c1st cfv c2nd xpexd ssun1 fssres sylancl ssun2 opelxp simpl3 simpl1 - wss jca elmapd simpl2 anbi12d syl5bb syl5ibr xp1st adantl syl xp2nd fun2d + wss jca elmapd simpl2 anbi12d bitrid syl5ibr xp1st adantl syl xp2nd fun2d simplr unexg syl2anc sylibrd 1st2nd2 ad2antll adantrl res0 eqtr4i reseq2d ex wb 3eqtr4a fresaunres1 syl3anc opeq12d eqtr4d reseq1 eqeq2d syl5ibrcom fresaunres2 wfn ffn fnresdm 3syl ad2antrl eqcomd vex resex op1std uneq12d @@ -92653,7 +92653,7 @@ Finite sets (cont.) 10.32 of [TakeutiZaring] p. 92. (Contributed by NM, 26-Jul-2004.) $) onfin $p |- ( A e. On -> ( A e. Fin <-> A e. _om ) ) $= ( vx cfn wcel cv cen wbr wrex con0 isfi wa wceq onomeneq wi eleq1a adantl - com sylbid rexlimdva enrefg breq2 rspcev mpdan impbid1 syl5bb ) ACDABEZFG + com sylbid rexlimdva enrefg breq2 rspcev mpdan impbid1 bitrid ) ACDABEZFG ZBQHZAIDZAQDZBAJUIUHUJUIUGUJBQUIUFQDZKUGAUFLZUJAUFMUKULUJNUIUFQAOPRSUJAAF GZUHAQTUGUMBAQUFAAFUAUBUCUDUE $. $} @@ -93340,7 +93340,7 @@ Finite sets (cont.) fimaxg $p |- ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A ( x =/= y -> y R x ) ) $= ( wor cfn wcel c0 wne w3a cv wbr wi wral wrex wn fimax2g wb wa weq imbi1i - df-ne pm4.64 bitri sotric con2bid syl5bb anassrs ralbidva rexbidva mpbird + df-ne pm4.64 bitri sotric con2bid bitrid anassrs ralbidva rexbidva mpbird wo 3ad2ant1 ) CDEZCFGZCHIZJAKZBKZIZURUQDLZMZBCNZACOZUQURDLZPZBCNZACOZABCD QUNUOVCVGRUPUNVBVFACUNUQCGZSVAVEBCUNVHURCGZVAVERVAABTZUTULZUNVHVISSZVEVAV JPZUTMVKUSVMUTUQURUBUAVJUTUCUDVLVDVKCUQURDUEUFUGUHUIUJUMUK $. @@ -93819,7 +93819,7 @@ Axiom of Infinity (see comments in ~ fin2inf ). (Contributed by NM, fodomfib $p |- ( A e. Fin -> ( ( A =/= (/) /\ E. f f : A -onto-> B ) <-> ( (/) ~< B /\ B ~<_ A ) ) ) $= ( cfn wcel c0 wne cv wfo wex wa csdm wbr cdom cdm wceq eqeq1d cvv 0sdomg - ex fof fdmd dm0rn0 forn syl5bb bitr3d necon3bid biimpac adantll eqeltrrdi + ex fof fdmd dm0rn0 forn bitrid bitr3d necon3bid biimpac adantll eqeltrrdi crn wb vex rnex adantl syl adantlr mpbird wi fodomfi jcad exlimdv expimpd adantr sdomdomtr syl5ib fodomr jca2 impbid ) ADEZAFGZABCHZIZCJZKFBLMZBANM ZKZVJVKVNVQVJVKKZVMVQCVRVMVOVPVRVMVOVRVMKVOBFGZVKVMVSVJVMVKVSVMAFBFVMVLOZ @@ -93841,7 +93841,7 @@ Axiom of Infinity (see comments in ~ fin2inf ). (Contributed by NM, wss nelne1 necomd df-pss php3 sdomentr nsyl3 cres difss ssfi fssres sylan foelrn simprll simprrr eldifsn simprrl eqcomd rspceeqv fveqeq2 syl5ibrcom fveq2 rexbidv imp eqid mpan2 sylbir adantll pm2.61dane fvres eqeq2d eqeq1 - rexbiia syl5bb rexlimdva syldan ralrimiva dffo3 fodomfi expr necon1bd mpd + rexbiia bitrid rexlimdva syldan ralrimiva dffo3 fodomfi expr necon1bd mpd anassrs ex ralrimivva dff13 df-f1o ) ABCUAZABUBIZBJKZUCZABCUDZXOABCUEXRAB CUFZDLZCMZELZCMZNZDEUGZUHZEAUIDAUIXSXRXOXTXOXPXQUJZABCUKULZXRYGDEAAXRYAAK ZYCAKZOZOZYEYFYMYEOZBAYCUMZUNZUQIZUOYFYQYPBURIZYNBYPUPYNYPAURIZXPYRYNAJKZ @@ -94202,7 +94202,7 @@ of Infinity (see comments in ~ fin2inf ). (Contributed by NM, fipreima $p |- ( ( F Fn B /\ A C_ ran F /\ A e. Fin ) -> E. c e. ( ~P B i^i Fin ) ( F " c ) = A ) $= ( vf vx vy wfn crn wss cfn wcel cv cfv wceq wral wa cima syl2anc ad2antrl - w3a wf cpw cin wrex wex simp3 dfss3 fvelrnb ralbidv syl5bb biimpa 3adant3 + w3a wf cpw cin wrex wex simp3 dfss3 fvelrnb ralbidv bitrid biimpa 3adant3 fveqeq2 ac6sfi fimass imaex elpw sylibr wfun ffun simpl3 imafi elind ccom vex cid cres fvco3 fvresi adantl eqeq12d ralbidva biimprd impr simpl1 ffn wi wb frn fnco syl3anc fnresi eqfnfv sylancl mpbird imaeq1d imaco resiima @@ -95661,7 +95661,7 @@ all reals (greatest real number) for which all positive reals are greater. supub $p |- ( ph -> ( C e. B -> -. sup ( B , A , R ) R C ) ) $= ( vw cv wbr wn wral wcel wi syl wceq notbid csup crab wrex wa a1i ss2rabi simpl crio supval2 wreu supeu riotacl2 eqeltrd sselid breq2 breq1 ralbidv - cbvralvw syl5bb elrab simprbi rspccv ) AFEHUAZKLZHMZNZKFOZGFPVCGHMZNZQAVC + cbvralvw bitrid elrab simprbi rspccv ) AFEHUAZKLZHMZNZKFOZGFPVCGHMZNZQAVC BLZCLZHMZNZCFOZBEUBZPZVGAVNVKVJHMVKDLHMDFUCQCEOZUDZBEUBZVOVCVRVNBEVRVNQVJ EPVNVQUGUEUFAVCVRBEUHZVSABCDEFHIUIAVRBEUJVTVSPABCDEFHIJUKVRBEULRUMUNVPVCE PVGVNVGBVCEVNVJVDHMZNZKFOVJVCSZVGVMWBCKFVKVDSVLWAVKVDVJHUOTURWCWBVFKFWCWA @@ -96028,7 +96028,7 @@ all reals (greatest real number) for which all positive reals are greater. infglb $p |- ( ph -> ( ( C e. A /\ inf ( B , A , R ) R C ) -> E. z e. B z R C ) ) $= ( wcel cinf wbr cv wrex wa wb wor brcnvg cvv ccnv csup df-inf simpr cnvso - breq1i sylib infcllem adantr bicomd syl2anc syl5bb suplub expdimp sylancl + breq1i sylib infcllem adantr bicomd syl2anc bitrid suplub expdimp sylancl supcl vex rexbidv sylibd sylbid expimpd ) AGEKZFEHLZGHMZDNZGHMZDFOZAVBPZV DGFEHUAZUBZVIMZVGVDVJGHMZVHVKVCVJGHFEHUCUFVHVBVJEKZVLVKQAVBUDZAVMVBABCDEF VIAEHREVIRIEHUEUGZABCDEFHIJUHZUPUIVBVMPVKVLGVJEEHSUJUKULVHVKGVEVIMZDFOZVG @@ -96041,7 +96041,7 @@ all reals (greatest real number) for which all positive reals are greater. ( inf ( B , A , R ) R C <-> E. z e. B z R C ) ) $= ( cinf wbr wcel wa wrex wb wor brcnvg cvv ccnv csup df-inf breq1i simpr cv cnvso sylib infcllem supcl adantr bicomd syl2anc suplub2 vex sylancl - rexbidv 3bitrd syl5bb ) FEHLZGHMFEHUAZUBZGHMZAGENZOZDUFZGHMZDFPZUTVBGHF + rexbidv 3bitrd bitrid ) FEHLZGHMFEHUAZUBZGHMZAGENZOZDUFZGHMZDFPZUTVBGHF EHUCUDVEVCGVBVAMZGVFVAMZDFPVHVEVDVBENZVCVIQAVDUEZAVKVDABCDEFVAAEHREVARI EHUGUHZABCDEFHIJUIZUJUKVDVKOVIVCGVBEEHSULUMABCDEFGVAVMVNKUNVEVJVGDFVEVD VFTNVJVGQVLDUOGVFETHSUPUQURUS $. @@ -96125,7 +96125,7 @@ all reals (greatest real number) for which all positive reals are greater. E. x e. A A. y e. A ( x =/= y -> x R y ) ) $= ( wor cfn wcel c0 wne w3a cv wbr wi wral wrex wn fimin2g wb wa weq imbi1i wo nesym pm4.64 sotric ancom2s con2bid anassrs ralbidva rexbidva 3ad2ant1 - bitri syl5bb mpbird ) CDEZCFGZCHIZJAKZBKZIZURUSDLZMZBCNZACOZUSURDLZPZBCNZ + bitri bitrid mpbird ) CDEZCFGZCHIZJAKZBKZIZURUSDLZMZBCNZACOZUSURDLZPZBCNZ ACOZABCDQUOUPVDVHRUQUOVCVGACUOURCGZSVBVFBCUOVIUSCGZVBVFRVBBATZVAUBZUOVIVJ SSZVFVBVKPZVAMVLUTVNVAURUSUCUAVKVAUDULVMVEVLUOVJVIVEVLPRCUSURDUEUFUGUMUHU IUJUKUN $. @@ -96135,7 +96135,7 @@ all reals (greatest real number) for which all positive reals are greater. fiinfg $p |- ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> E. x e. A ( A. y e. A -. y R x /\ A. y e. A ( x R y -> E. z e. A z R y ) ) ) $= ( wor cfn wcel c0 wne cv wbr wi wral wrex wn wa weq ex anassrs w3a fiming - equcom sotrieq2 ancom2s syl5bb simprbda a1dd pm2.27 soasym syl9r ralimdva + equcom sotrieq2 ancom2s bitrid simprbda a1dd pm2.27 soasym syl9r ralimdva wb pm2.61dne breq1 rspcev ralrimivw adantl jctird reximdva 3ad2ant1 mpd ) DEFZDGHZDIJZUAAKZBKZJZVFVGELZMZBDNZADOZVGVFELPZBDNZVICKZVGELZCDOZMZBDNZQZ ADOZABDEUBVCVDVLWAMVEVCVKVTADVCVFDHZQZVKVNVSWCVJVMBDWCVGDHZQZVJVMMVFVGWEA @@ -96420,7 +96420,7 @@ all reals (greatest real number) for which all positive reals are greater. ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) ) ) = F $= ( cv wral crecs cvv wbr crn crab crio cmpt wceq weq breq1 notbid cbvralvw - breq2 ralbidv syl5bb cbvriotavw cbvrabv eqtri rneq raleqdv rabbidv eqtrid + breq2 ralbidv bitrid cbvriotavw cbvrabv eqtri rneq raleqdv rabbidv eqtrid wn riotaeqbidv cbvmptv recseq ax-mp eqtr2i ) LMUAZHUBOSZNSZGUCZVCZOJSZASZ GUCZJHSZUDZTZAEUEZTZNVTUFZUGZUAZPMWCUHVIWDUHMIUBDSZCSZGUCZVCZDFTZCFUFZUGW CRIHUBWJWBIHUIZWJVMOFTZNFUFWBWIWLCNFWIVJWFGUCZVCZOFTCNUIZWLWHWNDOFDOUIWGW @@ -96461,7 +96461,7 @@ all reals (greatest real number) for which all positive reals are greater. elin2d syl cvv word wb wlim wfun tfr1a simpri limord ax-mp ordelord tfr2b sylancr mpbid crn rneq df-ima eqtr4di raleqdv rabbidv riotaeqbidv riotaex eqtrid fvmpt eqtrd wreu wwe wse wss c0 wne adantr ssrab2 wrex elin1d con0 - imaeq2 rexbidv elrab2 simprbi breq1 cbvralvw breq2 syl5bb cbvrexvw sylibr + imaeq2 rexbidv elrab2 simprbi breq1 cbvralvw breq2 bitrid cbvrexvw sylibr a1i ralbidv rabn0 wereu2 syl22anc riotacl2 eqeltrd ) APKNUEZUFUGZUHZPNUIZ FUJEUJJUKULZFMUJZDUJZJUKZMNPUMZUNZDHUOZUNZEYEUPZYFEYEUOZXQXRNPUQZOUIZYGXQ PXOUGZXRYJURXQKXOPAXPUSZVAZPNORUTVBXQYIVCUGZYJYGURXQYKYNYMXQPVDZYKYNVEXQX @@ -96582,7 +96582,7 @@ all reals (greatest real number) for which all positive reals are greater. cv wcel wa cfv wbr wrex wral cima word ordtypelem2 ordirr syl con0 wlim wn wfun tfr1a simpri limord ax-mp cres ordtypelem1 elexd eqeltrrd tfr2b mpbird ordelon sylancr imaeq2 raleqdv rexbidv crab breq1 cbvralvw breq2 - ralbidv syl5bb cbvrexvw cbvrabv eqtri elrab2 baib mtbid ralnex r19.21bi + ralbidv bitrid cbvrexvw cbvrabv eqtri elrab2 baib mtbid ralnex r19.21bi cvv sylibr rneqd df-ima eqtr4di adantr ffund funfnd ralrn bitr3d rexnal wfn ordtypelem7 ord rexlimdva mpd eqelssd isoeq5 mpbid ) APUJZPUKZULJPU MZYDHULJPUMZABCDEFGHIJKLMNOPRSTUAUBUCUDUNAYEHUOYFYGUPAUFYEHAKNUJZUQZHPA @@ -96809,7 +96809,7 @@ all reals (greatest real number) for which all positive reals are greater. eqsstrrid eqssd sseq1d reseq2d sqxpeqd difeq1 difun2 ineq1i 3eqtr3i weeq2 3anbi123d eqtrdi bitrd oieq1 oieq2 eqtrd dmeqd eqeq2d spcev syl21anc dmex brdomi simpr oion eqeltrdi simplr sylancr eqbrtrd simpll1 endomtr syl2an2 - oien ssdomg jca impbid2 syl5bb abbi2dv eqtr4id 3pm3.2i ) IUAZFFUBZUCZOIUD + oien ssdomg jca impbid2 bitrid abbi2dv eqtr4id 3pm3.2i ) IUAZFFUBZUCZOIUD ZFJUEZIUFZAUGZFUHUIZAUJUKZPVPUWMLUGZUAZFOZQUXCULZUXBOZUXBUXCUXCUBZOZUMZUX CUXBQUNZUOZRZBUGZUXCUXJUPZUAZPZRZBUQZLURZUWOUWMUXQLBUSZUAUXSIUXTMUTUXQLBV AVBUXRLUWOUXQUXBUWOUEZBUXIUYAUXKUXPUXIUXBUWNOUYAUXIUXBUXGUWNUXDUXFUXHVCUX @@ -96883,7 +96883,7 @@ all reals (greatest real number) for which all positive reals are greater. wofib $p |- ( ( R Or A /\ A e. Fin ) <-> ( R We A /\ `' R We A ) ) $= ( vz vy wor cfn wcel wa wwe ccnv wofi jca adantr com wss cep wbr wn cvv cnvso sylanb weso coi cdm cv wral wrex csuc peano2 sucidg wceq brcnv epel - vex bitri eleq2 syl5bb rspcev syl2anc dfrex2 sylib nrex word wb eqid oicl + vex bitri eleq2 bitrid rspcev syl2anc dfrex2 sylib nrex word wb eqid oicl ordom ordtri1 mp2an wfr c0 wne con0 oion mp1i simpr ssexd wiso oiiso mpan isocnv2 wefr isofr biimpar syl2an c1o 1onn ne0i fri syl22anc syl5bir mt3i ex ssid ssnnfi sylancl cen simpl oien sylancr enfi syl mpbid impbii ) ABF @@ -97016,7 +97016,7 @@ all reals (greatest real number) for which all positive reals are greater. wemapsolem $p |- ( ph -> T Or U ) $= ( cmap co wss wpo wor sopo syl wemappo syl2anc poss mpsyl wcel wceq wbr cv wa wo w3o wn wne df-ne cfv wi wral wrex cdif cdm crab wfn wf simprll - sselid elmapi simprlr fndmdif eleq2d nesym eqeq12d notbid syl5bb bitrdi + sselid elmapi simprlr fndmdif eleq2d nesym eqeq12d notbid bitrid bitrdi ffnd fveq2 imbi1d impexp con34b imbi2i bitr4i ralbidv2 anbi12d rexbidv2 elrab anass ad2antrr ffvelrnda sotrieq con2bid syl12anc anim1d reximdva mpbid biimprd mpd cvv wemaplem1 el2v orbi12i r19.43 andir ralbii anbi2i @@ -97069,7 +97069,7 @@ all reals (greatest real number) for which all positive reals are greater. co cdif cdm cfn csupp cun wfr wss c0 wn wral simprll breq1 elrab2 simprbi wrex syl simprlr fsuppunfi cfv crab wceq wf sselid elmapi fndmdif syl2anc wfn ffnd wi wo neneor elun simpr cvv wb adantr 3ad2ant1 ad2antrr elsuppfn - elex syl3anc mpbirand simpll1 orbi12d syl5bb syl5ibr rabss sylibr eqsstrd + elex syl3anc mpbirand simpll1 orbi12d bitrid syl5ibr rabss sylibr eqsstrd ralrimiva ssfid wwe suppssdm fssdm unssd soss sylc wofi simprr fndmdifeq0 wefr necon3bid mpbird fri syl22anc wemapsolem ) EKQZEGUDZFHUDZUEZMLQZRZAB CDEFGHIJUAUBPUCNASZMTUFZAFEUGULZJOUHZXSXTYAYCUIZXSXTYAYCUJYDUASZJQZUBSZJQ @@ -98537,7 +98537,7 @@ of all inductive sets (which is the smallest inductive set, since wbr cmpt crn wral csuc wfr omex mptex rnex zfregfr ssid dmmptg fvexd mprg wss cdm peano1 ne0ii eqnetri dm0rn0 necon3bii mpbi fri wfn wb eqid fnmpti mp4an fvelrnb peano2 fveq2 fvmpt syl fnfvelrn sylancr eqeltrrd epel eleq1 - syl5bb notbid df-nel bitr4di rspccv syl5com eqeq1 syl5ibcom neleq2 biimpd + bitrid notbid df-nel bitr4di rspccv syl5com eqeq1 syl5ibcom neleq2 biimpd wel syl6 com23 syldc reximdvai syl5bi com12 rexlimiv ) CFZDFZGUAZHZCEIEFZ BJZUBZUCZUDZDXDKZAFZUEZBJZXGBJZLZAIKZXDMNXDGUFXDXDUOXDOPZXFXCEIXBUGUHUIXD UJXDUKXCUPZOPXMXNIOXBMNXNIQEIEIXBMULXAINXABUMUNOIUQURUSXNOXDOXCUTVAVBDCXD @@ -99578,7 +99578,7 @@ a Cantor normal form (and injectivity, together with coherence cantnfs we0 oien mp2an en0 mpbi fveq2i seqom0g wfn ffnd fnfvelrn eqeltrrd eqtrdi pm2.61ne sylbid ex com23 syl5bi tfis2 com3l mpdd ssrdv eqssd dffo2 sylanbrc eleq12d imbi1d cbvrexvw eleq12 syl2an eqeqan12d rexbidv cbvopabv - a2i syl5bb simprll simprlr simprr cantnflem1 fvex epeli sylibr ralrimivva + a2i bitrid simprll simprlr simprr cantnflem1 fvex epeli sylibr ralrimivva soisoi syl22anc ) AHIUJFGUKOZPULZHUWRFGUOOZUMZUAQZUBQZIUNZUXBUWTRZUXCUWTR ZPUNZUPZUBHUQUAHUQHUWRIPUWTURABCDEFGHIJKLMUSAUWRUTZUWRPVAUWRPUJUWSAUWRVBS ZUXIAFVBSZGVBSZUXJKLFGVCVDZUWRVEVFZUWRVGUWRPVHUWRPVIVJAHUWRUWTWBZUWTVKZUW @@ -100534,7 +100534,7 @@ a Cantor normal form (and injectivity, together with coherence unieq ordunisuc wse csn df1o2 0ex ralsn cbvralvw cbvexvw cbvalvw pm3.2i cres 1on onordi ifbid ax-mp mp2an biantrurd brres df-3an breq12 pm5.32i mp2b 1n0 19.41v fveq1i setlikespec rdg0g 3bitr4d eliun df-rex elv anbi1 - crdg bitr4id alexbii 3ad2ant3 syl5bb con0 nnon ttrclselem1 dfse3 biimpi + crdg bitr4id alexbii 3ad2ant3 bitrid con0 nnon ttrclselem1 dfse3 biimpi wss ssralv sylc adantrr iunexg sylancr nfmpt1 nfrdg nfcxfr nffv predeq3 nfiun cbviunv iuneq1 rdgsucmptf syl2an2r simpr2r simplr3 simpr2l simpr3 eqbrtrrd breq2 syl2anc simp22r 3eqtrd simpl3 simp22l elnn sylan2 simp23 @@ -100654,7 +100654,7 @@ a Cantor normal form (and injectivity, together with coherence ttrclse $p |- ( R Se A -> t++ ( R |` A ) Se A ) $= ( vx vb vw vy vn vf va wse cv cpred cvv wcel wral wa com cfv csuc wb cres cttrcl ciun cmpt crdg cima cuni wbr wrex wfn c0 wceq brttrcl2 ttrclselem2 - w3a wex eqid ancoms rexbidva syl5bb vex elpred elv resdmss breldm dmttrcl + w3a wex eqid ancoms rexbidva bitrid vex elpred elv resdmss breldm dmttrcl 3expb cdm eleqtrdi sselid pm4.71ri bitr4i wfun rdgfun ax-mp 3bitr4g eqrdv eluniima omex funimaex uniex eqeltrdi ralrimiva dfse3 sylibr ) ABJZABAUAZ UBZCKZLZMNZCAOAWHJWFWKCAWFWIANZPZWJDMEDKABEKLUCUDZABWILZUEZQUFZUGZMWMFWJW @@ -102792,7 +102792,7 @@ suc suc ( ( rank ` A ) u. ( rank ` B ) ) $= rankbnd2 $p |- ( B e. On -> ( A. x e. A ( rank ` x ) C_ B <-> ( rank ` A ) C_ suc B ) ) $= ( cv crnk cfv wss wral cuni con0 wcel csuc rankuni rankuni2 eqtr3i sseq1i - ciun iunss bitr2i word wb rankon onssi eloni ordunisssuc sylancr syl5bb ) + ciun iunss bitr2i word wb rankon onssi eloni ordunisssuc sylancr bitrid ) AEFGZCHABIZBFGZJZCHZCKLZUKCMHZUMABUIRZCHUJULUPCBJFGULUPBNABDOPQABUICSTUNU KKHCUAUMUOUBUKBUCUDCUEUKCUFUGUH $. @@ -104305,7 +104305,7 @@ _Cardinal Arithmetic_ (1994), p. xxx (Roman numeral 30). See ~ cfval domtri2 $p |- ( ( A e. dom card /\ B e. dom card ) -> ( A ~<_ B <-> -. B ~< A ) ) $= ( ccrd cdm wcel wa cfv wss cdom wbr csdm wn carddom2 wb cardon ontri1 mp2an - con0 cardsdom2 ancoms notbid syl5bb bitr3d ) ACDZEZBUDEZFZACGZBCGZHZABIJBAK + con0 cardsdom2 ancoms notbid bitrid bitr3d ) ACDZEZBUDEZFZACGZBCGZHZABIJBAK JZLZABMUJUIUHEZLZUGULUHREUIREUJUNNAOBOUHUIPQUGUMUKUFUEUMUKNBASTUAUBUC $. $( $j usage 'domtri2' avoids 'ax-ac' 'ax-ac2'; $) @@ -104908,7 +104908,7 @@ x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( Y o. `' X ) ) ) ) $. vx vy vz cdif wrex wi wral c2o cxp cnfcom3c cen wbr comu df-2o oveq2i 1on csuc oesuc mp2an oe1 ax-mp oveq1i 3eqtri omxpen eqbrtri xpomen entri bren a1i sylib exdistrv cid ccnv cpr cres cop cun ccom cmpt simpl simprl sseq2 - oveq2 f1oeq3d cbvrexvw fveq2 f1oeq1d f1oeq2 bitrd rexbidv syl5bb cbvralvw + oveq2 f1oeq3d cbvrexvw fveq2 f1oeq1d f1oeq2 bitrd rexbidv bitrid cbvralvw crn imbi12d cbvmptv cnveqi fveq1i peano1 oen0 mpan2 eqid fveqf1o ad2antll 2on mp3an23 simpld simprd infxpenc2lem3 ex exlimdvv syl5bir mp2and ) AGHZ IUBJZUAZXOIUCJZKLZXODJZMZNZUCGOUEZUFZUGZUBAUHZDPZIUIKLZIEJZNZEPZICJZUAZYK @@ -105042,7 +105042,7 @@ x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( Y o. `' X ) ) ) ) $. ( vx vy wcel com cv cmap co cvv cxp c1st cfv csuc c2nd csn wa wb wceq wbr ciun cdom omex iunex xp1st peano2 syl xp2nd fconst6g adantl elmapg sylan2 ovex wf mpbird oveq2 eliuni syl2an2 ex weq wi wne nsuceq0 fvex snnz mp2an - xp11 peano4 syl2an sneqbg mp1i anbi12d syl5bb xpopth bitrd a1i dom2d mpi + xp11 peano4 syl2an sneqbg mp1i anbi12d bitrid xpopth bitrd a1i dom2d mpi c0 ) ACFZBGABHZIJZUBZKFGALZWDUCUABGWCUDAWBIUNUEWADEWEWDDHZMNZOZWFPNZQZLZE HZMNZOZWLPNZQZLZKWAWFWEFZWKWDFZWRWHGFZWAWKAWHIJZFZWSWRWGGFZWTWFGAUFZWGUGU HZWAWRRXBWHAWKUOZWRXFWAWRWIAFXFWFGAUIWHWIAUJUHUKWRWAWTXBXFSXEAWHWKCGULUMU @@ -105328,7 +105328,7 @@ x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( Y o. `' X ) ) ) ) $. acni2 $p |- ( ( X e. AC_ A /\ A. x e. A ( B C_ X /\ B =/= (/) ) ) -> E. g ( g : A --> X /\ A. x e. A ( g ` x ) e. B ) ) $= ( vy vf wcel c0 wa wral cv cfv cmpt wex wf wceq fveq2 cvv eleq1d elpw2g - wacn wss wne cpw csn cdif eldifsn anbi1d syl5bb ralbidv eqid fmpt sylib + wacn wss wne cpw csn cdif eldifsn anbi1d bitrid ralbidv eqid fmpt sylib biimpar acni syldan nffvmpt1 nfel2 nfv eleq12d cbvralw simplr wb simpll simpr ssexd fvmpt2 syl2anc eleq2d adantrd ralimdva imp ralbi syl biimpa ex wi ssel adantr ral2imi sylc rspccva sylan fmpttd acnrcl fex2 syl3anc @@ -106739,7 +106739,7 @@ our Axiom of Choice (in the form of ~ ac2 ). The proof does not depend raleq ad2antlr fvelrn adantlr eleq1 syl5ibcom necon3bd mpd neeq1 fveq2 id eleq12d simplr rspcdva ralrimiva wb dmex mptelixpg sylibr ne0d ex exlimdv ad4ant14 syl5com alrimiv csn cdif cid cres fnresi neldifsn difexi resiexg - wfn fnfun funeq rnresi eqtrdi eleq2d notbid syl5bb anbi12d dmresi ixpeq1d + wfn fnfun funeq rnresi eqtrdi eleq2d notbid bitrid anbi12d dmresi ixpeq1d rneq fveq1 fvresi sylan9eq ixpeq2dva eqtrd neeq1d mp2ani n0 elixp eldifsn dmeq imbi1i impexp bitri ralbii2 cbvralvw simplbiim eximi sylbi impbii syl ) UACFZGHZYADFZIZYAJZKZCEFZLZDMZEUBZBFZUCZGYKUDZUEZTZAYKUFZAFZYKIZNZG @@ -108613,7 +108613,7 @@ _Cardinal Arithmetic_ (1994), p. xxx (Roman numeral 30). The cofinality wb cab cint cfval eqeq1d vex eqeq1 anbi1d exbidv elab fveq2 cardidm eqeq2 eqtrdi mpbird adantr exlimiv sylbi cardon eqeltrrdi ssriv onint0 0ex onss ax-mp w3a ancoms sylan 3adant2 3adant3r simp2 simp3 eqcom cdm cvv onssnum - sstr mpan cardnueq0 syl syl5bb biimpa sseq1 rexeq ralbidv anbi12d wn rex0 + sstr mpan cardnueq0 syl bitrid biimpa sseq1 rexeq ralbidv anbi12d wn rex0 rgenw r19.2z mpan2 rexnal sylib necon4ai simpl2im syl21anc 3expib exlimdv wne syl5bi sylbid cf0 impbid1 ) AGHZAIJZKLZAKLZXCXEBMZCMZNJZLZXHAOZDMEMOZ EXHPZDAQZRZRZCSZBUAZUBZKLZXFXCXDXSKBCDEAUCUDXTKXRHZXCXFXRGOXTYATFXRGFMZXR @@ -108638,7 +108638,7 @@ _Cardinal Arithmetic_ (1994), p. xxx (Roman numeral 30). The cofinality cint wo wi eqimss a1i jaod syl5 sseq2 rspcev syl6an ralrimiv ssun2 df-suc cun sseqtrri jctil fveq2 eqeq2d sseq1 rexeq ralbidv anbi12d spcev syl2anc snex 1oex eqeq1 anbi1d exbidv elab sylibr el1o eqcom cdm cvv onssnum mpan - wb vex cardnueq0 syl syl5bb biimpa rex0 wne nsuceq0 r19.2z mtbiri intnand + wb vex cardnueq0 syl bitrid biimpa rex0 wne nsuceq0 r19.2z mtbiri intnand nrex mto imnan mpbi w3a suceloni onss sylan2 ancoms adantrr 3adant2 simp2 sstr simp3 jca31 3expib mtoi nexdv 0ex sylnibr adantr eleq1 adantl mtbird sylan2b ralrimiva cardon mpbiri exlimiv abssi oneqmini ax-mp eqtr4d ) AGH @@ -108751,7 +108751,7 @@ _Cardinal Arithmetic_ (1994), p. xxx (Roman numeral 30). The cofinality Carneiro, 28-Feb-2013.) $) cflim3 $p |- ( Lim A -> ( cf ` A ) = |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) ) $= - ( vy vz vw wlim ccf cfv cv ccrd wceq wss wrex wa wex cab cint wcel syl5bb + ( vy vz vw wlim ccf cfv cv ccrd wceq wss wrex wa wex cab cint wcel bitrid wral cuni crab ciin con0 word limord elon sylibr cfval fvex dfiin2 df-rex cpw ancom rabid velpw anbi1i coflim pm5.32da anbi2d exbidv abbidv eqtr2id syl inteqd eqtrd ) BGZBHIZDJAJZKIZLZVJBMZEJFJMFVJNEBUAZOZOZAPZDQZRZAVJUBB