diff --git a/changes-set.txt b/changes-set.txt index 1dbbb68cc..b62cf365d 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -92,6 +92,7 @@ make a github issue.) DONE: Date Old New Notes +19-Sep-25 bm1.3ii sepexi Generalized conclusion 10-Sep-25 soeq12d [same] Moved from SO's mathbox to main set.mm 10-Sep-25 freq12d [same] Moved from SO's mathbox to main set.mm 10-Sep-25 weeq12d [same] Moved from SO's mathbox to main set.mm diff --git a/discouraged b/discouraged index c5928aaef..48be77f2e 100644 --- a/discouraged +++ b/discouraged @@ -1731,6 +1731,9 @@ "axpowndlem2" is used by "axpowndlem3". "axpowndlem3" is used by "axpowndlem4". "axpowndlem4" is used by "axpownd". +"axprlem3OLD" is used by "axprOLD". +"axprlem4OLD" is used by "axprOLD". +"axprlem5OLD" is used by "axprOLD". "axregnd" is used by "axregprim". "axregnd" is used by "zfcndreg". "axregndlem1" is used by "axregnd". @@ -1905,6 +1908,7 @@ "blometi" is used by "blocni". "bloval" is used by "hhbloi". "bloval" is used by "isblo". +"bm1.3iiOLD" is used by "axprlem4OLD". "bnj1000" is used by "bnj965". "bnj1001" is used by "bnj1020". "bnj1006" is used by "bnj1020". @@ -13040,6 +13044,7 @@ "scandx" is used by "zlmlemOLD". "scandx" is used by "zlmtsetOLD". "selsALT" is used by "elALT". +"sepexlem" is used by "sepex". "setrec1lem1" is used by "setrec1lem2". "setrec1lem1" is used by "setrec1lem4". "setrec1lem1" is used by "setrec2fun". @@ -14947,14 +14952,20 @@ New usage of "axpowndlem3" is discouraged (1 uses). New usage of "axpowndlem4" is discouraged (1 uses). New usage of "axpr" is discouraged (0 uses). New usage of "axprALT" is discouraged (0 uses). +New usage of "axprOLD" is discouraged (0 uses). New usage of "axpre-ltadd" is discouraged (0 uses). New usage of "axpre-lttri" is discouraged (0 uses). New usage of "axpre-lttrn" is discouraged (0 uses). New usage of "axpre-mulgt0" is discouraged (0 uses). New usage of "axpre-sup" is discouraged (0 uses). +New usage of "axprlem3OLD" is discouraged (1 uses). +New usage of "axprlem4OLD" is discouraged (1 uses). +New usage of "axprlem5OLD" is discouraged (1 uses). New usage of "axregnd" is discouraged (2 uses). New usage of "axregndlem1" is discouraged (2 uses). New usage of "axregndlem2" is discouraged (1 uses). +New usage of "axrep4OLD" is discouraged (0 uses). +New usage of "axrep6OLD" is discouraged (0 uses). New usage of "axrepnd" is discouraged (2 uses). New usage of "axrepndlem1" is discouraged (1 uses). New usage of "axrepndlem2" is discouraged (1 uses). @@ -15056,6 +15067,7 @@ New usage of "blof" is discouraged (5 uses). New usage of "bloln" is discouraged (6 uses). New usage of "blometi" is discouraged (1 uses). New usage of "bloval" is discouraged (2 uses). +New usage of "bm1.3iiOLD" is discouraged (1 uses). New usage of "bnj1000" is discouraged (1 uses). New usage of "bnj1001" is discouraged (1 uses). New usage of "bnj1006" is discouraged (1 uses). @@ -19263,6 +19275,7 @@ New usage of "scmateALT" is discouraged (0 uses). New usage of "sdom0OLD" is discouraged (0 uses). New usage of "sdom1OLD" is discouraged (0 uses). New usage of "selsALT" is discouraged (1 uses). +New usage of "sepexlem" is discouraged (1 uses). New usage of "seq1hcau" is discouraged (0 uses). New usage of "setrec1lem1" is discouraged (3 uses). New usage of "setrec1lem2" is discouraged (1 uses). @@ -20066,6 +20079,12 @@ Proof modification of "axnul" is discouraged (36 steps). Proof modification of "axnulALT" is discouraged (95 steps). Proof modification of "axnulALT2" is discouraged (57 steps). Proof modification of "axprALT" is discouraged (67 steps). +Proof modification of "axprOLD" is discouraged (122 steps). +Proof modification of "axprlem3OLD" is discouraged (152 steps). +Proof modification of "axprlem4OLD" is discouraged (149 steps). +Proof modification of "axprlem5OLD" is discouraged (132 steps). +Proof modification of "axrep4OLD" is discouraged (130 steps). +Proof modification of "axrep6OLD" is discouraged (113 steps). Proof modification of "axsepg2ALT" is discouraged (170 steps). Proof modification of "barbariALT" is discouraged (22 steps). Proof modification of "barocoALT" is discouraged (24 steps). @@ -20316,6 +20335,7 @@ Proof modification of "bj-xpima1snALT" is discouraged (25 steps). Proof modification of "bj-xpima2sn" is discouraged (23 steps). Proof modification of "bj-xpnzex" is discouraged (71 steps). Proof modification of "bj-zfauscl" is discouraged (65 steps). +Proof modification of "bm1.3iiOLD" is discouraged (95 steps). Proof modification of "brdomgOLD" is discouraged (118 steps). Proof modification of "brdomiOLD" is discouraged (30 steps). Proof modification of "brenOLD" is discouraged (130 steps). diff --git a/set.mm b/set.mm index 6cf708df0..0ba196e8c 100644 --- a/set.mm +++ b/set.mm @@ -50480,12 +50480,39 @@ under a function is also a set (see the variant ~ funimaex ). Although $} ${ - $d x y z w $. + $d w x y z $. $d z ph $. + $( Version of ~ axrep4 with a disjoint variable condition, requiring fewer + axioms. (Contributed by Matthew House, 18-Sep-2025.) $) + axrep4v $p |- ( A. x E. z A. y ( ph -> y = z ) -> + E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) ) $= + ( wal weq wi wex wel wa wb ax-rep 19.3v imbi1i albii exbii anbi2i 3imtr3i + bibi2i ) ADFZCDGZHZCFZDIZBFCDJZBEJZUAKZBIZLZCFZDIAUBHZCFZDIZBFUFUGAKZBIZL + ZCFZDIAEDCBMUEUNBUDUMDUCULCUAAUBADNZOPQPUKURDUJUQCUIUPUFUHUOBUAAUGUSRQTPQ + S $. + $( $j usage 'axrep4v' avoids 'ax-12'; $) + $} + + ${ + $d w x y z $. axrep4.1 $e |- F/ z ph $. $( A more traditional version of the Axiom of Replacement. (Contributed by - NM, 14-Aug-1994.) $) + NM, 14-Aug-1994.) (Proof shortened by Matthew House, 18-Sep-2025.) $) axrep4 $p |- ( A. x E. z A. y ( ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) ) $= + ( wal weq wi wex wel wa wb ax-rep 19.3 imbi1i albii exbii anbi2i bibi2i + 3imtr3i ) ADGZCDHZIZCGZDJZBGCDKZBEKZUBLZBJZMZCGZDJAUCIZCGZDJZBGUGUHALZBJZ + MZCGZDJAEDCBNUFUOBUEUNDUDUMCUBAUCADFOZPQRQULUSDUKURCUJUQUGUIUPBUBAUHUTSRT + QRUA $. + $} + + ${ + $d x y z w $. + axrep4OLD.1 $e |- F/ z ph $. + $( Obsolete version of ~ axrep4 as of 18-Sep-2025. (Contributed by NM, + 14-Aug-1994.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + axrep4OLD $p |- ( A. x E. z A. y ( ph -> y = z ) -> + E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) ) $= ( weq wi wal wex wel wa wb axrep3 19.35i nfv nfa1 nfan nfbi nfal nfex a1i nfe1 elequ2 19.3 anbi2i exbii bibi12d albidv cbvexv1 sylib ) ACDGHCIDJZBI CBKZBEKZADIZLZBJZMZCIZBJCDKZUNALZBJZMZCIZDJULUSBABDCENOUSVDBDURDCUMUQDUMD @@ -50515,8 +50542,21 @@ under a function is also a set (see the variant ~ funimaex ). Although ${ $d w x y z $. $d y ph $. - $( A condensed form of ~ ax-rep . (Contributed by SN, 18-Sep-2023.) $) + $( A condensed form of ~ ax-rep . (Contributed by SN, 18-Sep-2023.) + (Proof shortened by Matthew House, 18-Sep-2025.) $) axrep6 $p |- ( A. w E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) ) $= + ( weq wi wal wex wel wa wb wmo cv wrex axrep4v df-mo albii df-rex bibi2i + exbii 3imtr4i ) ADCFGDHCIZEHDCJZEBJAKEIZLZDHZCIADMZEHUDAEBNZOZLZDHZCIAEDC + BPUHUCEADCQRULUGCUKUFDUJUEUDAEUISTRUAUB $. + $} + + ${ + $d w x y z $. $d y ph $. + $( Obsolete version of ~ axrep6 as of 18-Sep-2025. (Contributed by SN, + 18-Sep-2023.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + axrep6OLD $p |- ( A. w E* z ph -> E. y A. z ( z e. y <-> E. w e. x ph ) ) + $= ( wal weq wi wex wel wa wb wmo cv wrex ax-rep df-mo 19.3v albii exbii imbi1i bitr4i rexbii df-rex bitr3i bibi2i 3imtr4i ) ACFZDCGZHZDFZCIZEFDCJ ZEBJUHKEIZLZDFZCIADMZEFUMAEBNZOZLZDFZCIABCDEPUQULEUQAUIHZDFZCIULADCQUKVCC @@ -50685,13 +50725,48 @@ under a function is also a set (see the variant ~ funimaex ). Although IUBULUDUHAUCDUAMNOPQABCFRS $. $} + ${ + $d x y z $. $d y z ph $. + $( Lemma for ~ sepex . Use ~ sepex instead. (Contributed by Matthew + House, 19-Sep-2025.) (New usage is discouraged.) $) + sepexlem $p |- ( E. y A. x ( ph -> x e. y ) -> + E. z A. x ( x e. z <-> ph ) ) $= + ( wel wi wal wb wex wa ax-sep bimsc1 ex al2imi eximdv mpi exlimiv ) ABCEZ + FZBGZBDEZAHZBGZDIZCTUARAJHZBGZDIUDABDCKTUFUCDSUEUBBSUEUBARUALMNOPQ $. + $} + + ${ + $d x y w $. $d x z w $. $d y w ph $. $d z w ph $. + $( Convert implication to equivalence within an existence statement using + the Separation Scheme (Aussonderung) ~ ax-sep . Similar to Theorem + 1.3(ii) of [BellMachover] p. 463. (Contributed by Matthew House, + 19-Sep-2025.) $) + sepex $p |- ( E. y A. x ( ph -> x e. y ) -> + E. z A. x ( x e. z <-> ph ) ) $= + ( vw wel wi wal wex wb sepexlem biimpr alimi eximi 3syl ) ABCFGBHCIBEFZAJ + ZBHZEIAPGZBHZEIBDFAJBHDIABCEKRTEQSBPALMNABEDKO $. + $( $j usage 'sepex' avoids 'ax-9' 'ax-12'; $) + $} + + ${ + $d x y $. $d x z $. $d y ph $. $d z ph $. + sepexi.1 $e |- E. y A. x ( ph -> x e. y ) $. + $( Convert implication to equivalence within an existence statement using + the Separation Scheme (Aussonderung) ~ ax-sep . Inference associated + with ~ sepex . (Contributed by NM, 21-Jun-1993.) Generalize + conclusion, extract closed form, and avoid ~ ax-9 . (Revised by Matthew + House, 19-Sep-2025.) $) + sepexi $p |- E. z A. x ( x e. z <-> ph ) $= + ( wel wi wal wex wb sepex ax-mp ) ABCFGBHCIBDFAJBHDIEABCDKL $. + $} + ${ $d x ph z $. $d x y z $. - bm1.3ii.1 $e |- E. x A. y ( ph -> y e. x ) $. - $( Convert implication to equivalence using the Separation Scheme - (Aussonderung) ~ ax-sep . Similar to Theorem 1.3(ii) of [BellMachover] - p. 463. (Contributed by NM, 21-Jun-1993.) $) - bm1.3ii $p |- E. x A. y ( y e. x <-> ph ) $= + bm1.3iiOLD.1 $e |- E. x A. y ( ph -> y e. x ) $. + $( Obsolete version of ~ sepexi as of 18-Sep-2025. (Contributed by NM, + 21-Jun-1993.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + bm1.3iiOLD $p |- E. x A. y ( y e. x <-> ph ) $= ( vz wel wi wal wa wb wex 19.42v bimsc1 eximi sylbir elequ2 imbi2d albidv alanimi weq cbvexvw mpbi ax-sep exan exlimiiv ) ACEFZGZCHZCBFZUFAIJZCHZBK ZIZUIAJZCHZBKZEUMUHUKIZBKUPUHUKBLUQUOBUGUJUNCAUFUIMSNOUHULEAUIGZCHZBKUHEK @@ -51339,8 +51414,8 @@ holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc] i.e. the power set of ` x ` . Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) $) axpow3 $p |- E. y A. z ( z C_ x <-> z e. y ) $= - ( cv wss wel wb wal wex axpow2 bm1.3ii bicom albii exbii mpbir ) CDADEZCB - FZGZCHZBIQPGZCHZBIPBCABCJKSUABRTCPQLMNO $. + ( cv wss wel wb wal wex axpow2 sepexi bicom albii exbii mpbir ) CDADEZCBF + ZGZCHZBIQPGZCHZBIPCBBABCJKSUABRTCPQLMNO $. $} ${ @@ -51483,9 +51558,9 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove ~ pwexg from ~ vpwex . (Revised by BJ, 10-Aug-2022.) $) vpwex $p |- ~P x e. _V $= - ( vw vy vz cv cpw wss cab cvv df-pw wceq wex wel wal axpow2 bm1.3ii sseq1 - wb eqabbw exbii mpbir issetri eqeltri ) AEZFBEZUDGZBHZIBUDJCUGCEZUGKZCLDC - MDEZUDGZRDNZCLUKCDACDOPUIULCUFUKBDUHUEUJUDQSTUAUBUC $. + ( vw vy vz cv cpw wss cab cvv df-pw wceq wex wel wal axpow2 sepexi eqabbw + wb sseq1 exbii mpbir issetri eqeltri ) AEZFBEZUDGZBHZIBUDJCUGCEZUGKZCLDCM + DEZUDGZRDNZCLUKDCCACDOPUIULCUFUKBDUHUEUJUDSQTUAUBUC $. $( $j usage 'vpwex' avoids 'ax-10' 'ax-11' 'ax-12'; $) $} @@ -52034,7 +52109,7 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with ( vw wel wn wal wex ax-pow pm2.21 alimi a1i imim1d alimdv eximdv exlimiiv wi mpi ax-nul ) CDEZFCGZCBEZFZCGZBAEZQZBGZAHZDUAUBTQZCGZUEQZBGZAHUHDABCIU AULUGAUAUKUFBUAUDUJUEUDUJQUAUCUICUBTJKLMNORDCSP $. - $( $j usage 'axprlem1' avoids 'ax-ext' 'ax-sep'; $) + $( $j usage 'axprlem1' avoids 'ax-8' 'ax-9' 'ax-12' 'ax-ext' 'ax-sep'; $) $} ${ @@ -52047,78 +52122,129 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with alimdv eximdv mpi axprlem1 exlimiiv ) DCFGDHZCEFZIZCHZUDCBJZKZBAFZIZBHZAL ZEUGCBFZUEIZCHZUJIZBHZALUMEABCMUGURULAUGUQUKBUGUIUPUJUIUNUDIZCHUGUPUDCUHN UFUSUOCUDUEUNOPQRSTUAECDUBUC $. - $( $j usage 'axprlem2' avoids 'ax-ext' 'ax-sep'; $) + $( $j usage 'axprlem2' avoids 'ax-8' 'ax-9' 'ax-12' 'ax-ext' 'ax-sep'; $) $} ${ $d x z w $. $d y z w $. $d z w n $. $d z w s p $. $( Lemma for ~ axpr . Eliminate the antecedent of the relevant replacement - instance. (Contributed by Rohan Ridenour, 10-Aug-2023.) $) + instance. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Proof + shortened by Matthew House, 18-Sep-2025.) $) axprlem3 $p |- E. z A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $= + ( wel wex weq wif wi wal wa wb biimpd equeuclr syl9r alrimdv spimevw mpg + axrep4v ifptru wn ifpfal pm2.61i ) EFHEIZDAJZDBJZKZDCJZLZDMZCIZDCHFGHUJNF + IODMCIFUJFDCGUBUGUNUGUMCACAJZUGULDUGUJUHUOUKUGUJUHUGUHUIUCPCDAQRSTUGUDZUM + CBCBJZUPULDUPUJUIUQUKUPUJUIUGUHUIUEPCDBQRSTUFUA $. + $( $j usage 'axprlem3' avoids 'ax-8' 'ax-9' 'ax-12' 'ax-ext'; $) + $} + + ${ + $d w s $. $d v s $. + axprlem4.1 $e |- E. s A. n ph $. + axprlem4.2 $e |- ( ph -> ( n e. s -> A. t -. t e. n ) ) $. + axprlem4.3 $e |- ( A. n ph -> + ( if- ( E. n n e. s , w = x , w = y ) <-> w = v ) ) $. + $( Lemma for ~ axpr . If an existing set of empty sets corresponds to one + element of the pair, then the element is included in any superset of the + set whose existence is asserted by the axiom of replacement. + (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, + 13-Aug-2023.) (Revised by Matthew House, 18-Sep-2025.) $) + axprlem4 $p |- ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( w = v -> + E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) ) $= + ( wel wn wal cv wi wa wex weq wral wif alimi df-ral sylibr imim1i aleximi + ancrd mpi biimprcd anim2d eximdv syl5com ) FGMNFOZGHPZUAZHIMZQZHOZUQAGOZR + ZHSZDETZUQGHMZGSDBTDCTUBZRZHSUSUTHSVBJURUTVAHURUTUQUTUPUQUTVDUNQZGOUPAVGG + KUCUNGUOUDUEUFUHUGUIVCVAVFHVCUTVEUQUTVEVCLUJUKULUM $. + $( $j usage 'axprlem4' avoids 'ax-8' 'ax-9' 'ax-12' 'ax-ext'; $) + $} + + ${ + $d x z w s p $. $d y z w s p $. $d z w t n s p $. + $( Unabbreviated version of the Axiom of Pairing of ZF set theory, derived + as a theorem from the other axioms. + + This theorem should not be referenced by any proof. Instead, use + ~ ax-pr below so that the uses of the Axiom of Pairing can be more + easily identified. + + For a shorter proof using ~ ax-ext , see ~ axprALT . (Contributed by + NM, 14-Nov-2006.) Remove dependency on ~ ax-ext . (Revised by Rohan + Ridenour, 10-Aug-2023.) (Proof shortened by BJ, 13-Aug-2023.) (Proof + shortened by Matthew House, 18-Sep-2025.) Use ~ ax-pr instead. + (New usage is discouraged.) $) + axpr $p |- E. z A. w ( ( w = x \/ w = y ) -> w e. z ) $= + ( vt vn vs vp wel wn wal cv wral wi weq wo wex wb ax-nul axprlem4 wa exbi + wif axprlem3 axprlem1 sepexi biimp mpbiri ifptru pm2.21 alnex ifpfal jaod + syl sylbi imbi2 syl5ibrcom alimdv eximdv mpi axprlem2 exlimiiv ) EFIJEKZF + GLMGHIZNGKZDAOZDBOZPZDCIZNZDKZCQZHVEVIVDFGIZFQZVFVGUCZUAGQZRZDKZCQVLABCDF + GHUDVEVRVKCVEVQVJDVEVJVQVHVPNVEVFVPVGVMVCRZABDAEFGHVCFGGGFEUEUFVMVCUGVSFK + ZVNVOVFRVTVNVCFQFESVMVCFUBUHVNVFVGUIUNTVMJZABDBEFGHGFSVMVCUJWAFKVNJVOVGRV + MFUKVNVFVGULUOTUMVIVPVHUPUQURUSUTHGFEVAVB $. + $( $j usage 'axpr' avoids 'ax-8' 'ax-9' 'ax-10' 'ax-11' 'ax-12' + 'ax-ext'; $) + $} + + ${ + $d x z w $. $d y z w $. $d z w n $. $d z w s p $. + $( Obsolete version of ~ axprlem3 as of 18-Sep-2025. (Contributed by Rohan + Ridenour, 10-Aug-2023.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + axprlem3OLD $p |- E. z A. w ( w e. z <-> + E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $= ( cv wcel wex weq wi wal wa ax6evr biimpd alrimiv expcom eximdv mpi wb wn wif axrep4 ifptru equtrr sylan9r ifpfal adantl simpl equtr syl6ci pm2.61i nfv mpg ) EHFHZIEJZDAKZDBKZUCZDCKZLZDMZCJZDHCHIUPGHIUTNFJUADMCJFUTFDCGUTC UNUDUQVDUQACKZCJVDCAOUQVEVCCVEUQVCVEUQNVBDUQUTURVEVAUQUTURUQURUSUEPACDUFU GQRSTUQUBZBCKZCJVDCBOVFVGVCCVGVFVCVGVFNZVBDVHUTUSVGVAVFUTUSLVGVFUTUSUQURU SUHPUIVGVFUJDBCUKULQRSTUMUO $. - $( $j usage 'axprlem3' avoids 'ax-ext'; $) + $( $j usage 'axprlem3OLD' avoids 'ax-ext'; $) $} ${ $d x s $. $d w s $. $d t n s $. - $( Lemma for ~ axpr . The first element of the pair is included in any - superset of the set whose existence is asserted by the axiom of - replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by - BJ, 13-Aug-2023.) $) - axprlem4 $p |- ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = x ) - -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $= - ( wel wn wal cv wral wi weq wa wex nfa1 sp eximd mpi wif axprlem1 bm1.3ii - wb nfv nfan biimp alimi df-ral sylibr mpan9 adantrr ax-nul biimprd simprr - ifptru biimpar syl2an2r jca expcom ) DEHIDJZEFKZLZFGHZMZFJZCANZOZEFHZVAUD - ZEJZFPVDVIEPZVGCBNZUAZOZFPVAFEFEDUBUCVHVKVOFVFVGFVEFQVGFUEUFVKVHVOVKVHOVD - VNVKVFVDVGVKVCVFVDVKVIVAMZEJVCVJVPEVIVAUGUHVAEVBUIUJVEFRUKULVKVLVHVGVNVKV - AEPVLEDUMVKVAVIEVJEQVKVIVAVJERUNSTVKVFVGUOVLVNVGVLVGVMUPUQURUSUTST $. - $( $j usage 'axprlem4' avoids 'ax-ext'; $) + $( Obsolete version of ~ axprlem4 as of 18-Sep-2025. (Contributed by Rohan + Ridenour, 10-Aug-2023.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + axprlem4OLD $p |- ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) + /\ w = x ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $= + ( wel wn wal cv wral wi weq wa wex nfa1 sp eximd mpi wb wif axprlem1 nfan + bm1.3iiOLD biimp alimi df-ral sylibr adantrr ax-nul biimprd simprr ifptru + nfv mpan9 biimpar syl2an2r jca expcom ) DEHIDJZEFKZLZFGHZMZFJZCANZOZEFHZV + AUAZEJZFPVDVIEPZVGCBNZUBZOZFPVAFEFEDUCUEVHVKVOFVFVGFVEFQVGFUOUDVKVHVOVKVH + OVDVNVKVFVDVGVKVCVFVDVKVIVAMZEJVCVJVPEVIVAUFUGVAEVBUHUIVEFRUPUJVKVLVHVGVN + VKVAEPVLEDUKVKVAVIEVJEQVKVIVAVJERULSTVKVFVGUMVLVNVGVLVGVMUNUQURUSUTST $. + $( $j usage 'axprlem4OLD' avoids 'ax-ext'; $) $} ${ $d y s $. $d w s $. $d n s $. - $( Lemma for ~ axpr . The second element of the pair is included in any - superset of the set whose existence is asserted by the axiom of - replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by - BJ, 13-Aug-2023.) $) - axprlem5 $p |- ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) - -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $= + $( Obsolete version of ~ axprlem4 as of 18-Sep-2025. (Contributed by Rohan + Ridenour, 10-Aug-2023.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + axprlem5OLD $p |- ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) + /\ w = y ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) $= ( wel wn wal cv wral wi weq wa wex wif ax-nul nfa1 nfv nfan pm2.21 adantr alimi df-ral sylibr ad2antrl mpd simpl alnex sylib simprr biimpar syl2anc sp ifpfal jca expcom eximd mpi ) DEHIDJZEFKZLZFGHZMZFJZCBNZOZEFHZIZEJZFPV DVIEPZCANZVGQZOZFPFERVHVKVOFVFVGFVEFSVGFTUAVKVHVOVKVHOZVDVNVPVCVDVPVIVAMZ EJZVCVKVRVHVJVQEVIVAUBUDUCVAEVBUEUFVFVEVKVGVEFUOUGUHVPVLIZVGVNVPVKVSVKVHU IVIEUJUKVKVFVGULVSVNVGVLVMVGUPUMUNUQURUSUT $. - $( $j usage 'axprlem5' avoids 'ax-ext'; $) + $( $j usage 'axprlem5OLD' avoids 'ax-ext'; $) $} ${ $d x z w s p $. $d y z w s p $. $d z w t n s p $. - $( Unabbreviated version of the Axiom of Pairing of ZF set theory, derived - as a theorem from the other axioms. - - This theorem should not be referenced by any proof. Instead, use - ~ ax-pr below so that the uses of the Axiom of Pairing can be more - easily identified. - - For a shorter proof using ~ ax-ext , see ~ axprALT . (Contributed by - NM, 14-Nov-2006.) Remove dependency on ~ ax-ext . (Revised by Rohan - Ridenour, 10-Aug-2023.) (Proof shortened by BJ, 13-Aug-2023.) Use - ~ ax-pr instead. (New usage is discouraged.) $) - axpr $p |- E. z A. w ( ( w = x \/ w = y ) -> w e. z ) $= + $( Obsolete version of ~ axpr as of 18-Sep-2025. (Contributed by NM, + 14-Nov-2006.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + axprOLD $p |- E. z A. w ( ( w = x \/ w = y ) -> w e. z ) $= ( vt vn vs vp wel wn wal cv wral wi weq wo wex wif wa wb biimpr eximii ex - axprlem3 alimi axprlem4 axprlem5 jaodan imim1d alimdv eximdv mpi axprlem2 - exlimiiv ) EFIJEKFGLMGHIZNGKZDAOZDBOZPZDCIZNZDKZCQZHUPUOFGIFQUQURRSGQZUTN - ZDKZCQVCUTVDTZDKVFCABCDFGHUDVGVEDUTVDUAUEUBUPVFVBCUPVEVADUPUSVDUTUPUSVDUP - UQVDURABDEFGHUFABDEFGHUGUHUCUIUJUKULHGFEUMUN $. - $( $j usage 'axpr' avoids 'ax-ext'; $) + axprlem3OLD alimi axprlem4OLD axprlem5OLD jaodan imim1d alimdv eximdv mpi + axprlem2 exlimiiv ) EFIJEKFGLMGHIZNGKZDAOZDBOZPZDCIZNZDKZCQZHUPUOFGIFQUQU + RRSGQZUTNZDKZCQVCUTVDTZDKVFCABCDFGHUDVGVEDUTVDUAUEUBUPVFVBCUPVEVADUPUSVDU + TUPUSVDUPUQVDURABDEFGHUFABDEFGHUGUHUCUIUJUKULHGFEUMUN $. + $( $j usage 'axprOLD' avoids 'ax-ext'; $) $} ${ @@ -52134,9 +52260,9 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with See ~ zfpair for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006.) $) zfpair2 $p |- { x , y } e. _V $= - ( vz vw cv cpr wceq wex wcel wo wal ax-pr bm1.3ii dfcleq vex bibi2i albii - wb elpr bitri exbii mpbir issetri ) CAEZBEZFZCEZUFGZCHDEZUGIZUIUDGUIUEGJZ - RZDKZCHUKCDABCDLMUHUMCUHUJUIUFIZRZDKUMDUGUFNUOULDUNUKUJUIUDUEDOSPQTUAUBUC + ( vz vw cv cpr wceq wex wcel wo wb wal ax-pr sepexi dfcleq vex elpr albii + bibi2i bitri exbii mpbir issetri ) CAEZBEZFZCEZUFGZCHDEZUGIZUIUDGUIUEGJZK + ZDLZCHUKDCCABCDMNUHUMCUHUJUIUFIZKZDLUMDUGUFOUOULDUNUKUJUIUDUEDPQSRTUAUBUC $. $} @@ -76399,13 +76525,13 @@ result of an operator (deduction version). (Contributed by Paul of ` x ` i.e. the union of ` x ` . Axiom Union of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) $) axun2 $p |- E. y A. z ( z e. y <-> E. w ( z e. w /\ w e. x ) ) $= - ( wel wa wex ax-un bm1.3ii ) CDEDAEFDGBCABCDHI $. + ( wel wa wex ax-un sepexi ) CDEDAEFDGCBBABCDHI $. $( The Axiom of Union using the standard abbreviation for union. Given any set ` x ` , its union ` y ` exists. (Contributed by NM, 4-Jun-2006.) $) uniex2 $p |- E. y y = U. x $= ( vz vw cv cuni wceq wex wel wcel wb wi wa ax-un eluni imbi1i albii exbii - wal mpbir bm1.3ii dfcleq ) BEZAEZFZGZBHCBIZCEZUEJZKCSZBHUIBCUIUGLZCSZBHCD + wal mpbir sepexi dfcleq ) BEZAEZFZGZBHCBIZCEZUEJZKCSZBHUICBBUIUGLZCSZBHCD IDAIMDHZUGLZCSZBHABCDNULUOBUKUNCUIUMUGDUHUDOPQRTUAUFUJBCUCUEUBRT $. $} @@ -591261,7 +591387,7 @@ then use transitivity of a congruence relation (equality for ~ pw0 and existential quantifications using two different setvars ` x , y ` (which need not be disjoint). (Revised by BJ, 8-Aug-2022.) - TODO: move in place of ~ bm1.3ii . Relabel ("sepbi"?). $) + TODO: move in place of ~ bm1.3iiOLD . Relabel ("sepbi"?). $) bj-bm1.3ii $p |- ( E. x A. z ( ph -> z e. x ) <-> E. y A. z ( z e. y <-> ph ) ) $= ( vt wel wi wal wex weq elequ2 imbi2d albidv cbvexvw ax-sep 19.42v bimsc1