diff --git a/discouraged b/discouraged index a484eaef86..0557785111 100644 --- a/discouraged +++ b/discouraged @@ -18731,6 +18731,7 @@ New usage of "rabrabiOLD" is discouraged (0 uses). New usage of "ral0OLD" is discouraged (0 uses). New usage of "ralabOLD" is discouraged (0 uses). New usage of "ralbidaOLD" is discouraged (0 uses). +New usage of "ralcom13OLD" is discouraged (0 uses). New usage of "ralcom2" is discouraged (0 uses). New usage of "ralcom3OLD" is discouraged (0 uses). New usage of "ralcom4OLD" is discouraged (0 uses). @@ -21115,6 +21116,7 @@ Proof modification of "rabrabiOLD" is discouraged (38 steps). Proof modification of "ral0OLD" is discouraged (12 steps). Proof modification of "ralabOLD" is discouraged (40 steps). Proof modification of "ralbidaOLD" is discouraged (43 steps). +Proof modification of "ralcom13OLD" is discouraged (58 steps). Proof modification of "ralcom3OLD" is discouraged (38 steps). Proof modification of "ralcom4OLD" is discouraged (63 steps). Proof modification of "raleleqALT" is discouraged (26 steps). diff --git a/set.mm b/set.mm index 3f56d58905..452c738487 100644 --- a/set.mm +++ b/set.mm @@ -30008,6 +30008,12 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is rsp2 $p |- ( A. x e. A A. y e. B ph -> ( ( x e. A /\ y e. B ) -> ph ) ) $= ( wral cv wcel wi rsp syl6 impd ) ACEFZBDFZBGDHZCGEHZANOMPAIMBDJACEJKL $. + $( Restricted specialization. (Contributed by FL, 4-Jun-2012.) (Proof + shortened by Wolf Lammen, 7-Jan-2020.) $) + rsp2e $p |- ( ( x e. A /\ y e. B /\ ph ) -> E. x e. A E. y e. B ph ) $= + ( cv wcel wrex wa rspe sylan2 3impb ) BFDGZCFEGZAACEHZBDHZNAIMOPACEJOBDJKL + $. + ${ rspec2.1 $e |- A. x e. A A. y e. B ph $. $( Specialization rule for restricted quantification, with two quantifiers. @@ -30060,6 +30066,149 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is EITEOPATELGMBCQJRSS $. $} + $( *** Theorems using axioms up to ax-8 and ax-10 only: *** $) + + $( The setvar ` x ` is not free in ` A. x e. A ph ` . (Contributed by NM, + 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.) $) + nfra1 $p |- F/ x A. x e. A ph $= + ( wral cv wcel wi wal df-ral nfa1 nfxfr ) ABCDBECFAGZBHBABCILBJK $. + + $( The setvar ` x ` is not free in ` E. x e. A ph ` . (Contributed by NM, + 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.) $) + nfre1 $p |- F/ x E. x e. A ph $= + ( wrex cv wcel wa wex df-rex nfe1 nfxfr ) ABCDBECFAGZBHBABCILBJK $. + + $( *** Theorems using axioms up to ax-8 and ax-11 only: *** $) + + ${ + $d x y $. $d y A $. + $( Commutation of restricted and unrestricted universal quantifiers. + (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, + 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) + (Proof shortened by Wolf Lammen, 31-Oct-2024.) $) + ralcom4 $p |- ( A. x e. A A. y ph <-> A. y A. x e. A ph ) $= + ( wal wral cv wcel wi 19.21v albii alcom df-ral 3bitr4ri bitr4i ) ACEZBDF + ZBGDHZAIZBEZCEZABDFZCESCEZBERPIZBEUAQUCUDBRACJKSCBLPBDMNUBTCABDMKO $. + + $( Obsolete version of ~ ralcom4 as of 31-Oct-2024. (Contributed by NM, + 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce + axiom dependencies. (Revised by BJ, 13-Jun-2019.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + ralcom4OLD $p |- ( A. x e. A A. y ph <-> A. y A. x e. A ph ) $= + ( cv wcel wal wi wral 19.21v bicomi albii alcom bitri df-ral 3bitr4i ) BE + DFZACGZHZBGZQAHZBGZCGZRBDIABDIZCGTUACGZBGUCSUEBUESQACJKLUABCMNRBDOUDUBCAB + DOLP $. + + $( Commutation of restricted and unrestricted existential quantifiers. + (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, + 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, + 13-Jun-2019.) $) + rexcom4 $p |- ( E. x e. A E. y ph <-> E. y E. x e. A ph ) $= + ( cv wcel wa wex wrex exdistr df-rex exbii excom bitri 3bitr4ri ) BEDFZAG + ZCHBHZPACHZGBHABDIZCHZSBDIPABCJUAQBHZCHRTUBCABDKLQCBMNSBDKO $. + + $d x B $. + $( Commutation of restricted universal quantifiers. See ~ ralcom2 for a + version without disjoint variable condition on ` x , y ` . This theorem + should be used in place of ~ ralcom2 since it depends on a smaller set + of axioms. (Contributed by NM, 13-Oct-1999.) (Revised by Mario + Carneiro, 14-Oct-2016.) $) + ralcom $p |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph ) $= + ( cv wcel wa wi wal wral ancomst 2albii alcom bitri r2al 3bitr4i ) BFDGZC + FEGZHAIZCJBJZSRHAIZBJCJZACEKBDKABDKCEKUAUBCJBJUCTUBBCRSALMUBBCNOABCDEPACB + EDPQ $. + $( $j usage 'ralcom' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12' + 'ax-13' 'ax-ext'; $) + + $( Commutation of restricted existential quantifiers. (Contributed by NM, + 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof + shortened by BJ, 26-Aug-2023.) (Proof shortened by Wolf Lammen, + 8-Dec-2024.) $) + rexcom $p |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph ) $= + ( wrex wn wral ralcom ralnex2 3bitr3i con4bii ) ACEFBDFZABDFCEFZAGZCEHBDH + OBDHCEHMGNGOBCDEIABCDEJACBEDJKL $. + $( $j usage 'rexcom' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12' + 'ax-13' 'ax-ext'; $) + + $( Obsolete version of ~ rexcom as of 8-Dec-2024. (Contributed by NM, + 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof + shortened by BJ, 26-Aug-2023.) (New usage is discouraged.) + (Proof modification is discouraged.) $) + rexcomOLD $p |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph ) $= + ( wrex cv wcel wa wex df-rex rexbii rexcom4 r19.42v exbii bitr4i 3bitri ) + ACEFZBDFCGEHZAIZCJZBDFTBDFZCJZABDFZCEFZRUABDACEKLTBCDMUCSUDIZCJUEUBUFCSAB + DNOUDCEKPQ $. + $( $j usage 'rexcomOLD' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12' + 'ax-13' 'ax-ext'; $) + $} + + ${ + $d x A $. $d x y $. $d x ph $. + $( Specialized existential commutation lemma. (Contributed by Jeff Madsen, + 1-Jun-2011.) $) + rexcom4a $p |- ( E. x E. y e. A ( ph /\ ps ) <-> + E. y e. A ( ph /\ E. x ps ) ) $= + ( wa wrex wex rexcom4 19.42v rexbii bitr3i ) ABFZDEGCHMCHZDEGABCHFZDEGMDC + EINODEABCJKL $. + $} + + ${ + $d z A $. $d z B $. $d x C $. $d y C $. $d x z $. $d y z $. + $( Rotate three restricted universal quantifiers. (Contributed by AV, + 3-Dec-2021.) $) + ralrot3 $p |- ( A. x e. A A. y e. B A. z e. C ph + <-> A. z e. C A. x e. A A. y e. B ph ) $= + ( wral ralcom ralbii bitri ) ADGHCFHZBEHACFHZDGHZBEHMBEHDGHLNBEACDFGIJMBD + EGIK $. + $} + + ${ + $d y z A $. $d x z B $. $d x y C $. + $( Swap first and third restricted universal quantifiers. (Contributed by + AV, 3-Dec-2021.) (Proof shortened by Wolf Lammen, 2-Jan-2025.) $) + ralcom13 $p |- ( A. x e. A A. y e. B A. z e. C ph + <-> A. z e. C A. y e. B A. x e. A ph ) $= + ( wral ralrot3 ralcom ralbii bitri ) ADGHCFHBEHACFHBEHZDGHABEHCFHZDGHABCD + EFGIMNDGABCEFJKL $. + + $( Obsolete version of ~ ralcom13 as of 2-Jan-2025. (Contributed by AV, + 3-Dec-2021.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + ralcom13OLD $p |- ( A. x e. A A. y e. B A. z e. C ph + <-> A. z e. C A. y e. B A. x e. A ph ) $= + ( wral ralcom ralbii 3bitri ) ADGHZCFHBEHLBEHZCFHABEHZDGHZCFHNCFHDGHLBCEF + IMOCFABDEGIJNCDFGIK $. + + $( Swap first and third restricted existential quantifiers. (Contributed + by NM, 8-Apr-2015.) $) + rexcom13 $p |- ( E. x e. A E. y e. B E. z e. C ph + <-> E. z e. C E. y e. B E. x e. A ph ) $= + ( wrex rexcom rexbii 3bitri ) ADGHZCFHBEHLBEHZCFHABEHZDGHZCFHNCFHDGHLBCEF + IMOCFABDEGIJNCDFGIK $. + $} + + ${ + $d w z A $. $d w z B $. $d w x C $. $d w y C $. $d x z D $. + $d y z D $. + $( Rotate four restricted existential quantifiers twice. (Contributed by + NM, 8-Apr-2015.) $) + rexrot4 $p |- ( E. x e. A E. y e. B E. z e. C E. w e. D ph + <-> E. z e. C E. w e. D E. x e. A E. y e. B ph ) $= + ( wrex rexcom13 rexbii bitri ) AEIJDHJCGJZBFJACGJZDHJEIJZBFJOBFJEIJDHJNPB + FACDEGHIKLOBEDFIHKM $. + $} + + ${ + $d A x $. $d A y $. $d B x $. $d B y $. $d w x $. $d w y $. $d x z $. + $d y z $. + $( Rotate two existential quantifiers and two restricted existential + quantifiers. (Contributed by AV, 9-Nov-2023.) $) + 2ex2rexrot $p |- ( E. x E. y E. z e. A E. w e. B ph + <-> E. z e. A E. w e. B E. x E. y ph ) $= + ( wex wrex rexcom4 rexbii bitri exbii 3bitrri ) ACHZBHEGIZDFIOEGIZBHZDFIQ + DFIZBHAEGIZDFICHZBHPRDFOEBGJKQDBFJSUABSTCHZDFIUAQUBDFAECGJKTDCFJLMN $. + $} + $( Extend wff notation to include restricted existential uniqueness. $) wreu $a wff E! x e. A ph $. @@ -30108,11 +30257,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.) (Revised by Mario Carneiro, 7-Oct-2016.) $) - nfra1 $p |- F/ x A. x e. A ph $= - ( wral cv wcel wi wal df-ral nfa1 nfxfr ) ABCDBECFAGZBHBABCILBJK $. - $( 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 ) $= @@ -30267,93 +30411,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is ( cv wcel eleq2i imbi12i ralbii2 ) ABCDECHZDIMEIABDEMFJGKL $. $} - ${ - $d x y $. $d y A $. - $( Commutation of restricted and unrestricted universal quantifiers. - (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, - 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) - (Proof shortened by Wolf Lammen, 31-Oct-2024.) $) - ralcom4 $p |- ( A. x e. A A. y ph <-> A. y A. x e. A ph ) $= - ( wal wral cv wcel wi 19.21v albii alcom df-ral 3bitr4ri bitr4i ) ACEZBDF - ZBGDHZAIZBEZCEZABDFZCESCEZBERPIZBEUAQUCUDBRACJKSCBLPBDMNUBTCABDMKO $. - - $( Obsolete version of ~ ralcom4 as of 31-Oct-2024. (Contributed by NM, - 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce - axiom dependencies. (Revised by BJ, 13-Jun-2019.) - (New usage is discouraged.) (Proof modification is discouraged.) $) - ralcom4OLD $p |- ( A. x e. A A. y ph <-> A. y A. x e. A ph ) $= - ( cv wcel wal wi wral 19.21v bicomi albii alcom bitri df-ral 3bitr4i ) BE - DFZACGZHZBGZQAHZBGZCGZRBDIABDIZCGTUACGZBGUCSUEBUESQACJKLUABCMNRBDOUDUBCAB - DOLP $. - - $d x B $. - $( Commutation of restricted universal quantifiers. See ~ ralcom2 for a - version without disjoint variable condition on ` x , y ` . This theorem - should be used in place of ~ ralcom2 since it depends on a smaller set - of axioms. (Contributed by NM, 13-Oct-1999.) (Revised by Mario - Carneiro, 14-Oct-2016.) $) - ralcom $p |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph ) $= - ( cv wcel wa wi wal wral ancomst 2albii alcom bitri r2al 3bitr4i ) BFDGZC - FEGZHAIZCJBJZSRHAIZBJCJZACEKBDKABDKCEKUAUBCJBJUCTUBBCRSALMUBBCNOABCDEPACB - EDPQ $. - $( $j usage 'ralcom' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12' - 'ax-13' 'ax-ext'; $) - $} - - ${ - $d x y $. $d y A $. - $( Commutation of restricted and unrestricted existential quantifiers. - (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, - 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, - 13-Jun-2019.) $) - rexcom4 $p |- ( E. x e. A E. y ph <-> E. y E. x e. A ph ) $= - ( cv wcel wa wex wrex exdistr df-rex exbii excom bitri 3bitr4ri ) BEDFZAG - ZCHBHZPACHZGBHABDIZCHZSBDIPABCJUAQBHZCHRTUBCABDKLQCBMNSBDKO $. - - $d x B $. - $( Commutation of restricted existential quantifiers. (Contributed by NM, - 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof - shortened by BJ, 26-Aug-2023.) (Proof shortened by Wolf Lammen, - 8-Dec-2024.) $) - rexcom $p |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph ) $= - ( wrex wn wral ralcom ralnex2 3bitr3i con4bii ) ACEFBDFZABDFCEFZAGZCEHBDH - OBDHCEHMGNGOBCDEIABCDEJACBEDJKL $. - $( $j usage 'rexcom' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12' - 'ax-13' 'ax-ext'; $) - $} - - ${ - $d A x $. $d A y $. $d B x $. $d B y $. $d w x $. $d w y $. $d x z $. - $d y z $. - $( Rotate two existential quantifiers and two restricted existential - quantifiers. (Contributed by AV, 9-Nov-2023.) $) - 2ex2rexrot $p |- ( E. x E. y E. z e. A E. w e. B ph - <-> E. z e. A E. w e. B E. x E. y ph ) $= - ( wex wrex rexcom4 rexbii bitri exbii 3bitrri ) ACHZBHEGIZDFIOEGIZBHZDFIQ - DFIZBHAEGIZDFICHZBHPRDFOEBGJKQDBFJSUABSTCHZDFIUAQUBDFAECGJKTDCFJLMN $. - $} - - ${ - $d x A $. $d x y $. $d x ph $. - $( Specialized existential commutation lemma. (Contributed by Jeff Madsen, - 1-Jun-2011.) $) - rexcom4a $p |- ( E. x E. y e. A ( ph /\ ps ) <-> - E. y e. A ( ph /\ E. x ps ) ) $= - ( wa wrex wex rexcom4 19.42v rexbii bitr3i ) ABFZDEGCHMCHZDEGABCHFZDEGMDC - EINODEABCJKL $. - $} - - $( Restricted specialization. (Contributed by FL, 4-Jun-2012.) (Proof - shortened by Wolf Lammen, 7-Jan-2020.) $) - rsp2e $p |- ( ( x e. A /\ y e. B /\ ph ) -> E. x e. A E. y e. B ph ) $= - ( cv wcel wrex wa rspe sylan2 3impb ) BFDGZCFEGZAACEHZBDHZNAIMOPACEJOBDJKL - $. - - $( The setvar ` x ` is not free in ` E. x e. A ph ` . (Contributed by NM, - 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.) $) - nfre1 $p |- F/ x E. x e. A ph $= - ( wrex cv wcel wa wex df-rex nfe1 nfxfr ) ABCDBECFAGZBHBABCILBJK $. - ${ $d x y $. nfrexd.1 $e |- F/ y ph $. @@ -30464,58 +30521,6 @@ atomic formula (class version of ~ elsb1 ). Usage of this theorem is BCPQABCDEFRACBEDGRS $. $} - ${ - $d x y $. $d y A $. $d x B $. - $( Obsolete version of ~ rexcom as of 8-Dec-2024. (Contributed by NM, - 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof - shortened by BJ, 26-Aug-2023.) (New usage is discouraged.) - (Proof modification is discouraged.) $) - rexcomOLD $p |- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph ) $= - ( wrex cv wcel wa wex df-rex rexbii rexcom4 r19.42v exbii bitr4i 3bitri ) - ACEFZBDFCGEHZAIZCJZBDFTBDFZCJZABDFZCEFZRUABDACEKLTBCDMUCSUDIZCJUEUBUFCSAB - DNOUDCEKPQ $. - $( $j usage 'rexcomOLD' avoids 'ax-6' 'ax-7' 'ax-8' 'ax-9' 'ax-10' 'ax-12' - 'ax-13' 'ax-ext'; $) - $} - - ${ - $d y z A $. $d x z B $. $d x y C $. - $( Swap first and third restricted universal quantifiers. (Contributed by - AV, 3-Dec-2021.) $) - ralcom13 $p |- ( A. x e. A A. y e. B A. z e. C ph - <-> A. z e. C A. y e. B A. x e. A ph ) $= - ( wral ralcom ralbii 3bitri ) ADGHZCFHBEHLBEHZCFHABEHZDGHZCFHNCFHDGHLBCEF - IMOCFABDEGIJNCDFGIK $. - - $( Swap first and third restricted existential quantifiers. (Contributed - by NM, 8-Apr-2015.) $) - rexcom13 $p |- ( E. x e. A E. y e. B E. z e. C ph - <-> E. z e. C E. y e. B E. x e. A ph ) $= - ( wrex rexcom rexbii 3bitri ) ADGHZCFHBEHLBEHZCFHABEHZDGHZCFHNCFHDGHLBCEF - IMOCFABDEGIJNCDFGIK $. - $} - - ${ - $d z A $. $d z B $. $d x C $. $d y C $. $d x z $. $d y z $. - $( Rotate three restricted universal quantifiers. (Contributed by AV, - 3-Dec-2021.) $) - ralrot3 $p |- ( A. x e. A A. y e. B A. z e. C ph - <-> A. z e. C A. x e. A A. y e. B ph ) $= - ( wral ralcom ralbii bitri ) ADGHCFHZBEHACFHZDGHZBEHMBEHDGHLNBEACDFGIJMBD - EGIK $. - $} - - ${ - $d w z A $. $d w z B $. $d w x C $. $d w y C $. $d x z D $. - $d y z D $. - $( Rotate four restricted existential quantifiers twice. (Contributed by - NM, 8-Apr-2015.) $) - rexrot4 $p |- ( E. x e. A E. y e. B E. z e. C E. w e. D ph - <-> E. z e. C E. w e. D E. x e. A E. y e. B ph ) $= - ( wrex rexcom13 rexbii bitri ) AEIJDHJCGJZBFJACGJZDHJEIJZBFJOBFJEIJDHJNPB - FACDEGHIKLOBEDFIHKM $. - $} - ${ $d y A $. $d x A $. $( Commutation of restricted universal quantifiers. Note that ` x ` and