From 59c5196cb9de7d3a5ab633100b95a1b36de68d68 Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 4 Jan 2025 13:01:20 +0100 Subject: [PATCH 1/5] move cbvralvw before df-rmo --- set.mm | 144 +++++++++++++++++++++++++++++---------------------------- 1 file changed, 74 insertions(+), 70 deletions(-) diff --git a/set.mm b/set.mm index 1f9e720f21..bfcbcd1e8d 100644 --- a/set.mm +++ b/set.mm @@ -29733,6 +29733,79 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is $( $j usage 'rspw' avoids 'ax-10' 'ax-11' 'ax-12'; $) $} + ${ + $d x y A $. $d y ph $. $d x ps $. + cbvralvw.1 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( Change the bound variable of a restricted universal quantifier using + implicit substitution. Version of ~ cbvralv with a disjoint variable + condition, which does not require ~ ax-10 , ~ ax-11 , ~ ax-12 , + ~ ax-13 . (Contributed by NM, 28-Jan-1997.) (Revised by Gino Giotto, + 10-Jan-2024.) $) + cbvralvw $p |- ( A. x e. A ph <-> A. y e. A ps ) $= + ( cv wcel wi wal wral weq eleq1w imbi12d cbvalvw df-ral 3bitr4i ) CGEHZAI + ZCJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $. + $( $j usage 'cbvralvw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + + $( Change the bound variable of a restricted existential quantifier using + implicit substitution. Version of ~ cbvrexv with a disjoint variable + condition, which does not require ~ ax-10 , ~ ax-11 , ~ ax-12 , + ~ ax-13 . (Contributed by NM, 2-Jun-1998.) (Revised by Gino Giotto, + 10-Jan-2024.) $) + cbvrexvw $p |- ( E. x e. A ph <-> E. y e. A ps ) $= + ( cv wcel wa wex wrex weq eleq1w anbi12d cbvexvw df-rex 3bitr4i ) CGEHZAI + ZCJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $. + $( $j usage 'cbvrexvw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + $} + + ${ + $d x z $. $d w y $. $d x A $. $d z A $. $d x y B $. $d z y B $. + $d w B $. $d z ph $. $d y ps $. $d x ch $. $d w ch $. + cbvral2vw.1 $e |- ( x = z -> ( ph <-> ch ) ) $. + cbvral2vw.2 $e |- ( y = w -> ( ch <-> ps ) ) $. + $( Change bound variables of double restricted universal quantification, + using implicit substitution. Version of ~ cbvral2v with a disjoint + variable condition, which does not require ~ ax-13 . (Contributed by + NM, 10-Aug-2004.) (Revised by Gino Giotto, 10-Jan-2024.) $) + cbvral2vw $p |- ( A. x e. A A. y e. B ph <-> A. z e. A A. w e. B ps ) $= + ( wral weq ralbidv cbvralvw ralbii bitri ) AEILZDHLCEILZFHLBGILZFHLRSDFHD + FMACEIJNOSTFHCBEGIKOPQ $. + $( $j usage 'cbvral2vw' avoids 'ax-13'; $) + $} + + ${ + $d x z $. $d w y $. $d A x $. $d A z $. $d B w $. $d B x y $. + $d B z y $. $d ch w $. $d ch x $. $d ph z $. $d ps y $. + cbvrex2vw.1 $e |- ( x = z -> ( ph <-> ch ) ) $. + cbvrex2vw.2 $e |- ( y = w -> ( ch <-> ps ) ) $. + $( Change bound variables of double restricted universal quantification, + using implicit substitution. Version of ~ cbvrex2v with a disjoint + variable condition, which does not require ~ ax-13 . (Contributed by + FL, 2-Jul-2012.) (Revised by Gino Giotto, 10-Jan-2024.) $) + cbvrex2vw $p |- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B ps ) $= + ( wrex weq rexbidv cbvrexvw rexbii bitri ) AEILZDHLCEILZFHLBGILZFHLRSDFHD + FMACEIJNOSTFHCBEGIKOPQ $. + $( $j usage 'cbvrex2vw' avoids 'ax-13'; $) + $} + + ${ + $d w ph $. $d z ps $. $d x ch $. $d v ch $. $d y th $. $d u th $. + $d x A $. $d u z $. $d w A $. $d x y B $. $d w y B $. $d v B $. + $d x y z C $. $d w x $. $d w y z C $. $d v z C $. $d z y C $. + $d z C $. $d u C $. $d v y $. + cbvral3vw.1 $e |- ( x = w -> ( ph <-> ch ) ) $. + cbvral3vw.2 $e |- ( y = v -> ( ch <-> th ) ) $. + cbvral3vw.3 $e |- ( z = u -> ( th <-> ps ) ) $. + $( Change bound variables of triple restricted universal quantification, + using implicit substitution. Version of ~ cbvral3v with a disjoint + variable condition, which does not require ~ ax-13 . (Contributed by + NM, 10-May-2005.) (Revised by Gino Giotto, 10-Jan-2024.) $) + cbvral3vw $p |- ( A. x e. A A. y e. B A. z e. C ph <-> + A. w e. A A. v e. B A. u e. C ps ) $= + ( wral weq 2ralbidv cbvralvw cbvral2vw ralbii bitri ) AGMQFLQZEKQCGMQFLQZ + HKQBJMQILQZHKQUDUEEHKEHRACFGLMNSTUEUFHKCBDFGIJLMOPUAUBUC $. + $( $j usage 'cbvral3vw' avoids 'ax-13'; $) + $} + $( *** Theorems using axioms up to ax-8 and ax-12 only: *** $) $( Restricted specialization. (Contributed by NM, 17-Oct-1996.) $) @@ -31349,27 +31422,7 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ${ $d x y A $. $d y ph $. $d x ps $. - cbvralvw.1 $e |- ( x = y -> ( ph <-> ps ) ) $. - $( Change the bound variable of a restricted universal quantifier using - implicit substitution. Version of ~ cbvralv with a disjoint variable - condition, which does not require ~ ax-10 , ~ ax-11 , ~ ax-12 , - ~ ax-13 . (Contributed by NM, 28-Jan-1997.) (Revised by Gino Giotto, - 10-Jan-2024.) $) - cbvralvw $p |- ( A. x e. A ph <-> A. y e. A ps ) $= - ( cv wcel wi wal wral weq eleq1w imbi12d cbvalvw df-ral 3bitr4i ) CGEHZAI - ZCJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $. - $( $j usage 'cbvralvw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) - - $( Change the bound variable of a restricted existential quantifier using - implicit substitution. Version of ~ cbvrexv with a disjoint variable - condition, which does not require ~ ax-10 , ~ ax-11 , ~ ax-12 , - ~ ax-13 . (Contributed by NM, 2-Jun-1998.) (Revised by Gino Giotto, - 10-Jan-2024.) $) - cbvrexvw $p |- ( E. x e. A ph <-> E. y e. A ps ) $= - ( cv wcel wa wex wrex weq eleq1w anbi12d cbvexvw df-rex 3bitr4i ) CGEHZAI - ZCJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $. - $( $j usage 'cbvrexvw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) - + cbvrmovw.1 $e |- ( x = y -> ( ph <-> ps ) ) $. $( Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of ~ cbvrmov with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, @@ -31472,55 +31525,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( weq wa eqidd cbvrexdva2 ) ABCDEFFGADEHIFJK $. $} - ${ - $d x z $. $d w y $. $d x A $. $d z A $. $d x y B $. $d z y B $. - $d w B $. $d z ph $. $d y ps $. $d x ch $. $d w ch $. - cbvral2vw.1 $e |- ( x = z -> ( ph <-> ch ) ) $. - cbvral2vw.2 $e |- ( y = w -> ( ch <-> ps ) ) $. - $( Change bound variables of double restricted universal quantification, - using implicit substitution. Version of ~ cbvral2v with a disjoint - variable condition, which does not require ~ ax-13 . (Contributed by - NM, 10-Aug-2004.) (Revised by Gino Giotto, 10-Jan-2024.) $) - cbvral2vw $p |- ( A. x e. A A. y e. B ph <-> A. z e. A A. w e. B ps ) $= - ( wral weq ralbidv cbvralvw ralbii bitri ) AEILZDHLCEILZFHLBGILZFHLRSDFHD - FMACEIJNOSTFHCBEGIKOPQ $. - $( $j usage 'cbvral2vw' avoids 'ax-13'; $) - $} - - ${ - $d x z $. $d w y $. $d A x $. $d A z $. $d B w $. $d B x y $. - $d B z y $. $d ch w $. $d ch x $. $d ph z $. $d ps y $. - cbvrex2vw.1 $e |- ( x = z -> ( ph <-> ch ) ) $. - cbvrex2vw.2 $e |- ( y = w -> ( ch <-> ps ) ) $. - $( Change bound variables of double restricted universal quantification, - using implicit substitution. Version of ~ cbvrex2v with a disjoint - variable condition, which does not require ~ ax-13 . (Contributed by - FL, 2-Jul-2012.) (Revised by Gino Giotto, 10-Jan-2024.) $) - cbvrex2vw $p |- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B ps ) $= - ( wrex weq rexbidv cbvrexvw rexbii bitri ) AEILZDHLCEILZFHLBGILZFHLRSDFHD - FMACEIJNOSTFHCBEGIKOPQ $. - $( $j usage 'cbvrex2vw' avoids 'ax-13'; $) - $} - - ${ - $d w ph $. $d z ps $. $d x ch $. $d v ch $. $d y th $. $d u th $. - $d x A $. $d u z $. $d w A $. $d x y B $. $d w y B $. $d v B $. - $d x y z C $. $d w x $. $d w y z C $. $d v z C $. $d z y C $. - $d z C $. $d u C $. $d v y $. - cbvral3vw.1 $e |- ( x = w -> ( ph <-> ch ) ) $. - cbvral3vw.2 $e |- ( y = v -> ( ch <-> th ) ) $. - cbvral3vw.3 $e |- ( z = u -> ( th <-> ps ) ) $. - $( Change bound variables of triple restricted universal quantification, - using implicit substitution. Version of ~ cbvral3v with a disjoint - variable condition, which does not require ~ ax-13 . (Contributed by - NM, 10-May-2005.) (Revised by Gino Giotto, 10-Jan-2024.) $) - cbvral3vw $p |- ( A. x e. A A. y e. B A. z e. C ph <-> - A. w e. A A. v e. B A. u e. C ps ) $= - ( wral weq 2ralbidv cbvralvw cbvral2vw ralbii bitri ) AGMQFLQZEKQCGMQFLQZ - HKQBJMQILQZHKQUDUEEHKEHRACFGLMNSTUEUFHKCBDFGIJLMOPUAUBUC $. - $( $j usage 'cbvral3vw' avoids 'ax-13'; $) - $} - ${ $d x A $. $d z A $. $d x y B $. $d z y B $. $d w B $. $d z ph $. $d y ps $. $d x ch $. $d w ch $. From 5120ba44a3d718939acb806c08acf69c41c009a4 Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 4 Jan 2025 13:04:13 +0100 Subject: [PATCH 2/5] move ralrimia before df-rmo --- set.mm | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/set.mm b/set.mm index bfcbcd1e8d..5e1a036547 100644 --- a/set.mm +++ b/set.mm @@ -29890,6 +29890,15 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( nf5ri hbralrimi ) ABCDACEGFH $. $} + ${ + ralrimia.1 $e |- F/ x ph $. + ralrimia.2 $e |- ( ( ph /\ x e. A ) -> ps ) $. + $( Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier + version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) $) + ralrimia $p |- ( ph -> A. x e. A ps ) $= + ( cv wcel ex ralrimi ) ABCDEACGDHBFIJ $. + $} + ${ rexlimi.1 $e |- F/ x ps $. rexlimi.2 $e |- ( x e. A -> ( ph -> ps ) ) $. @@ -31881,15 +31890,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ZBIZCJDBCDKARCDAQRAQBAQBELMNOP $. $} - ${ - ralrimia.1 $e |- F/ x ph $. - ralrimia.2 $e |- ( ( ph /\ x e. A ) -> ps ) $. - $( Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier - version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) $) - ralrimia $p |- ( ph -> A. x e. A ps ) $= - ( cv wcel ex ralrimi ) ABCDEACGDHBFIJ $. - $} - ${ ralimda.1 $e |- F/ x ph $. ralimda.2 $e |- ( ( ph /\ x e. A ) -> ( ps -> ch ) ) $. From cd475d4fc6d4ae07f09ad843da725a1aca674eef Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 4 Jan 2025 13:09:27 +0100 Subject: [PATCH 3/5] delete ralimda --- changes-set.txt | 1 + set.mm | 110 ++++++++++++++++++++++-------------------------- 2 files changed, 51 insertions(+), 60 deletions(-) diff --git a/changes-set.txt b/changes-set.txt index 817ad4748b..89f31a3cd7 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -92,6 +92,7 @@ make a github issue.) DONE: Date Old New Notes + 4-Jan-25 ralimda --- obsolete - use ralimdaa instead 2-Jan-25 pr2nelem enpr2 28-Dec-24 fovrnd fovcdmd 28-Dec-24 fovrnda fovcdmda diff --git a/set.mm b/set.mm index 5e1a036547..8351a048db 100644 --- a/set.mm +++ b/set.mm @@ -31890,16 +31890,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ZBIZCJDBCDKARCDAQRAQBAQBELMNOP $. $} - ${ - ralimda.1 $e |- F/ x ph $. - ralimda.2 $e |- ( ( ph /\ x e. A ) -> ( ps -> ch ) ) $. - $( Deduction quantifying both antecedent and consequent. (Contributed by - Glauco Siliprandi, 23-Oct-2021.) $) - ralimda $p |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) ) $= - ( wral wa nfra1 nfan cv wcel id adantlr rspa adantll sylc ralrimia ex ) A - BDEHZCDEHAUAIZCDEAUADFBDEJKUBDLEMZIAUCIZBCAUCUDUAUDNOUAUCBABDEPQGRST $. - $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -712302,15 +712292,15 @@ reals with any finite set (the extended reals is an example of such a wa cordt wi a1i cc cpm clm w3a clsxlim df-xlim breqi sylib ctopon letopon nfcv lmbr3 mpbid simp3d jca simp2d rexrd mnfltd lbico1 syl3anc wceq eleq2 clt anbi2d ralbidv rexbidv imbi12d rspcva ffdmd ffvelcdmda adantrr adantr - sylc nfv simprr icoltubd xrltled ex ralimda a1d reximdai wb rexuz3 mpbird - mpd syl ) ACUAZDNZFUBOZCBUAZUCNZPZBGUDZXDBQUDZAWSDUEZRZWTSFUFUGZRZUIZCXCP - ZBQUDZXFAXIUBUJNZRZSMUAZRZXHWTXPRZUIZCXCPZBQUDZUKZMXNPZUISXIRZXMAXOYCXOAF - UHULADTUMUNUGRZSTRZYCADSXNUONZOZYEYFYCUPADSUQOYHKDSUQYGURUSUTAMSBCDXNTCDV - CXNTVANRAVBULVDVEZVFVGAYFFTRZSFVOOYDAYEYFYCYIVHZAFLVIZAFLVJSFVKVLYBYDXMUK - MXIXNXPXIVMZXQYDYAXMXPXISVNYMXTXLBQYMXSXKCXCYMXRXJXHXPXIWTVNVPVQVRVSVTWEA - XLXDBQABWFAXLXDUKXBQRAXKXACXCACWFAXKXAUKWSXCRAXKXAAXKUIZWTFAXHWTTRXJAXGTW - SDAGTDJWAWBWCAYJXKYLWDZYNSFWTAYFXKYKWDYOAXHXJWGWHWIWJWDWKWLWMWQAEQRXEXFWN - HXABCEGIWOWRWP $. + nfv simprr icoltubd xrltled ex ralimdaa a1d reximdai mpd wb rexuz3 mpbird + sylc syl ) ACUAZDNZFUBOZCBUAZUCNZPZBGUDZXDBQUDZAWSDUEZRZWTSFUFUGZRZUIZCXC + PZBQUDZXFAXIUBUJNZRZSMUAZRZXHWTXPRZUIZCXCPZBQUDZUKZMXNPZUISXIRZXMAXOYCXOA + FUHULADTUMUNUGRZSTRZYCADSXNUONZOZYEYFYCUPADSUQOYHKDSUQYGURUSUTAMSBCDXNTCD + VCXNTVANRAVBULVDVEZVFVGAYFFTRZSFVOOYDAYEYFYCYIVHZAFLVIZAFLVJSFVKVLYBYDXMU + KMXIXNXPXIVMZXQYDYAXMXPXISVNYMXTXLBQYMXSXKCXCYMXRXJXHXPXIWTVNVPVQVRVSVTWQ + AXLXDBQABWEAXLXDUKXBQRAXKXACXCACWEAXKXAUKWSXCRAXKXAAXKUIZWTFAXHWTTRXJAXGT + WSDAGTDJWAWBWCAYJXKYLWDZYNSFWTAYFXKYKWDYOAXHXJWFWGWHWIWDWJWKWLWMAEQRXEXFW + NHXABCEGIWOWRWP $. $} ${ @@ -712329,22 +712319,22 @@ reals with any finite set (the extended reals is an example of such a cv cuz wral cz wrex wi w3a cvv wf wss ctopon letopon elfvexd cnex uzsscn2 elpm2r syl22anc mnfxr cico cr mnfnei adantll clt nfan simprr 3adant1 wceq uztrn2 fdmd 3ad2ant1 eleqtrrd ad5ant134 adantl4r simp-4r rexr syl simp-4l - ad4ant23 ffvelcdmda syl2anc mnfled elicod adantl3r sseldd ralimda adantrr - simpr jca ex mpd 3impb r19.21bi adantr reximdd rexuz3 ad2antrr rexlimdva2 - wb mpbid ralrimiva 3jca nfcv lmbr3 mpbird df-xlim breqi ) AENUBUCZENUDUEO - ZUFOZUCZAXTEPUGUHUIQZNPQZNUAUKZQZDUKZEUJZQZYEEOZYCQZRZDCUKZULOZUMZCUNUOZU - PZUAXRUMZUQAYAYBYPAPURQUGURQZGPEUSGUGUTZYAAXRVAPXRPVAOQAVBSZVCYQAVDSLYRAF - GKVESPUGGEURURVFVGYBAVHSAYOUAXRAYCXRQZRZYDYNUUAYDRNBUKZVIUIZYCUTZBVJUOZYN - YTYDUUEABYCVKVLAUUEYNUPYTYDAUUDYNBVJAUUBVJQZRZUUDRZYMCGUOZYNUUHYHUUBVMUCZ - DYLUMZYMCGUUGUUDCAUUFCIUUFCTVNUUDCTVNUUHYKGQZUUKYMUUHUULUUKRRUUKYMUUHUULU - UKVOUUHUULUUKYMUPUUKUUHUULRZUUJYJDYLUUHUULDUUGUUDDAUUFDHUUFDTVNUUDDTVNUUL - DTVNUUMYEYLQZRZUUJYJUUOUUJRZYGYIAUUFUUDUULUUNUUJYGAUULUUNYGUUDUUJAUULUUNU - QYEGYFUULUUNYEGQZAFYEYKGKVRZVPAUULYFGVQUUNAGPELVSVTWAWBWCUUPUUCYCYHAUUFUU - DUULUUNUUJUUDAUUDUULUUNUUJWDWCUUGUULUUNUUJYHUUCQUUDUUGUULRUUNRZUUJRZNUUBY - HYBUUTVHSUUTUUFUUBPQAUUFUULUUNUUJWDUUBWEWFUUTAUUQYHPQAUUFUULUUNUUJWGUULUU - NUUQUUGUUJUURWHAGPYEELWIWJZUUTYHUVAWKUUSUUJWQWLWMWNWRWSWOWPWTXAUUGUUKCGUO - ZUUDAUVBBVJMXBXCXDAUUIYNXHZUUFUUDAFUNQUVCJYJCDFGKXEWFXFXIXGXFWTWSXJXKAUAN - CDEXRPDEXLYSXMXNXQXTXHAENUBXSXOXPSXN $. + ad4ant23 ffvelcdmda syl2anc mnfled elicod adantl3r sseldd jca ex ralimdaa + simpr adantrr 3impb r19.21bi adantr reximdd wb rexuz3 ad2antrr rexlimdva2 + mpd mpbid ralrimiva 3jca nfcv lmbr3 mpbird df-xlim breqi ) AENUBUCZENUDUE + OZUFOZUCZAXTEPUGUHUIQZNPQZNUAUKZQZDUKZEUJZQZYEEOZYCQZRZDCUKZULOZUMZCUNUOZ + UPZUAXRUMZUQAYAYBYPAPURQUGURQZGPEUSGUGUTZYAAXRVAPXRPVAOQAVBSZVCYQAVDSLYRA + FGKVESPUGGEURURVFVGYBAVHSAYOUAXRAYCXRQZRZYDYNUUAYDRNBUKZVIUIZYCUTZBVJUOZY + NYTYDUUEABYCVKVLAUUEYNUPYTYDAUUDYNBVJAUUBVJQZRZUUDRZYMCGUOZYNUUHYHUUBVMUC + ZDYLUMZYMCGUUGUUDCAUUFCIUUFCTVNUUDCTVNUUHYKGQZUUKYMUUHUULUUKRRUUKYMUUHUUL + UUKVOUUHUULUUKYMUPUUKUUHUULRZUUJYJDYLUUHUULDUUGUUDDAUUFDHUUFDTVNUUDDTVNUU + LDTVNUUMYEYLQZRZUUJYJUUOUUJRZYGYIAUUFUUDUULUUNUUJYGAUULUUNYGUUDUUJAUULUUN + UQYEGYFUULUUNYEGQZAFYEYKGKVRZVPAUULYFGVQUUNAGPELVSVTWAWBWCUUPUUCYCYHAUUFU + UDUULUUNUUJUUDAUUDUULUUNUUJWDWCUUGUULUUNUUJYHUUCQUUDUUGUULRUUNRZUUJRZNUUB + YHYBUUTVHSUUTUUFUUBPQAUUFUULUUNUUJWDUUBWEWFUUTAUUQYHPQAUUFUULUUNUUJWGUULU + UNUUQUUGUUJUURWHAGPYEELWIWJZUUTYHUVAWKUUSUUJWRWLWMWNWOWPWQWSXHWTUUGUUKCGU + OZUUDAUVBBVJMXAXBXCAUUIYNXDZUUFUUDAFUNQUVCJYJCDFGKXEWFXFXIXGXFXHWPXJXKAUA + NCDEXRPDEXLYSXMXNXQXTXDAENUBXSXOXPSXN $. $} ${ @@ -712407,15 +712397,15 @@ reals with any finite set (the extended reals is an example of such a wa cordt wi a1i cc cpm clm w3a clsxlim df-xlim breqi sylib ctopon letopon nfcv lmbr3 mpbid simp3d jca rexrd simp2d ltpnfd ubioc1 syl3anc wceq eleq2 clt anbi2d ralbidv rexbidv imbi12d rspcva adantr ffdmd ffvelcdmda adantrr - sylc nfv simprr iocgtlbd xrltled ex ralimda a1d reximdai wb rexuz3 mpbird - mpd syl ) AFCUAZDNZUBOZCBUAZUCNZPZBGUDZXDBQUDZAWSDUEZRZWTFSUFUGZRZUIZCXCP - ZBQUDZXFAXIUBUJNZRZSMUAZRZXHWTXPRZUIZCXCPZBQUDZUKZMXNPZUISXIRZXMAXOYCXOAF - UHULADTUMUNUGRZSTRZYCADSXNUONZOZYEYFYCUPADSUQOYHKDSUQYGURUSUTAMSBCDXNTCDV - CXNTVANRAVBULVDVEZVFVGAFTRZYFFSVOOYDAFLVHZAYEYFYCYIVIZAFLVJFSVKVLYBYDXMUK - MXIXNXPXIVMZXQYDYAXMXPXISVNYMXTXLBQYMXSXKCXCYMXRXJXHXPXIWTVNVPVQVRVSVTWEA - XLXDBQABWFAXLXDUKXBQRAXKXACXCACWFAXKXAUKWSXCRAXKXAAXKUIZFWTAYJXKYKWAZAXHW - TTRXJAXGTWSDAGTDJWBWCWDYNFSWTYOAYFXKYLWAAXHXJWGWHWIWJWAWKWLWMWQAEQRXEXFWN - HXABCEGIWOWRWP $. + nfv simprr iocgtlbd xrltled ex ralimdaa a1d reximdai mpd wb rexuz3 mpbird + sylc syl ) AFCUAZDNZUBOZCBUAZUCNZPZBGUDZXDBQUDZAWSDUEZRZWTFSUFUGZRZUIZCXC + PZBQUDZXFAXIUBUJNZRZSMUAZRZXHWTXPRZUIZCXCPZBQUDZUKZMXNPZUISXIRZXMAXOYCXOA + FUHULADTUMUNUGRZSTRZYCADSXNUONZOZYEYFYCUPADSUQOYHKDSUQYGURUSUTAMSBCDXNTCD + VCXNTVANRAVBULVDVEZVFVGAFTRZYFFSVOOYDAFLVHZAYEYFYCYIVIZAFLVJFSVKVLYBYDXMU + KMXIXNXPXIVMZXQYDYAXMXPXISVNYMXTXLBQYMXSXKCXCYMXRXJXHXPXIWTVNVPVQVRVSVTWQ + AXLXDBQABWEAXLXDUKXBQRAXKXACXCACWEAXKXAUKWSXCRAXKXAAXKUIZFWTAYJXKYKWAZAXH + WTTRXJAXGTWSDAGTDJWBWCWDYNFSWTYOAYFXKYLWAAXHXJWFWGWHWIWAWJWKWLWMAEQRXEXFW + NHXABCEGIWOWRWP $. $} ${ @@ -712435,22 +712425,22 @@ reals with any finite set (the extended reals is an example of such a elpm2r syl22anc pnfxr cioc cr pnfnei adantll clt nfan simprr 3adant1 wceq uztrn2 fdmd 3ad2ant1 eleqtrrd ad5ant134 adantl4r simp-4r rexr syl simp-4l ad4ant23 ffvelcdmda syl2anc simpr ffvelcdmd pnfged eliocd adantl3r sseldd - jca ex ralimda adantrr mpd 3impb r19.21bi adantr wb rexuz3 ad2antrr mpbid - reximdd rexlimdva2 ralrimiva 3jca nfcv lmbr3 mpbird df-xlim breqi ) AENUB - UCZENUDUEOZUFOZUCZAYAEPUGUHUIQZNPQZNUAUKZQZDUKZEUJZQZYFEOZYDQZRZDCUKZULOZ - UMZCUNUOZUPZUAXSUMZUQAYBYCYQAPURQUGURQZGPEUSZGUGUTZYBAXSVAPXSPVAOQAVBSZVC - YRAVDSLYTAFGKVESPUGGEURURVFVGYCAVHSAYPUAXSAYDXSQZRZYEYOUUCYERBUKZNVIUIZYD - UTZBVJUOZYOUUBYEUUGABYDVKVLAUUGYOUPUUBYEAUUFYOBVJAUUDVJQZRZUUFRZYNCGUOZYO - UUJUUDYIVMUCZDYMUMZYNCGUUIUUFCAUUHCIUUHCTVNUUFCTVNUUJYLGQZUUMYNUUJUUNUUMR - RUUMYNUUJUUNUUMVOUUJUUNUUMYNUPUUMUUJUUNRZUULYKDYMUUJUUNDUUIUUFDAUUHDHUUHD - TVNUUFDTVNUUNDTVNUUOYFYMQZRZUULYKUUQUULRZYHYJAUUHUUFUUNUUPUULYHAUUNUUPYHU - UFUULAUUNUUPUQZYFGYGUUNUUPYFGQZAFYFYLGKVRZVPZAUUNYGGVQUUPAGPELVSVTWAWBWCU - URUUEYDYIAUUHUUFUUNUUPUULUUFAUUFUUNUUPUULWDWCUUIUUNUUPUULYIUUEQUUFUUIUUNR - UUPRZUULRZUUDNYIUVDUUHUUDPQAUUHUUNUUPUULWDUUDWEWFYCUVDVHSUVDAUUTYIPQAUUHU - UNUUPUULWGUUNUUPUUTUUIUULUVAWHAGPYFELWIWJUVCUULWKAUUNUUPYINUDUCUUHUULUUSY - IUUSGPYFEAUUNYSUUPLVTUVBWLWMWBWNWOWPWQWRWSWTXAXBUUIUUMCGUOZUUFAUVEBVJMXCX - DXIAUUKYOXEZUUHUUFAFUNQUVFJYKCDFGKXFWFXGXHXJXGXAWRXKXLAUANCDEXSPDEXMUUAXN - XOXRYAXEAENUBXTXPXQSXO $. + jca ex ralimdaa adantrr mpd 3impb r19.21bi adantr reximdd rexuz3 ad2antrr + wb mpbid rexlimdva2 ralrimiva 3jca nfcv lmbr3 mpbird df-xlim breqi ) AENU + BUCZENUDUEOZUFOZUCZAYAEPUGUHUIQZNPQZNUAUKZQZDUKZEUJZQZYFEOZYDQZRZDCUKZULO + ZUMZCUNUOZUPZUAXSUMZUQAYBYCYQAPURQUGURQZGPEUSZGUGUTZYBAXSVAPXSPVAOQAVBSZV + CYRAVDSLYTAFGKVESPUGGEURURVFVGYCAVHSAYPUAXSAYDXSQZRZYEYOUUCYERBUKZNVIUIZY + DUTZBVJUOZYOUUBYEUUGABYDVKVLAUUGYOUPUUBYEAUUFYOBVJAUUDVJQZRZUUFRZYNCGUOZY + OUUJUUDYIVMUCZDYMUMZYNCGUUIUUFCAUUHCIUUHCTVNUUFCTVNUUJYLGQZUUMYNUUJUUNUUM + RRUUMYNUUJUUNUUMVOUUJUUNUUMYNUPUUMUUJUUNRZUULYKDYMUUJUUNDUUIUUFDAUUHDHUUH + DTVNUUFDTVNUUNDTVNUUOYFYMQZRZUULYKUUQUULRZYHYJAUUHUUFUUNUUPUULYHAUUNUUPYH + UUFUULAUUNUUPUQZYFGYGUUNUUPYFGQZAFYFYLGKVRZVPZAUUNYGGVQUUPAGPELVSVTWAWBWC + UURUUEYDYIAUUHUUFUUNUUPUULUUFAUUFUUNUUPUULWDWCUUIUUNUUPUULYIUUEQUUFUUIUUN + RUUPRZUULRZUUDNYIUVDUUHUUDPQAUUHUUNUUPUULWDUUDWEWFYCUVDVHSUVDAUUTYIPQAUUH + UUNUUPUULWGUUNUUPUUTUUIUULUVAWHAGPYFELWIWJUVCUULWKAUUNUUPYINUDUCUUHUULUUS + YIUUSGPYFEAUUNYSUUPLVTUVBWLWMWBWNWOWPWQWRWSWTXAXBUUIUUMCGUOZUUFAUVEBVJMXC + XDXEAUUKYOXHZUUHUUFAFUNQUVFJYKCDFGKXFWFXGXIXJXGXAWRXKXLAUANCDEXSPDEXMUUAX + NXOXRYAXHAENUBXTXPXQSXO $. $} ${ From a33b00bbb0fbeafafc21f353d70b79b1dc1362e4 Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sat, 4 Jan 2025 13:13:58 +0100 Subject: [PATCH 4/5] move hbra1 before df-rmo --- set.mm | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/set.mm b/set.mm index 8351a048db..6b2b4c2c84 100644 --- a/set.mm +++ b/set.mm @@ -30317,6 +30317,13 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is 'df-cleq' 'ax-12' 'ax-13' 'ax-ext'; $) $} + $( *** Theorems using axioms up to ax-8 and ax-10, ax-12 only: *** $) + + $( The setvar ` x ` is not free in ` A. x e. A ph ` . (Contributed by NM, + 18-Oct-1996.) (Proof shortened by Wolf Lammen, 7-Dec-2019.) $) + hbra1 $p |- ( A. x e. A ph -> A. x A. x e. A ph ) $= + ( wral nfra1 nf5ri ) ABCDBABCEF $. + $( Extend wff notation to include restricted existential uniqueness. $) wreu $a wff E! x e. A ph $. @@ -30365,11 +30372,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ~ df-ral . (Contributed by NM, 22-Nov-1994.) $) df-rab $a |- { x e. A | ph } = { x | ( x e. A /\ ph ) } $. - $( The setvar ` x ` is not free in ` A. x e. A ph ` . (Contributed by NM, - 18-Oct-1996.) (Proof shortened by Wolf Lammen, 7-Dec-2019.) $) - hbra1 $p |- ( A. x e. A ph -> A. x A. x e. A ph ) $= - ( wral nfra1 nf5ri ) ABCDBABCEF $. - ${ hbral.1 $e |- ( y e. A -> A. x y e. A ) $. hbral.2 $e |- ( ph -> A. x ph ) $. From 722b43c443df109e9b05d3c2e6f114fd862d3133 Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sun, 5 Jan 2025 03:51:08 +0100 Subject: [PATCH 5/5] fix merge conflict --- changes-set.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/changes-set.txt b/changes-set.txt index 89f31a3cd7..1b1a7bfa7c 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -93,6 +93,7 @@ make a github issue.) DONE: Date Old New Notes 4-Jan-25 ralimda --- obsolete - use ralimdaa instead + 3-Jan-25 srgi srgdilem 2-Jan-25 pr2nelem enpr2 28-Dec-24 fovrnd fovcdmd 28-Dec-24 fovrnda fovcdmda