From a713b25f08ccf612769686226511ce5b3bb5f87b Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Thu, 12 Oct 2023 00:37:43 +0200 Subject: [PATCH 1/3] replaced '|- ( [ x / y ]' with '|- ( [ y / x ]' in set.mm --- set.mm | 212 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 106 insertions(+), 106 deletions(-) diff --git a/set.mm b/set.mm index fb963226f4..c2d8b7bf2a 100644 --- a/set.mm +++ b/set.mm @@ -17238,27 +17238,27 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the $} ${ - $d y w z $. $d x w $. + $d x w z $. $d y w $. $( Substitution in an equality. (Contributed by Raph Levien and FL, 4-Dec-2005.) Reduce axiom usage. (Revised by Wolf Lammen, 23-Jul-2023.) $) - equsb3 $p |- ( [ x / y ] y = z <-> x = z ) $= - ( vw weq equequ1 sbievw2 ) BCEACEDCEBADBDCFDACFG $. + equsb3 $p |- ( [ y / x ] x = z <-> y = z ) $= + ( vw weq equequ1 sbievw2 ) ACEBCEDCEABDADCFDBCFG $. $( Substitution applied to the atomic wff with equality. Variant of ~ equsb3 . (Contributed by AV, 29-Jul-2023.) (Proof shortened by Wolf Lammen, 2-Sep-2023.) $) - equsb3r $p |- ( [ x / y ] z = y <-> z = x ) $= - ( vw weq equequ2 sbievw2 ) CBECAECDEBADBDCFDACFG $. + equsb3r $p |- ( [ y / x ] z = x <-> z = y ) $= + ( vw weq equequ2 sbievw2 ) CAECBECDEABDADCFDBCFG $. $} ${ - $d y z $. - $( Obsolete version of ~ equsb3 as of 2-Sep-2023. (Contributed by AV, + $d x z $. + $( Obsolete version of ~ equsb3r as of 2-Sep-2023. (Contributed by AV, 29-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) $) - equsb3rOLD $p |- ( [ x / y ] z = y <-> z = x ) $= - ( weq wsb equcom sbbii equsb3 3bitri ) CBDZBAEBCDZBAEACDCADJKBACBFGABCHAC + equsb3rOLD $p |- ( [ y / x ] z = x <-> z = y ) $= + ( weq wsb equcom sbbii equsb3 3bitri ) CADZABEACDZABEBCDCBDJKABCAFGABCHBC FI $. $} @@ -17271,7 +17271,7 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the (Revised by Steven Nguyen, 11-Jul-2023.) (Proof shortened by Steven Nguyen, 22-Jul-2023.) $) equsb1v $p |- [ y / x ] x = y $= - ( weq wsb equid equsb3 mpbir ) ABCABDBBCBEBABFG $. + ( weq wsb equid equsb3 mpbir ) ABCABDBBCBEABBFG $. $( Obsolete version of ~ equsb1v as of 22-Jul-2023. Version of ~ equsb1 with a disjoint variable condition, which neither requires ~ ax-12 nor @@ -17428,12 +17428,12 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the ( weq wel ax8 wi equcoms impbid ) ABDACEZBCEZABCFKJGBABACFHI $. ${ - $d w y z $. $d w x $. + $d w x z $. $d w y $. $( Substitution applied to an atomic membership wff. (Contributed by NM, 7-Nov-2006.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) Reduce axiom usage. (Revised by Wolf Lammen, 24-Jul-2023.) $) - elsb3 $p |- ( [ x / y ] y e. z <-> x e. z ) $= - ( vw wel elequ1 sbievw2 ) BCEACEDCEBADBDCFDACFG $. + elsb3 $p |- ( [ y / x ] x e. z <-> y e. z ) $= + ( vw wel elequ1 sbievw2 ) ACEBCEDCEABDADCFDBCFG $. $} ${ @@ -17524,13 +17524,13 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the ( weq wel ax9 wi equcoms impbid ) ABDCAEZCBEZABCFKJGBABACFHI $. ${ - $d w y z $. $d w x $. + $d w x z $. $d w y $. $( Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) Reduce axiom usage. (Revised by Wolf Lammen, 24-Jul-2023.) $) - elsb4 $p |- ( [ x / y ] z e. y <-> z e. x ) $= - ( vw wel elequ2 sbievw2 ) CBECAECDEBADBDCFDACFG $. + elsb4 $p |- ( [ y / x ] z e. x <-> z e. y ) $= + ( vw wel elequ2 sbievw2 ) CAECBECDEABDADCFDBCFG $. $} ${ @@ -22635,7 +22635,7 @@ derived from that of uniqueness ( ~ df-mo ). (Contributed by Wolf wi sp anim12d equtr2 syl6 exlimiv sylbi nfs1v pm3.21 imim1d alimd aleximi com12 sb8ev mof 3imtr4g moabs sylibr alcoms impbii ) ABFZAABCGZHZBCIZSZCJ ZBJUSVDBABKUSVCCACBDLUSABEIZSZBJZEMVCABENVGVCEVGVAVECEIZHVBVGAVEUTVHVFBTV - GUTVEBCGVHAVEBCOCBEPQUABCEUBUCUDUERRVCUSCBVCBJZCJZABMZUSSUSVJUTCMAVBSZBJZ + GUTVEBCGVHAVEBCOBCEPQUABCEUBUCUDUERRVCUSCBVCBJZCJZABMZUSSUSVJUTCMAVBSZBJZ CMVKUSVIUTVMCUTVIVMUTVCVLBABCUFUTAVAVBUTAUGUHUIUKUJABCDULABCDUMUNABUOUPUQ UR $. @@ -22648,7 +22648,7 @@ derived from that of uniqueness ( ~ df-mo ). (Contributed by Wolf nfmo anim12d equtr2 exlimiv sylbi nfs1v pm3.21 imim1d alimd com12 aleximi syl6 sb8e mof 3imtr4g moabs sylibr alcoms impbii ) ABFZAABCGZHZBCIZJZCKZB KUSVDBABLUSVCCACBDTUSABEIZJZBKZEMVCABENVGVCEVGVAVECEIZHVBVGAVEUTVHVFBOVGU - TVEBCGVHAVEBCPCBEQRUABCEUBUKUCUDSSVCUSCBVCBKZCKZABMZUSJUSVJUTCMAVBJZBKZCM + TVEBCGVHAVEBCPBCEQRUABCEUBUKUCUDSSVCUSCBVCBKZCKZABMZUSJUSVJUTCMAVBJZBKZCM VKUSVIUTVMCUTVIVMUTVCVLBABCUEUTAVAVBUTAUFUGUHUIUJABCDULABCDUMUNABUOUPUQUR $. $} @@ -23160,7 +23160,7 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not sb8eulem $p |- ( E! x ph <-> E! y [ y / x ] ph ) $= ( vz weq wb wal wex wsb weu nfv sb8v equsb3 sblbis albii nfbi sbequ eu6 equequ1 bibi12d cbvalv1 3bitri exbii 3bitr4i ) ABFGZHZBIZFJABCKZCFGZHZCIZ - FJABLUJCLUIUMFUIUHBDKZDIABDKZDFGZHZDIUMUHBDUHDMNUNUQDUGUPABDDBFOPQUQULDCU + FJABLUJCLUIUMFUIUHBDKZDIABDKZDFGZHZDIUMUHBDUHDMNUNUQDUGUPABDBDFOPQUQULDCU OUPCEUPCMRULDMDCGUOUJUPUKADCBSDCFUAUBUCUDUEABFTUJCFTUF $. $} @@ -25308,7 +25308,7 @@ the definition of class equality ( ~ df-cleq ). Its forward implication Lammen, 4-May-2023.) $) cvjust $p |- x = { y | y e. x } $= ( vz cv wel cab wceq wcel wb dfcleq wsb df-clab elsb3 bitr2i mpgbir ) ADZ - BAEZBFZGCAEZCDRHZICCPRJTQBCKSQCBLCBAMNO $. + BAEZBFZGCAEZCDRHZICCPRJTQBCKSQCBLBCAMNO $. $( $j usage 'cvjust' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13' 'df-clel'; $) $} @@ -26387,28 +26387,28 @@ the definition of class equality ( ~ df-cleq ). Its forward implication ( wcel wceq eleq2 biimpcd con3dimp ) ABDZBCEZACDZJIKBCAFGH $. ${ - $d y A $. $d w y $. $d w A $. $d x w $. + $d x A $. $d w x $. $d w A $. $d y w $. $( Substitution applied to an atomic wff (class version of ~ equsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010.) $) - eqsb3 $p |- ( [ x / y ] y = A <-> x = A ) $= - ( vw cv wceq eqeq1 sbievw2 ) BEZCFAEZCFDEZCFBADIKCGKJCGH $. + eqsb3 $p |- ( [ y / x ] x = A <-> y = A ) $= + ( vw cv wceq eqeq1 sbievw2 ) AEZCFBEZCFDEZCFABDIKCGKJCGH $. $} ${ - $d w y A $. $d w x $. + $d w x A $. $d w y $. $( Substitution applied to an atomic wff (class version of ~ elsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - clelsb3 $p |- ( [ x / y ] y e. A <-> x e. A ) $= - ( vw cv wcel eleq1w sbievw2 ) BECFAECFDECFBADBDCGDACGH $. + clelsb3 $p |- ( [ y / x ] x e. A <-> y e. A ) $= + ( vw cv wcel eleq1w sbievw2 ) AECFBECFDECFABDADCGDBCGH $. $d x y $. $( Obsolete version of ~ clelsb3 as of 29-Jul-2023. (Contributed by Wolf Lammen, 30-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.) $) - clelsb3vOLD $p |- ( [ x / y ] y e. A <-> x e. A ) $= - ( vw cv wcel wsb sbco2vv eleq1w sbievw sbbii 3bitr3i ) DECFZDBGZBAGMDAGBE - CFZBAGAECFZMDABHNOBAMODBDBCIJKMPDADACIJL $. + clelsb3vOLD $p |- ( [ y / x ] x e. A <-> y e. A ) $= + ( vw cv wcel wsb sbco2vv eleq1w sbievw sbbii 3bitr3i ) DECFZDAGZABGMDBGAE + CFZABGBECFZMDBAHNOABMODADACIJKMPDBDBCIJL $. $} ${ @@ -26429,7 +26429,7 @@ the definition of class equality ( ~ df-cleq ). Its forward implication 11-Jul-2011.) $) hblem $p |- ( z e. A -> A. x z e. A ) $= ( cv wcel wsb wal hbsb clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAEJ - CBDKZOPAQLM $. + BCDKZOPAQLM $. $} @@ -26512,7 +26512,7 @@ the definition of class equality ( ~ df-cleq ). Its forward implication 9-Jul-1994.) Avoid ~ ax-11 . (Revised by Wolf Lammen, 6-May-2023.) $) abbi2dv $p |- ( ph -> A = { x | ps } ) $= ( vy cab cv wcel wsb sbbidv clelsb3 bicomi df-clab 3bitr4g eqrdv ) AFDBCG - ZACHDIZCFJZBCFJFHZDIZTQIARBCFEKSUAFCDLMBFCNOP $. + ZACHDIZCFJZBCFJFHZDIZTQIARBCFEKSUACFDLMBFCNOP $. $} ${ @@ -26770,7 +26770,7 @@ choice between (what we call) a "definitional form" where the shorter 11-Aug-2016.) $) nfcrii $p |- ( y e. A -> A. x y e. A ) $= ( vz cv wcel wsb wal nfcriv nfsbv nf5ri clelsb3 albii 3imtr3i ) EFCGZEBHZ - QAIBFCGZRAIQAPEBAAECDJKLBECMZQRASNO $. + QAIBFCGZRAIQAPEBAAECDJKLEBCMZQRASNO $. $( Consequence of the not-free predicate. (Note that unlike ~ nfcr , this does not require ` y ` and ` A ` to be disjoint.) (Contributed by Mario @@ -26855,23 +26855,23 @@ choice between (what we call) a "definitional form" where the shorter $} ${ - $d w y $. $d w A $. $d w x $. - clelsb3f.1 $e |- F/_ y A $. + $d w x $. $d w A $. $d w y $. + clelsb3f.1 $e |- F/_ x A $. $( Substitution applied to an atomic wff (class version of ~ elsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.) (Proof shortened by Wolf Lammen, 7-May-2023.) $) - clelsb3f $p |- ( [ x / y ] y e. A <-> x e. A ) $= - ( vw cv wcel wsb nfcri sbco2 clelsb3 sbbii 3bitr3i ) EFCGZEBHZBAHNEAHBFCG - ZBAHAFCGNEABBECDIJOPBABECKLAECKM $. + clelsb3f $p |- ( [ y / x ] x e. A <-> y e. A ) $= + ( vw cv wcel wsb nfcri sbco2 clelsb3 sbbii 3bitr3i ) EFCGZEAHZABHNEBHAFCG + ZABHBFCGNEBAAECDIJOPABEACKLEBCKM $. $( Obsolete version of ~ clelsb3f as of 7-May-2023. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.) $) - clelsb3fOLD $p |- ( [ x / y ] y e. A <-> x e. A ) $= - ( vw cv wcel wsb nfcri sbco2 nfv eleq1w sbie sbbii 3bitr3i ) EFCGZEBHZBAH - PEAHBFCGZBAHAFCGZPEABBECDIJQRBAPREBREKEBCLMNPSEASEKEACLMO $. + clelsb3fOLD $p |- ( [ y / x ] x e. A <-> y e. A ) $= + ( vw cv wcel wsb nfcri sbco2 nfv eleq1w sbie sbbii 3bitr3i ) EFCGZEAHZABH + PEBHAFCGZABHBFCGZPEBAAECDIJQRABPREAREKEACLMNPSEBSEKEBCLMO $. $} ${ @@ -30664,7 +30664,7 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed ( vz cv wcel wa weu wreu wsb nfv sb8eu sban eubii df-reu anbi1i nfsb nfan clelsb3 weq eleq1w sbequ sbie syl6bb anbi12d cbveu bitri 3bitri 3bitr4i ) CJEKZALZCMZDJEKZBLZDMZACENBDENUQUPCIOZIMUOCIOZACIOZLZIMZUTUPCIUPIPQVAVDIU - OACIRSVEIJEKZVCLZIMUTVDVGIVBVFVCICEUDUASVGUSIDVFVCDVFDPACIDFUBUCUSIPIDUEZ + OACIRSVEIJEKZVCLZIMUTVDVGIVBVFVCCIEUDUASVGUSIDVFVCDVFDPACIDFUBUCUSIPIDUEZ VFURVCBIDEUFVHVCACDOBAIDCUGABCDGHUHUIUJUKULUMACETBDETUN $. $( Change the bound variable of a restricted at-most-one quantifier using @@ -30808,14 +30808,14 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed $} ${ - $d x y z $. $d y z ph $. $d x z ps $. + $d x y z $. $d x z ph $. $d y z ps $. sbralie.1 $e |- ( x = y -> ( ph <-> ps ) ) $. $( Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.) $) - sbralie $p |- ( [ x / y ] A. x e. y ph <-> A. y e. x ps ) $= - ( vz cv wral wsb cbvralsv sbbii raleq sbievw bitri sbco2vv ralbii ) ACDGZ - HZDCIZACFIZFCGZHZBDUAHZSTFQHZDCIUBRUDDCACFQJKUDUBDCTFQUALMNUBTFDIZDUAHUCT - FDUAJUEBDUAUEACDIBACDFOABCDEMNPNN $. + sbralie $p |- ( [ y / x ] A. y e. x ph <-> A. x e. y ps ) $= + ( vz cv wral wsb cbvralsv sbbii raleq sbievw bitri sbco2vv eqcoms ralbii + wb ) ADCGZHZCDIZADFIZFDGZHZBCUCHZUAUBFSHZCDIUDTUFCDADFSJKUFUDCDUBFSUCLMNU + DUBFCIZCUCHUEUBFCUCJUGBCUCUGADCIBADCFOABDCABRSUCEPMNQNN $. $} ${ @@ -32800,7 +32800,7 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed ( vy cv wceq weq wb wal eqeq1 eqeq2 bibi1d albidv alrimiv wsb stdpc4 sbbi eqsb3 sylbi bibi2i equsb1v biimp mpi syl impbii vtoclbg ) EFZCGZAEHZAFZCG ZIZAJZBCGUKBGZULIZAJEBDUHBCKUHBGZUMUPAUQUJUOULUHBUKLMNUIUNUIUMAUHCUKLOUNU - MAEPZUIUMAEQURUJAEPZULAEPZIZUIUJULAERVAUSUIIZUIUTUIUSEACSUAVBUSUIAEUBUSUI + MAEPZUIUMAEQURUJAEPZULAEPZIZUIUJULAERVAUSUIIZUIUTUIUSAECSUAVBUSUIAEUBUSUI UCUDTTUEUFUG $. $( Obsolete version of ~ pm13.183 as of 29-Apr-2023. (Contributed by @@ -32810,7 +32810,7 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed ( vy cv wceq wal eqeq1 eqeq2 bibi1d albidv alrimiv wsb stdpc4 sbbi bibi2i wb eqsb3 sylbi equsb1 biimp mpi syl impbii vtoclbg ) EFZCGZAFZUGGZUICGZRZ AHZBCGUIBGZUKRZAHEBDUGBCIUGBGZULUOAUPUJUNUKUGBUIJKLUHUMUHULAUGCUIJMUMULAE - NZUHULAEOUQUJAENZUKAENZRZUHUJUKAEPUTURUHRZUHUSUHUREACSQVAURUHAEUAURUHUBUC + NZUHULAEOUQUJAENZUKAENZRZUHUJUKAEPUTURUHRZUHUSUHURAECSQVAURUHAEUAURUHUBUC TTUDUEUF $. $} @@ -33504,7 +33504,7 @@ Such interpretation is rarely needed (see also ~ df-ral ). (Contributed wmo weq df-rmo sban clelsb3f anbi2i an4 ancom imbi1i nfcri r19.21 3bitr2i nfan mo3 3bitr4i ) ABDUABHDIZAJZBUBZAABCKZJZBCUCZLZCDMZBDMZABDUDURURBCKZJ ZVBLZCNZBNUQVDLZBNUSVEVIVJBVICHDIZUQVCLZLZCNVLCDMVJVHVMCVHVKUQJZVAJZVBLVN - VCLVMVGVOVBVGURVKUTJZJUQVKJZVAJVOVFVPURVFUQBCKZUTJVPUQABCUEVRVKUTCBDEUFOP + VCLVMVGVOVBVGURVKUTJZJUQVKJZVAJVOVFVPURVFUQBCKZUTJVPUQABCUEVRVKUTBCDEUFOP UGUQAVKUTUHVQVNVAUQVKUIOQUJVNVAVBRVKUQVCRQSVLCDTUQVCCDCBDFUKZULUMSURBCUQA CVSGUNUOVDBDTUPP $. $} @@ -34543,14 +34543,14 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use by Wolf Lammen, 29-Apr-2023.) $) eqsbc3 $p |- ( A e. V -> ( [. A / x ]. x = B <-> A = B ) ) $= ( vy cv wceq wsbc dfsbcq eqeq1 wsb sbsbc eqsb3 bitr3i vtoclbg ) AFCGZAEFZ - HZQCGZPABHBCGEBDPAQBIQBCJRPAEKSPAELEACMNO $. + HZQCGZPABHBCGEBDPAQBIQBCJRPAEKSPAELAECMNO $. $( Obsolete version of ~ eqsbc3 as of 29-Apr-2023. (Contributed by Andrew Salmon, 29-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) $) eqsbc3OLD $p |- ( A e. V -> ( [. A / x ]. x = B <-> A = B ) ) $= ( vy cv wceq wsbc dfsbcq eqeq1 wsb sbsbc eqsb3 bitr3i vtoclbg ) AFCGZAEFZ - HZQCGZPABHBCGEBDPAQBIQBCJRPAEKSPAELEACMNO $. + HZQCGZPABHBCGEBDPAQBIQBCJRPAEKSPAELAECMNO $. $} ${ @@ -34717,14 +34717,14 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use 30-Apr-2023.) $) sbcel1v $p |- ( [. A / x ]. x e. B <-> A e. B ) $= ( vy wcel wsbc cvv sbcex elex wsb dfsbcq2 eleq1 clelsb3 vtoclbg pm5.21nii - cv ) APCEZABFZBGEBCEZQABHBCIQADJDPZCERSDBGQADBKTBCLDACMNO $. + cv ) APCEZABFZBGEBCEZQABHBCIQADJDPZCERSDBGQADBKTBCLADCMNO $. $( Obsolete version of ~ sbcel1v as of 30-Apr-2023. (Contributed by NM, 17-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) $) sbcel1vOLD $p |- ( [. A / x ]. x e. B <-> A e. B ) $= ( vy wcel wsbc cvv sbcex elex wsb dfsbcq2 eleq1 clelsb3 vtoclbg pm5.21nii - cv ) APCEZABFZBGEBCEZQABHBCIQADJDPZCERSDBGQADBKTBCLDACMNO $. + cv ) APCEZABFZBGEBCEZQABHBCIQADJDPZCERSDBGQADBKTBCLADCMNO $. $} ${ @@ -35051,7 +35051,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use wal weq df-rmo sban clelsb3 anbi2i an4 ancom r19.21v 3bitr2i nfv nfan mo3 imbi1i 3bitr4i ) ABDFBGDHZAIZBJZAABCKZIZBCUAZLZCDMZBDMZABDUBUPUPBCKZIZUTL ZCTZBTUOVBLZBTUQVCVGVHBVGCGDHZUOVALZLZCTVJCDMVHVFVKCVFVIUOIZUSIZUTLVLVALV - KVEVMUTVEUPVIURIZIUOVIIZUSIVMVDVNUPVDUOBCKZURIVNUOABCUCVPVIURCBDUDNOUEUOA + KVEVMUTVEUPVIURIZIUOVIIZUSIVMVDVNUPVDUOBCKZURIVNUOABCUCVPVIURBCDUDNOUEUOA VIURUFVOVLUSUOVIUGNPUMVLUSUTQVIUOVAQPRVJCDSUOVACDUHUIRUPBCUOACUOCUJEUKULV BBDSUNO $. @@ -35064,7 +35064,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use wal weq df-rmo sban clelsb3 anbi2i an4 ancom r19.21v 3bitr2i nfv nfan mo3 imbi1i 3bitr4i ) ABDFBGDHZAIZBJZAABCKZIZBCUAZLZCDMZBDMZABDUBUPUPBCKZIZUTL ZCTZBTUOVBLZBTUQVCVGVHBVGCGDHZUOVALZLZCTVJCDMVHVFVKCVFVIUOIZUSIZUTLVLVALV - KVEVMUTVEUPVIURIZIUOVIIZUSIVMVDVNUPVDUOBCKZURIVNUOABCUCVPVIURCBDUDNOUEUOA + KVEVMUTVEUPVIURIZIUOVIIZUSIVMVDVNUPVDUOBCKZURIVNUOABCUCVPVIURBCDUDNOUEUOA VIURUFVOVLUSUOVIUGNPUMVLUSUTQVIUOVAQPRVJCDSUOVACDUHUIRUPBCUOACUOCUJEUKULV BBDSUNO $. $} @@ -47439,7 +47439,7 @@ This theorem is proved directly from set theory axioms (no set theory ( vy vz vw cv wnfc wel wal weq dtru ax-ext sps alimi mto wnf df-nfc sbnf2 wb wsb elsb4 bibi12i 2albii bitri albii alrot3 3bitri mtbir ) AAEZFZBCGZB DGZRZBHZDHZCHZUOCDIZCHCDJUNUPCUMUPDCDBKLMNUIBAGZAOZBHULDHCHZBHUOABUHPURUS - BURUQACSZUQADSZRZDHCHUSUQACDQVBULCDUTUJVAUKCABTDABTUAUBUCUDULBCDUEUFUG $. + BURUQACSZUQADSZRZDHCHUSUQACDQVBULCDUTUJVAUKACBTADBTUAUBUCUDULBCDUEUFUG $. $} $( The "distinctor" expression ` -. A. x x = y ` , stating that ` x ` and @@ -57138,8 +57138,8 @@ Definite description binder (inverted iota) ( vz vw weq wal cab cuni wsb cio nfv sb8 sbbi nfsb equsb3 nfxfr dfiota2 wb nfbi sbequ cbvalv1 sblbis albii 3bitri abbii unieqi 3eqtr4i ) ABEGZTZB HZEIZJABCKZCEGZTZCHZEIZJABLUNCLUMURULUQEULUKBFKZFHUKBCKZCHUQUKBFUKFMNUSUT - FCUSABFKZUJBFKZTCAUJBFOVAVBCABFCDPVBFEGZCFBEQVCCMRUARUTFMUKFCBUBUCUTUPCUJ - UOABCCBEQUDUEUFUGUHABESUNCESUI $. + FCUSABFKZUJBFKZTCAUJBFOVAVBCABFCDPVBFEGZCBFEQVCCMRUARUTFMUKFCBUBUCUTUPCUJ + UOABCBCEQUDUEUFUGUHABESUNCESUI $. $} ${ @@ -70776,15 +70776,15 @@ last three are the basis and the induction hypotheses (for successor and tfinds2 $p |- ( x e. On -> ( ta -> ph ) ) $= ( wi wsbc sbcie cvv elv wb sbcimg c0 0ex wceq imbi2d mpbir con0 wcel csuc a2d sbcth mpbi sbcel1v 3imtr3i vex weq bicomd equcoms sucex sbcbii sbcco2 - cv suceq bitr3i 3imtr3g wral wlim wsb sbsbc sbralie r19.21v limeq syl5bir - syl5bi tfindes ) EANZFGVOFUAOEBNZKVOVPFUAUBFVAZUAUCABEHUDPUEVQUFUGZECNZGV - QOZEDNZGVQOZVOVOFVQUHZOZGVAZUFUGZGVQOZVSWANZGVQOZVRVTWBNZWFWHNZGVQOZWGWIN - ZWLFWKGVQQWFECDLUIUJRWLWMSFWFWHGVQQTRUKGVQUFULWIWJSFVSWAGVQQTRUMVSVOGVQFU - NGFUOCAECASFGFGUOACIUPUQUDZPWBVOFWEUHZOZGVQOWDWPWAGVQVOWAFWOWEGUNZURVQWOU - CADEJUDPUSVOFGWCWOVQWEVBUTVCVDVOFWEVEZVSGVQVEZFWEOZWEVFZVOFWEOZWTWSFGVGWR - WSFGVHVSVOGFWNVIVCVQVFZFWEOZWSVONZFWEOZXAWTXBNZXCXENZFWEOZXDXFNZXIGXHFWEQ - WSECGVQVEZNXCVOECGVQVJXCEXKAMUIVMUJRXIXJSGXCXEFWEQTRUKXCXAFWEWQVQWEVKPXFX - GSGWSVOFWEQTRUMVLVN $. + cv suceq bitr3i 3imtr3g wral wlim wsb sbsbc eqcoms sbralie r19.21v syl5bi + limeq syl5bir tfindes ) EANZFGVPFUAOEBNZKVPVQFUAUBFVAZUAUCABEHUDPUEVRUFUG + ZECNZGVROZEDNZGVROZVPVPFVRUHZOZGVAZUFUGZGVROZVTWBNZGVROZVSWAWCNZWGWINZGVR + OZWHWJNZWMFWLGVRQWGECDLUIUJRWMWNSFWGWIGVRQTRUKGVRUFULWJWKSFVTWBGVRQTRUMVT + VPGVRFUNGFUOCAECASFGFGUOACIUPUQUDZPWCVPFWFUHZOZGVROWEWQWBGVRVPWBFWPWFGUNZ + URVRWPUCADEJUDPUSVPFGWDWPVRWFVBUTVCVDVPFWFVEZVTGVRVEZFWFOZWFVFZVPFWFOZXAW + TFGVGWSWTFGVHVTVPFGVTVPSWFVRWOVIVJVCVRVFZFWFOZWTVPNZFWFOZXBXAXCNZXDXFNZFW + FOZXEXGNZXJGXIFWFQWTECGVRVEZNXDVPECGVRVKXDEXLAMUIVLUJRXJXKSGXDXFFWFQTRUKX + DXBFWFWRVRWFVMPXGXHSGWTVPFWFQTRUMVNVO $. $} ${ @@ -99021,7 +99021,7 @@ our Axiom of Choice (in the form of ~ ac2 ). The proof does not depend anbi12i 3bitri anbi2i 19.42v bitr2i 3bitr2i ) EDLUAZCMVFBHNZGOZFNZMVFVHMZ FNVFBMHNZGOZFNCVIVFCGPZFPZEPZUBZUCZGUDZFDPZUIGFLGELMZHFLHELMZHGUEZQZMZHNZ GOZFVSUIZVIKVRWFFVSVRVQVQGHUFZGHUEZQZHNZMZGOWFVQGHVQHUGUHWLWEGWLVTWCHNZMW - EVQVTWKWMVMVNVOUJWJWCHWHWAWIWBWHHPZVPUCWAHGVPUKWNVNVOUJRGHULUMSUTVTWCHTUN + EVQVTWKWMVMVNVOUJWJWCHWHWAWIWBWHHPZVPUCWAGHVPUKWNVNVOUJRGHULUMSUTVTWCHTUN UORUPWGFDLZWFQZFNVIWFFVSUQVHWPFVHWOWEQZGOWPVGWQGVGWOWDQZHNWQBWRHJSWOWDHUR RUOWOWEGUSRSUNVAVBVFVHFTVJVLFVLVFVGMZGOVJVKWSGVFBHTUOVFVGGVCVDSVE $. @@ -459712,7 +459712,7 @@ and the expression ( x e. A /\ x e. B ) ` . sban sbf anbi2i bitr4i equsb3 imbi12i bitri sbalv albii 3bitri ) ABGAABDH ZIZBDJZKZDLZBLUQBCHZCLABCHZUMIZCDJZKZDLZCLABDFMUQBCUPCDUNUOCAUMCEABDCENOU OCPQRSURVCCUPVBBCDUPBCHUNBCHZUOBCHZKVBUNUOBCTVDUTVEVAVDUSUMBCHZIUTAUMBCUC - UMVFUSVFUMUMBCABDUAUDUBUEUFCBDUGUHUIUJUKUL $. + UMVFUSVFUMUMBCABDUAUDUBUEUFBCDUGUHUIUJUKUL $. $} ${ @@ -460417,7 +460417,7 @@ Class abstractions (a.k.a. class builders) VBQUUGYECUUEXJMZUPUUBCYDUUEXJVCUUHYKYECYHXJYKYCIPVDXIYHDRUMVEUNVFVJUUAYEY FYKYTYGVGVHUUAAYSUUCYKNZYSAYGVIUUDAYSSZYFYKVKZUUIAXIUDHZSZXJXIIPKZDLZVKZO ZCGTZUUJUUKOZUUQCGFVLUURUUMCGTZUUPCGTZOUUSUUMUUPCGVMUUJUUTUUKUVAUUTACGTZU - ULCGTZSUUJAUULCGVNUVBAUVCYSACGVOGCUDVPVQVRUVAUUPCYCVSZCYCXJVTZCYCUUOVTZVK + ULCGTZSUUJAUULCGVNUVBAUVCYSACGVOCGUDVPVQVRUVAUUPCYCVSZCYCXJVTZCYCUUOVTZVK ZUUKUUPCGWAUVDUVGWBGCYCXJUUOWDWCWEUVEYFUVFYKCYCDWOUVFCYCUUNVTZDLZCYCXIVTZ IPKZDLYKUVFUVINGCYCUUNWDDWFWEUVHUVKDUVHUVKNGCYCXIIPWDWGWEWHUVKYHDUVJYCIPC YCGWIWJWKWHWLWMWNWPWQWRYFYKWSWTXAXBXCXFXDXE $. @@ -461444,7 +461444,7 @@ Class abstractions (a.k.a. class builders) cvv sbceq1g elv imbi12i mpbi suppss2 syl5eqss ) ADBCNZGOPMBDMUAZCUGZNZGOP FVHVKGODMBCVJIMBUBMCUBDVICUCDVICUDUEUFABVJMEFGADUABFUHZUIZQZCGUJZRZDMSZAV IVLUIZQZVJGUJZRZVPDMKUKVQVNDMSZVODMSZRWAVNVODMULWBVSWCVTWBADMSZVMDMSZQVSA - VMDMUMWDAWEVRADMHUNMDVLDBFIJUOUPUQTWCVODVIURZVTVODMUSWFVTUTMDVICGVAVBVCTV + VMDMUMWDAWEVRADMHUNDMVLDBFIJUOUPUQTWCVODVIURZVTVODMUSWFVTUTMDVICGVAVBVCTV DTVELVFVG $. $} @@ -461731,7 +461731,7 @@ Class abstractions (a.k.a. class builders) sbimi wsbc sbsbc sbcel12 csbgfi 3imtr3i ralrimiva nfcsb1v csbeq1a cbvmptf vex eleq2i fmpt sylib feq1i sylibr ) ACEBCDUAZMZCEFMABLNZDOZEPZLCUBVDAVGL CABNCPZQZBLRZDEPZBLRZAVECPZQZVGVIVKBLJUGVJABLRZVHBLRZQVNAVHBLUCVOAVPVMABL - GUDLBCHUEUFSVLVKBVEUHZVGVKBLUIVQVFBVEEOZPVGBVEDEUJVREVFBVEELUQIUKURSSULUM + GUDBLCHUEUFSVLVKBVEUHZVGVKBLUIVQVFBVEEOZPVGBVEDEUJVREVFBVEELUQIUKURSSULUM LCEVFVCBLCDVFHLCTLDTBVEDUNBVEDUOUPUSUTCEFVCKVAVB $. $} @@ -462533,7 +462533,7 @@ its graph has a given second element (that is, function value). JCPAWMJCAWFCQZRZWLKCWOWGCQZRZWHWIWJUGSMZUFZWLWOWSKCAWSKCPZJCABCDUDWTJCPIB CDJKGUEUHUIUIWQWRWKWHWQWRWKAWNWPWRWKAWNWPWRUJRWRWISOZWKAWNWPWRUKAWPWNXAWR ABLCQZRZBJTZDSOZBJTZWOXAXCXEBJXCDESULUMZQXEHDESUNUOUPXDABJTZXBBJTZRWOAXBB - JUSXHAXIWNABJFUQJBCGURUTVAXFXEBWFVBWIBWFSNZOXAXEBJVCBWFDSVDXJSWIBWFVEVFVJ + JUSXHAXIWNABJFUQBJCGURUTVAXFXEBWFVBWIBWFSNZOXAXEBJVCBWFDSVDXJSWIBWFVEVFVJ VGVHWRXARWIWJUMZSOZWKWRXAXLWRWIXKSWRWIXKMWIWJVIVKVLVMWIWJVNUOWAVOVPVQVRVS VSABCDJKWEXGFGBCDVTWEWBHWCWD $. $} @@ -478803,7 +478803,7 @@ embedding at each step ( ` ZZ ` , ` QQ ` and ` RR ` ). It would be VMYGVNOZAYFVNOXQROYMVOJKUCVPXQYFRVQVRPVSVTWAXTXRXSMVPWBWCABUOOBYJXSWDYAXT WEGADBCYJXSFEDYJQHYKVGBXSUOWFWGANIBDIVBZCWHZUFZMLBYOIUDYAYBABYOIGYICSOZWI ZDITZAYNBOZVCZYOSOZWIZYRDIYIYJSCYJWKSWJWLWMHVEWNYSYIDITZYQDITZWIUUCYIYQDI - WOUUDUUAUUEUUBUUDADITZYHDITZVCUUAAYHDIWPUUFAUUGYTADIFWQIDBEWRWSWTUUEYQDYN + WOUUDUUAUUEUUBUUDADITZYHDITZVCUUAAYHDIWPUUFAUUGYTADIFWQDIBEWRWSWTUUEYQDYN XAZUUBYQDIXBUUHUUBXCIDYNCSRXDXEWTXFWTXGXHXSYPNMDIBCYOEIBQZICQZDYNCXIZDYNC XJZXKXNBCYODIUULUUIEUUJUUKXOXLXM $. $} @@ -481275,7 +481275,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry YJEXOYEEUBZXOQZRAYKIQZYJAYDYLVAYEXOIYKYEISUOZXOITIPGUCUDZUOZYEYNRSXOIXNVB YEYNVDVEYEYPRZXOYOIYQXNYOQGXNVFOQXOYOTYQXNIYOAYDYPVGYEYPVDZVHXNPGVIXNPGVJ VKYRVLAYNYPVMZYDLUTVNVOYEFEVPZYGFEVPZAYMRZYJYEYGFENVQYTAFEVPZYDFEVPZRUUBA - YDFEVRUUCAUUDYMAFEVSEFIVTWAWBUUAYGFYKWGZFYKBWCZDQZYJYGFEWDUUEUUGWEEFYKBDW + YDFEVRUUCAUUDYMAFEVSFEIVTWAWBUUAYGFYKWGZFYKBWCZDQZYJYGFEWDUUEUUGWEEFYKBDW FWHWIUUFCDUUFEYKCWCCFEYKBCEBWJJKWKECWLWMWNWRWOWPWQCDEXNWSWPBXPDWTXHWQAIST ZSUKULUMYCAYSUUHLYNUUHYPISXAYPUUHYOSTGVBIYOSXBXCXDUSXEISXFXIABCEFGIJKLXGF IXQDHXJXKXL $. @@ -488098,7 +488098,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry VEWTXJXPWTXJXNSZDXIUKXPWTXGYCDXIWTXDXIRZTZXFUDYEWTXDUDXHUJUIZRZTZXFVGRZ WTYDYGWTXIYFXDXIYFVHWTXHVIVJVKVLWTQUBZYFRZTZQDVQZYJXEUCZVGRZQDVQYHYIYLY OQDYLYNYLABCDFYJGHIJKLMNOWTYKVMYKYJVNRWTYJUDXHVRVOVPVSVTYMWTQDVQZYKQDVQ - ZTYHWTYKQDWAYPWTYQYGWTQDWBDQYFWCWDWEYOYIQDYIQWIQDWJYNXFVGYJXDXEWFWGWHWK + ZTYHWTYKQDWAYPWTYQYGWTQDWBQDYFWCWDWEYOYIQDYIQWIQDWJYNXFVGYJXDXEWFWGWHWK WLYEWMWNWOXNDXIWPWQWRWSWE $. $} @@ -524831,9 +524831,9 @@ A Fne if ( S = (/) , { X } , U. S ) ) $= See ~ negsym1 for more information. (Contributed by Anthony Hart, 11-Sep-2011.) $) - subsym1 $p |- ( [ x / y ] [ x / y ] F. -> [ x / y ] ph ) $= - ( wfal wsb weq wi wa wex fal intnan nex dfsb1 mtbir pm2.21i ) DCBEZCBEZACBE - QCBFZPGZRPHZCIZHUASTCPRPRDGZRDHZCIZHUDUBUCCDRJKLKDCBMNKLKPCBMNO $. + subsym1 $p |- ( [ y / x ] [ y / x ] F. -> [ y / x ] ph ) $= + ( wfal wsb weq wi wa wex fal intnan nex dfsb1 mtbir pm2.21i ) DBCEZBCEZABCE + QBCFZPGZRPHZBIZHUASTBPRPRDGZRDHZBIZHUDUBUCBDRJKLKDBCMNKLKPBCMNO $. $( (End of Anthony Hart's mathbox.) $) @@ -530885,7 +530885,7 @@ nonfreeness hypothesis (for the sake of illustration). (Contributed by bj-nfcf $p |- ( F/_ x A <-> A. y F/ x y e. A ) $= ( vz wnfc cv wcel wnf wal df-nfc wsb nfcri nfnf sb8 bj-sbnf clelsb3 nfbii bitri albii ) ACFEGCHZAIZEJZBGCHZAIZBJZAECKUCUBEBLZBJUFUBEBUABABECDMNOUGU - EBUGUAEBLZAIUEUAAEBPUHUDABECQRSTSS $. + EBUGUAEBLZAIUEUAAEBPUHUDAEBCQRSTSS $. $} ${ @@ -534503,7 +534503,7 @@ Complex numbers (supplements) SWETUVAUUTUUQOUVBBYAYASWFTYGYBMZBYARZUURBYARZUUSUUTMUURUVCUURQZBYARZUVD UVEQZUVAUVGUVBUVFBYASUVCYSUUBYOYBUUBYSOYGUULWGUVCUUBYOQZAUVCANYCUVIYBAD VBUUBYCYOUUCYOBYOUUDUUEWHWIWJWKWIXBWLTUVAUVGUVHOUVBUVCUURBYASWMTWNYGYBB - YAWOUURBYAUVBYSYOBYSBWPBIYEBYDYCBWQWRWSWTXAXCXDXEXFIAYEUSXGXHXIAIAXJUUP + YAWOUURBYAUVBYSYOBYSBWPBIYEBYDYCBWQWRWSWTXAXCXDXEXFIAYEUSXGXHXIIAAXJUUP IAXLXCTXKXMXNXO $. $} @@ -537256,7 +537256,7 @@ dependency is expressed in our hypothesis (called implicit wl-equsb3 $p |- ( -. A. y y = z -> ( [ x / y ] y = z <-> x = z ) ) $= ( vw weq wal wn wsb nfna1 nfeqf2 wb wi equequ1 a1i sbbidv sbco2vv 3bitr3g sbied equsb3 ) BCEZBFGZTBDHZDAHDCEZDAHTBAHACEUAUBUCDAUATUCBDTBIBCDJBDETUC - KLUABDCMNROTBADPADCSQ $. + KLUABDCMNROTBADPDACSQ $. $} $( Substitution applied to an atomic wff. The distinctor antecedent is more @@ -537484,7 +537484,7 @@ dependency is expressed in our hypothesis (called implicit sylbi nfs1v pm3.3 com23 sps aleximi alcoms moabs wl-sb8et wl-mo2t imbi12d ex syl5bb syl5ibr impbid ) ACEZBFZABGZAABCHZIZBCJZKZCFZBFZVGVHVMBVFBLZABM VGVHVMVGVHIVLCVGVHCVFCBACNTVGACBVOVFBOPQVHVLVGVHABDJZKZBFZDRVLABDUAVRVLDV - RVJVPCDJZIVKVRAVPVIVSVQBOVRVIVPBCHVSAVPBCUBCBDUCUDUEBCDUFUGUHUKUIUJVBSVNV + RVJVPCDJZIVKVRAVPVIVSVQBOVRVIVPBCHVSAVPBCUBBCDUCUDUEBCDUFUGUHUKUIUJVBSVNV HVGVICRZAVKKZBFZCRZKZVLWDCBVLBFZVIWBCWEVIWABVLBLABCULVLVIWAKBVLAVIVKAVIVK UMUNUOSUPUQVHABRZVHKVGWDABURVGWFVTVHWCABCUSABCUTVAVCVDVE $. $} @@ -537497,8 +537497,8 @@ dependency is expressed in our hypothesis (called implicit ( vu vv wnf wal weq wb wex wsb weu nfnf1 nfal equsb3 sblbis nfa1 sp nfsbd eu6 nfvd nfbid nfxfrd wi sbequ a1i cbvald nfv bicomi albii 3bitr3g exbidv sb8 3bitr4g ) ACFZBGZABDHZIZBGZDJABCKZCDHZIZCGZDJABLUTCLUPUSVCDUPURBEKZEG - ZURBCKZCGUSVCUPVDVFECUOCBACMNVDABEKZEDHZIUPCUQVHABEEBDOPUPVGVHCUPABECUOBQ - UOBRSUPVHCUAUBUCECHVDVFIUDUPURECBUEUFUGUSVEURBEUREUHUMUIVFVBCUQVAABCCBDOP + ZURBCKZCGUSVCUPVDVFECUOCBACMNVDABEKZEDHZIUPCUQVHABEBEDOPUPVGVHCUPABECUOBQ + UOBRSUPVHCUAUBUCECHVDVFIUDUPURECBUEUFUGUSVEURBEUREUHUMUIVFVBCUQVAABCBCDOP UJUKULABDTUTCDTUN $. $} @@ -537944,7 +537944,7 @@ can be simplified (see ~ wl-dfrexf , ~ wl-dfrexv ). ( vz weq wi wl-ral wex cv wcel wsb wal wl-rmo wmo wl-dfralsb imbi2i bitri wa sbim equsb3 impexp bitr4i albii exbii df-wl-rmo df-mo 3bitr4i ) ABEFZG ZBDHZEICJDKZABCLZSZCEFZGZCMZEIABDNUNCOUKUQEUKULUJBCLZGZCMUQUJBCDPUSUPCUSU - LUMUOGZGUPURUTULURUMUIBCLZGUTAUIBCTVAUOUMCBEUAQRQULUMUOUBUCUDRUEABEDUFUNC + LUMUOGZGUPURUTULURUMUIBCLZGUTAUIBCTVAUOUMBCEUAQRQULUMUOUBUCUDRUEABEDUFUNC EUGUH $. $} @@ -538050,7 +538050,7 @@ can be simplified (see ~ wl-dfrexf , ~ wl-dfrexv ). = { x | ( x e. A /\ ph ) } $= ( vy vz wl-crab cv wcel wsb cab wl-dfrabsb clelsb3 bitr4i sbco2vv anbi12i wa df-clab sban bitri 3bitr4i eqriv eqtri ) ABCFDGCHZABDIZPZDJZBGCHZAPZBJ - ZABDCKEUFUIUCDEIZUDDEIZPZUGBEIZABEIZPZEGZUFHZUPUIHZUJUMUKUNUJUPCHUMEDCLEB + ZABDCKEUFUIUCDEIZUDDEIZPZUGBEIZABEIZPZEGZUFHZUPUIHZUJUMUKUNUJUPCHUMDECLBE CLMABEDNOUQUEDEIULUEEDQUCUDDERSURUHBEIUOUHEBQUGABERSTUAUB $. $} @@ -538062,7 +538062,7 @@ can be simplified (see ~ wl-dfrexf , ~ wl-dfrexv ). 29-May-2023.) $) wl-clelsb3df $p |- ( ph -> ( [ x / y ] y e. A <-> x e. A ) ) $= ( vw cv wcel wsb nfv nfcrd sbco2d clelsb3 sbbii 3bitr3g ) AGHDIZGCJZCBJQG - BJCHDIZCBJBHDIAQGBCAGKEACGDFLMRSCBCGDNOBGDNP $. + BJCHDIZCBJBHDIAQGBCAGKEACGDFLMRSCBGCDNOGBDNP $. $} ${ @@ -538075,7 +538075,7 @@ can be simplified (see ~ wl-dfrexf , ~ wl-dfrexv ). ( vy vz wnfc wl-crab cv wcel wsb wa cab wl-dfrabsb nfnfc1 id wl-clelsb3df clelsb3 df-clab sban bitri syl6rbbr wb sbco2vv a1i anbi12d 3bitr4g syl5eq eqrdv ) BCFZABCGDHCIZABDJZKZDLZBHCIZAKZBLZABDCMUIEUMUPUIUJDEJZUKDEJZKZUNB - EJZABEJZKZEHZUMIZVCUPIZUIUQUTURVAUIUTVCCIUQUIEBCBCNUIOPEDCQUAURVAUBUIABED + EJZABEJZKZEHZUMIZVCUPIZUIUQUTURVAUIUTVCCIUQUIEBCBCNUIOPDECQUAURVAUBUIABED UCUDUEVDULDEJUSULEDRUJUKDESTVEUOBEJVBUOEBRUNABESTUFUHUG $. $} @@ -642265,8 +642265,8 @@ the concept (illegal in our notation ) ` ( ph `` ps ) ` with $( Lemma for frege102 (via ~ frege92 ). Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) $) - frege53b $p |- ( [ x / y ] ph -> ( x = z -> [ z / y ] ph ) ) $= - ( weq wsb wi frege52b ax-frege8 ax-mp ) BDEZACBFZACDFZGGLKMGGABDCHKLMIJ $. + frege53b $p |- ( [ y / x ] ph -> ( y = z -> [ z / x ] ph ) ) $= + ( weq wsb wi frege52b ax-frege8 ax-mp ) CDEZABCFZABDFZGGLKMGGACDBHKLMIJ $. $( Reflexive equality of classes. Identical to ~ eqid . Justification for ~ ax-frege54c . (Contributed by RP, 24-Dec-2019.) $) @@ -642295,13 +642295,13 @@ the concept (illegal in our notation ) ` ( ph `` ps ) ` with (Contributed by RP, 24-Dec-2019.) $) frege55lem1b $p |- ( ( ph -> [ x / y ] y = z ) -> ( ph -> x = z ) ) $= - ( weq wsb equsb3 biimpi imim2i ) CDECBFZBDEZAJKBCDGHI $. + ( weq wsb equsb3 biimpi imim2i ) CDECBFZBDEZAJKCBDGHI $. $} $( Lemma for ~ frege55b . Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) $) frege55lem2b $p |- ( x = y -> [ y / z ] z = x ) $= - ( weq wsb wi frege54cor1b frege53b ax-mp ) CADZCAEABDJCBEFACGJACBHI $. + ( weq wsb wi frege54cor1b frege53b ax-mp ) CADZCAEABDJCBEFACGJCABHI $. ${ $d x z $. $d y z $. @@ -642358,9 +642358,9 @@ the concept (illegal in our notation ) ` ( ph `` ps ) ` with collection _From Frege to Goedel_, this proof has the ~ frege12 incorrectly referenced where ~ frege30 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) $) - frege59b $p |- ( [ x / y ] ph - -> ( -. [ x / y ] ps -> -. A. y ( ph -> ps ) ) ) $= - ( wi wal wsb wn frege58bcor frege30 ax-mp ) ABEDFZADCGZBDCGZEEMNHLHEEABDCIL + frege59b $p |- ( [ y / x ] ph + -> ( -. [ y / x ] ps -> -. A. x ( ph -> ps ) ) ) $= + ( wi wal wsb wn frege58bcor frege30 ax-mp ) ABECFZACDGZBCDGZEEMNHLHEEABCDIL MNJK $. $( Swap antecedents of ~ ax-frege58b . Proposition 60 of [Frege1879] p. 52. @@ -642381,24 +642381,24 @@ the concept (illegal in our notation ) ` ( ph `` ps ) ` with inference ~ barbara when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) $) - frege62b $p |- ( [ x / y ] ph - -> ( A. y ( ph -> ps ) -> [ x / y ] ps ) ) $= - ( wi wal wsb frege58bcor ax-frege8 ax-mp ) ABEDFZADCGZBDCGZEELKMEEABDCHKLMI + frege62b $p |- ( [ y / x ] ph + -> ( A. x ( ph -> ps ) -> [ y / x ] ps ) ) $= + ( wi wal wsb frege58bcor ax-frege8 ax-mp ) ABECFZACDGZBCDGZEELKMEEABCDHKLMI J $. $( Lemma for ~ frege91 . Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) $) - frege63b $p |- ( [ x / y ] ph + frege63b $p |- ( [ y / x ] ph -> ( ps - -> ( A. y ( ph -> ch ) -> [ x / y ] ch ) ) ) $= - ( wsb wi wal frege62b frege24 ax-mp ) AEDFZACGEHCEDFGZGLBMGGACDEILMBJK $. + -> ( A. x ( ph -> ch ) -> [ y / x ] ch ) ) ) $= + ( wsb wi wal frege62b frege24 ax-mp ) ADEFZACGDHCDEFGZGLBMGGACDEILMBJK $. $( Lemma for ~ frege65b . Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) $) frege64b $p |- ( ( [ x / y ] ph -> [ z / y ] ps ) -> ( A. y ( ps -> ch ) -> ( [ x / y ] ph -> [ z / y ] ch ) ) ) $= - ( wsb wi wal frege62b frege18 ax-mp ) BEFGZBCHEIZCEFGZHHAEDGZMHNPOHHHBCFEJM + ( wsb wi wal frege62b frege18 ax-mp ) BEFGZBCHEIZCEFGZHHAEDGZMHNPOHHHBCEFJM NOPKL $. $( A kind of Aristotelian inference. This judgement replaces the mode of @@ -652144,7 +652144,7 @@ elements and the subgroup containing only the identity ( ~ simpgnsgbid ). $( If ` x = y ` always implies ` x = z ` , then ` y = z ` . (Contributed by Andrew Salmon, 2-Jun-2011.) $) sbeqal1 $p |- ( A. x ( x = y -> x = z ) -> y = z ) $= - ( weq wi wal wsb sb2 equsb3 sylib ) ABDACDZEAFKABGBCDKABHBACIJ $. + ( weq wi wal wsb sb2 equsb3 sylib ) ABDACDZEAFKABGBCDKABHABCIJ $. $d x z $. sbeqal1i.1 $e |- ( x = y -> x = z ) $. @@ -671507,7 +671507,7 @@ closed under the multiplication ( ' X ' ) of a finite number of XOXFUFYBXDXNUDYBXNXMBXADESTZUQZXDYBXMACQXAHABCYCQHABUBCRZUHZDELAWTYENURUS JUTZVAVBYBYAYDQRXMYDVCAYAVDZYBYDBXADUQZESTZQYDYJVCOBXADESVEVFVGZYBYIEYBDQ RZBOVHZYIQRZYFYLUMZYBYMUMLYBYFBOVHZYOYMYPABOVHZYEBOVHZUHYBAYEBOVIYQAYRYAA - BOABVJVKOBCVLVMVNYOBOVHYOYPYMUMYOBOYOBLVOVKYFYLBOVPVQVSVRYMYLBXAVTZYNYLBO + BOABVJVKBOCVLVMVNYOBOVHYOYPYMUMYOBOYOBLVOVKYFYLBOVPVQVSVRYMYLBXAVTZYNYLBO WAYSYNWIOBXADQVEWBVGVNWCZAWTYANURUSWDBXAYCCHQJWEWFYBXDYJYDYBXCYIESYBYAYNX CYIVCYHYTBXADCGQIWEWFWJYKWGWHWKWLWSWMWNWOWPAUAPOCFEGABCDQGLIUTKMWQAUAPOCF UNHYGKMWQWR $. @@ -725844,7 +725844,7 @@ valid cases ( ` (/) ` is the last symbol) and invalid cases ( ` (/) ` icheq $p |- [ x <> y ] x = y $= ( vz weq wich wsb wb equsb3r 2sbbii equsb3 sbbii equcom bitri 3bitri gen2 wal df-ich mpbir ) ABDZABESBCFZABFCAFZSGZBPAPUBABUAACDZABFZCAFBCDZCAFZSTU - CCABACBAHIUDUECABACJKUFBADSACBHBALMNOSABCQR $. + CCABABCAHIUDUECAABCJKUFBADSCABHBALMNOSABCQR $. $} ${ From dad1c24dcca1b468c8a59d345dbc35e3cb7a4bc6 Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Thu, 12 Oct 2023 00:42:04 +0200 Subject: [PATCH 2/3] replaced '|- ( [ x / y ]' with '|- ( [ y / x ]' in iset.mm --- iset.mm | 148 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 74 insertions(+), 74 deletions(-) diff --git a/iset.mm b/iset.mm index 10b00b5c5f..87bcc92827 100644 --- a/iset.mm +++ b/iset.mm @@ -15149,20 +15149,20 @@ Predicate calculus with distinct variables (cont.) $} ${ - $d y z $. $d x y $. + $d x z $. $d x y $. $( Lemma for ~ equsb3 . (Contributed by NM, 4-Dec-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - equsb3lem $p |- ( [ x / y ] y = z <-> x = z ) $= - ( cv wceq ax-17 equequ1 sbieh ) BDCDZEADIEZBAJBFBACGH $. + equsb3lem $p |- ( [ y / x ] x = z <-> y = z ) $= + ( cv wceq ax-17 equequ1 sbieh ) ADCDZEBDIEZABJAFABCGH $. $} ${ - $d w y z $. $d w x $. + $d w x z $. $d w y $. $( Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.) $) - equsb3 $p |- ( [ x / y ] y = z <-> x = z ) $= - ( vw weq wsb equsb3lem sbbii ax-17 sbco2v 3bitr3i ) BCEZBDFZDAFDCEZDAFLBA - FACEMNDADBCGHLBADLDIJADCGK $. + equsb3 $p |- ( [ y / x ] x = z <-> y = z ) $= + ( vw weq wsb equsb3lem sbbii ax-17 sbco2v 3bitr3i ) ACEZADFZDBFDCEZDBFLAB + FBCEMNDBADCGHLABDLDIJDBCGK $. $} ${ @@ -15400,26 +15400,26 @@ Predicate calculus with distinct variables (cont.) $} ${ - $d w y z $. $d w x $. + $d w x z $. $d w y $. $( Substitution applied to an atomic membership wff. (Contributed by NM, 7-Nov-2006.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - elsb3 $p |- ( [ x / y ] y e. z <-> x e. z ) $= + elsb3 $p |- ( [ y / x ] x e. z <-> y e. z ) $= ( vw wel wsb ax-17 elequ1 sbieh sbbii sbco2h bitr3i wb equsb1 sbimi ax-mp - weq sbbi mpbi sbh 3bitri ) BCEZBAFZDCEZDAFZACEZDAFZUFUCUDDBFZBAFUEUHUBBAU - DUBDBUBDGDBCHIJUDDABUDBGKLUDUFMZDAFZUEUGMDAQZDAFUJDANUKUIDADACHOPUDUFDARS - UFDAUFDGTUA $. + weq sbbi mpbi sbh 3bitri ) ACEZABFZDCEZDBFZBCEZDBFZUFUCUDDAFZABFUEUHUBABU + DUBDAUBDGDACHIJUDDBAUDAGKLUDUFMZDBFZUEUGMDBQZDBFUJDBNUKUIDBDBCHOPUDUFDBRS + UFDBUFDGTUA $. $} ${ - $d w y z $. $d w x $. + $d w x z $. $d w y $. $( Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - elsb4 $p |- ( [ x / y ] z e. y <-> z e. x ) $= + elsb4 $p |- ( [ y / x ] z e. x <-> z e. y ) $= ( vw wel wsb ax-17 elequ2 sbieh sbbii sbco2h bitr3i wb equsb1 sbimi ax-mp - weq sbbi mpbi sbh 3bitri ) CBEZBAFZCDEZDAFZCAEZDAFZUFUCUDDBFZBAFUEUHUBBAU - DUBDBUBDGDBCHIJUDDABUDBGKLUDUFMZDAFZUEUGMDAQZDAFUJDANUKUIDADACHOPUDUFDARS - UFDAUFDGTUA $. + weq sbbi mpbi sbh 3bitri ) CAEZABFZCDEZDBFZCBEZDBFZUFUCUDDAFZABFUEUHUBABU + DUBDAUBDGDACHIJUDDBAUDAGKLUDUFMZDBFZUEUGMDBQZDBFUJDBNUKUIDBDBCHOPUDUFDBRS + UFDBUFDGTUA $. $} ${ @@ -16097,7 +16097,7 @@ Predicate calculus with distinct variables (cont.) ( vz vw weq wb wal wex wsb weu nfv sb8 sbbi nfsb equsb3 nfxfr nfbi df-eu sbequ cbval sblbis albii 3bitri exbii 3bitr4i ) ABEGZHZBIZEJABCKZCEGZHZCI ZEJABLUKCLUJUNEUJUIBFKZFIUIBCKZCIUNUIBFUIFMNUOUPFCUOABFKZUHBFKZHCAUHBFOUQ - URCABFCDPURFEGZCFBEQUSCMRSRUPFMUIFCBUAUBUPUMCUHULABCCBEQUCUDUEUFABETUKCET + URCABFCDPURFEGZCBFEQUSCMRSRUPFMUIFCBUAUBUPUMCUHULABCBCEQUCUDUEUFABETUKCET UG $. $( Variable substitution for "at most one." (Contributed by Alexander van @@ -16194,7 +16194,7 @@ Predicate calculus with distinct variables (cont.) ( vz vw weq wb wal wex wsb ax-17 sb8h sbbi hbsb equsb3 hbxfrbi hbbi df-eu weu sbequ cbvalh sblbis albii 3bitri exbii 3bitr4i ) ABEGZHZBIZEJABCKZCEG ZHZCIZEJABTUKCTUJUNEUJUIBFKZFIUIBCKZCIUNUIBFUIFLMUOUPFCUOABFKZUHBFKZHCAUH - BFNUQURCABFCDOURFEGZCFBEPUSCLQRQUPFLUIFCBUAUBUPUMCUHULABCCBEPUCUDUEUFABES + BFNUQURCABFCDOURFEGZCBFEPUSCLQRQUPFLUIFCBUAUBUPUMCUHULABCBCEPUCUDUEUFABES UKCESUG $. $} @@ -17964,7 +17964,7 @@ of logic but rather presupposes the Axiom of Extensionality (see theorem (Contributed by NM, 7-Nov-2006.) $) cvjust $p |- x = { y | y e. x } $= ( vz cv wcel cab wceq wb dfcleq wsb df-clab elsb3 bitr2i mpgbir ) ADZBDOE - ZBFZGCDZOEZRQEZHCCOQITPBCJSPCBKCBALMN $. + ZBFZGCDZOEZRQEZHCCOQITPBCJSPCBKBCALMN $. $} ${ @@ -18881,39 +18881,39 @@ This law is thought to have originated with Aristotle (_Metaphysics_, ( wcel wceq eleq2 biimpcd con3dimp ) ABDZBCEZACDZJIKBCAFGH $. ${ - $d x y $. $d y A $. + $d x y $. $d x A $. $( Lemma for ~ eqsb3 . (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - eqsb3lem $p |- ( [ x / y ] y = A <-> x = A ) $= - ( cv wceq nfv eqeq1 sbie ) BDZCEADZCEZBAKBFIJCGH $. + eqsb3lem $p |- ( [ y / x ] x = A <-> y = A ) $= + ( cv wceq nfv eqeq1 sbie ) ADZCEBDZCEZABKAFIJCGH $. $} ${ - $d y A $. $d w y $. $d w A $. $d x w $. + $d x A $. $d w x $. $d w A $. $d y w $. $( Substitution applied to an atomic wff (class version of ~ equsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010.) $) - eqsb3 $p |- ( [ x / y ] y = A <-> x = A ) $= - ( vw cv wceq wsb eqsb3lem sbbii nfv sbco2 3bitr3i ) BECFZBDGZDAGDECFZDAGM - BAGAECFNODADBCHIMBADMDJKADCHL $. + eqsb3 $p |- ( [ y / x ] x = A <-> y = A ) $= + ( vw cv wceq wsb eqsb3lem sbbii nfv sbco2 3bitr3i ) AECFZADGZDBGDECFZDBGM + ABGBECFNODBADCHIMABDMDJKDBCHL $. $} ${ - $d y A $. $d w y $. $d w A $. $d w x $. + $d x A $. $d w x $. $d w A $. $d w y $. $( Substitution applied to an atomic wff (class version of ~ elsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - clelsb3 $p |- ( [ x / y ] y e. A <-> x e. A ) $= - ( vw cv wcel wsb nfv sbco2 eleq1 sbie sbbii 3bitr3i ) DEZCFZDBGZBAGODAGBE - ZCFZBAGAEZCFZODABOBHIPRBAORDBRDHNQCJKLOTDATDHNSCJKM $. + clelsb3 $p |- ( [ y / x ] x e. A <-> y e. A ) $= + ( vw cv wcel wsb nfv sbco2 eleq1 sbie sbbii 3bitr3i ) DEZCFZDAGZABGODBGAE + ZCFZABGBEZCFZODBAOAHIPRABORDARDHNQCJKLOTDBTDHNSCJKM $. $} ${ - $d y A $. $d w y $. $d w A $. $d w x $. + $d x A $. $d w x $. $d w A $. $d w y $. $( Substitution applied to an atomic wff (class version of ~ elsb4 ). (Contributed by Jim Kingdon, 22-Nov-2018.) $) - clelsb4 $p |- ( [ x / y ] A e. y <-> A e. x ) $= - ( vw cv wcel wsb nfv sbco2 eleq2 sbie sbbii 3bitr3i ) CDEZFZDBGZBAGODAGCB - EZFZBAGCAEZFZODABOBHIPRBAORDBRDHNQCJKLOTDATDHNSCJKM $. + clelsb4 $p |- ( [ y / x ] A e. x <-> A e. y ) $= + ( vw cv wcel wsb nfv sbco2 eleq2 sbie sbbii 3bitr3i ) CDEZFZDAGZABGODBGCA + EZFZABGCBEZFZODBAOAHIPRABORDARDHNQCJKLOTDBTDHNSCJKM $. $} ${ @@ -18933,7 +18933,7 @@ This law is thought to have originated with Aristotle (_Metaphysics_, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) $) hblem $p |- ( z e. A -> A. x z e. A ) $= ( cv wcel wsb wal hbsb clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAEJ - CBDKZOPAQLM $. + BCDKZOPAQLM $. $} ${ @@ -19278,15 +19278,15 @@ effectively bound by a quantifier or something that expands to one (such $} ${ - $d w y $. $d w A $. $d w x $. - clelsb3f.1 $e |- F/_ y A $. + $d w x $. $d w A $. $d w y $. + clelsb3f.1 $e |- F/_ x A $. $( Substitution applied to an atomic wff (class version of ~ elsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.) $) - clelsb3f $p |- ( [ x / y ] y e. A <-> x e. A ) $= - ( vw cv wcel wsb nfcri sbco2 nfv eleq1w sbie sbbii 3bitr3i ) EFCGZEBHZBAH - PEAHBFCGZBAHAFCGZPEABBECDIJQRBAPREBREKEBCLMNPSEASEKEACLMO $. + clelsb3f $p |- ( [ y / x ] x e. A <-> y e. A ) $= + ( vw cv wcel wsb nfcri sbco2 nfv eleq1w sbie sbbii 3bitr3i ) EFCGZEAHZABH + PEBHAFCGZABHBFCGZPEBAAECDIJQRABPREAREKEACLMNPSEBSEKEBCLMO $. $} ${ @@ -20707,7 +20707,7 @@ effectively bound by a quantifier or something that expands to one (such nfraldya $p |- ( ph -> F/ x A. y e. A ps ) $= ( vz wral cv wcel wi wal df-ral wsb sbim clelsb3 nfv nfxfrd bitri 3bitr4i imbi1i albii sb8 nfsbd nfraldxy ) BDEJDKELZBMZDNZACBDEOUJBDIPZIEJZACUIDIP - ZINIKELZUKMZINUJULUMUOIUMUHDIPZUKMUOUHBDIQUPUNUKIDERUCUAUDUIDIUIISUEUKIEO + ZINIKELZUKMZINUJULUMUOIUMUHDIPZUKMUOUHBDIQUPUNUKDIERUCUAUDUIDIUIISUEUKIEO UBAUKCIEAISGABDICFHUFUGTT $. $( Not-free for restricted existential quantification where ` y ` and ` A ` @@ -20716,7 +20716,7 @@ effectively bound by a quantifier or something that expands to one (such nfrexdya $p |- ( ph -> F/ x E. y e. A ps ) $= ( vz wrex cv wcel wa wex df-rex wsb sban clelsb3 nfv nfxfrd bitri 3bitr4i anbi1i exbii sb8e nfsbd nfrexdxy ) BDEJDKELZBMZDNZACBDEOUJBDIPZIEJZACUIDI - PZINIKELZUKMZINUJULUMUOIUMUHDIPZUKMUOUHBDIQUPUNUKIDERUCUAUDUIDIUIISUEUKIE + PZINIKELZUKMZINUJULUMUOIUMUHDIPZUKMUOUHBDIQUPUNUKDIERUCUAUDUIDIUIISUEUKIE OUBAUKCIEAISGABDICFHUFUGTT $. $} @@ -22278,7 +22278,7 @@ deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.) $) ( vz cv wcel wa weu wreu wsb nfv sb8eu sban eubii df-reu anbi1i nfsb nfan clelsb3 weq eleq1 sbequ sbie syl6bb anbi12d cbveu bitri 3bitri 3bitr4i ) CJEKZALZCMZDJZEKZBLZDMZACENBDENUQUPCIOZIMUOCIOZACIOZLZIMZVAUPCIUPIPQVBVEI - UOACIRSVFIJZEKZVDLZIMVAVEVIIVCVHVDICEUDUASVIUTIDVHVDDVHDPACIDFUBUCUTIPIDU + UOACIRSVFIJZEKZVDLZIMVAVEVIIVCVHVDCIEUDUASVIUTIDVHVDDVHDPACIDFUBUCUTIPIDU EZVHUSVDBVGUREUFVJVDACDOBAIDCUGABCDGHUHUIUJUKULUMACETBDETUN $. $( Change the bound variable of restricted "at most one" using implicit @@ -22409,14 +22409,14 @@ deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.) $) $} ${ - $d x y z $. $d y z ph $. $d x z ps $. + $d x y z $. $d x z ph $. $d y z ps $. sbralie.1 $e |- ( x = y -> ( ph <-> ps ) ) $. $( Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.) $) - sbralie $p |- ( [ x / y ] A. x e. y ph <-> A. y e. x ps ) $= - ( vz cv wral wsb cbvralsv sbbii nfv raleq sbie bitri sbco2 ralbii ) ACDGZ - HZDCIZACFIZFCGZHZBDUBHZTUAFRHZDCIUCSUEDCACFRJKUEUCDCUCDLUAFRUBMNOUCUAFDIZ - DUBHUDUAFDUBJUFBDUBUFACDIBACDFAFLPABCDBCLENOQOO $. + sbralie $p |- ( [ y / x ] A. y e. x ph <-> A. x e. y ps ) $= + ( vz cv wral wsb cbvralsv sbbii nfv raleq sbie bitri sbco2 equcoms ralbii + wb ) ADCGZHZCDIZADFIZFDGZHZBCUDHZUBUCFTHZCDIUEUAUGCDADFTJKUGUECDUECLUCFTU + DMNOUEUCFCIZCUDHUFUCFCUDJUHBCUDUHADCIBADCFAFLPABDCBDLABSCDEQNOROO $. $} ${ @@ -24095,7 +24095,7 @@ deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.) $) ( vy cv wceq wal eqeq1 eqeq2 bibi1d albidv alrimiv wsb stdpc4 sbbi bibi2i wb eqsb3 sylbi equsb1 bi1 mpi syl impbii vtoclbg ) EFZCGZAFZUGGZUICGZRZAH ZBCGUIBGZUKRZAHEBDUGBCIUGBGZULUOAUPUJUNUKUGBUIJKLUHUMUHULAUGCUIJMUMULAENZ - UHULAEOUQUJAENZUKAENZRZUHUJUKAEPUTURUHRZUHUSUHUREACSQVAURUHAEUAURUHUBUCTT + UHULAEOUQUJAENZUKAENZRZUHUJUKAEPUTURUHRZUHUSUHURAECSQVAURUHAEUAURUHUBUCTT UDUEUF $. $} @@ -24739,7 +24739,7 @@ deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.) $) wmo weq df-rmo sban clelsb3f anbi2i an4 ancom imbi1i nfcri r19.21 3bitr2i nfan mo3 3bitr4i ) ABDUABHDIZAJZBUBZAABCKZJZBCUCZLZCDMZBDMZABDUDURURBCKZJ ZVBLZCNZBNUQVDLZBNUSVEVIVJBVICHDIZUQVCLZLZCNVLCDMVJVHVMCVHVKUQJZVAJZVBLVN - VCLVMVGVOVBVGURVKUTJZJUQVKJZVAJVOVFVPURVFUQBCKZUTJVPUQABCUEVRVKUTCBDEUFOP + VCLVMVGVOVBVGURVKUTJZJUQVKJZVAJVOVFVPURVFUQBCKZUTJVPUQABCUEVRVKUTBCDEUFOP UGUQAVKUTUHVQVNVAUQVKUIOQUJVNVAVBRVKUQVCRQSVLCDTUQVCCDCBDFUKZULUMSURBCUQA CVSGUNUOVDBDTUPP $. $} @@ -25485,7 +25485,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use (Contributed by Andrew Salmon, 29-Jun-2011.) $) eqsbc3 $p |- ( A e. V -> ( [. A / x ]. x = B <-> A = B ) ) $= ( vy cv wceq wsbc dfsbcq eqeq1 wsb sbsbc eqsb3 bitr3i vtoclbg ) AFCGZAEFZ - HZQCGZPABHBCGEBDPAQBIQBCJRPAEKSPAELEACMNO $. + HZQCGZPABHBCGEBDPAQBIQBCJRPAEKSPAELAECMNO $. $} ${ @@ -25671,7 +25671,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use 17-Aug-2018.) $) sbcel1v $p |- ( [. A / x ]. x e. B <-> A e. B ) $= ( vy wcel wsbc cvv sbcex elex wsb dfsbcq2 eleq1 clelsb3 vtoclbg pm5.21nii - cv ) APCEZABFZBGEBCEZQABHBCIQADJDPZCERSDBGQADBKTBCLDACMNO $. + cv ) APCEZABFZBGEBCEZQABHBCIQADJDPZCERSDBGQADBKTBCLADCMNO $. $} ${ @@ -25961,7 +25961,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use wal weq df-rmo sban clelsb3 anbi2i an4 ancom r19.21v 3bitr2i nfv nfan mo3 imbi1i 3bitr4i ) ABDFBGDHZAIZBJZAABCKZIZBCUAZLZCDMZBDMZABDUBUPUPBCKZIZUTL ZCTZBTUOVBLZBTUQVCVGVHBVGCGDHZUOVALZLZCTVJCDMVHVFVKCVFVIUOIZUSIZUTLVLVALV - KVEVMUTVEUPVIURIZIUOVIIZUSIVMVDVNUPVDUOBCKZURIVNUOABCUCVPVIURCBDUDNOUEUOA + KVEVMUTVEUPVIURIZIUOVIIZUSIVMVDVNUPVDUOBCKZURIVNUOABCUCVPVIURBCDUDNOUEUOA VIURUFVOVLUSUOVIUGNPUMVLUSUTQVIUOVAQPRVJCDSUOVACDUHUIRUPBCUOACUOCUJEUKULV BBDSUNO $. $} @@ -39131,7 +39131,7 @@ this axiom (that is, Non-wellfounded Set Theory but in the absence of S = _V ) $= ( cv wcel wi wal cvv wceq wsb wral clelsb3 ralbii df-ral imbi1i ax-setind bitri albii sylbir eqv sylibr ) BDZADZEUBCEZFBGZUCCEZFZAGZUFAGZCHIUHUFABJ - ZBUCKZUFFZAGUIULUGAUKUEUFUKUDBUCKUEUJUDBUCBACLMUDBUCNQORUFBAPSACTUA $. + ZBUCKZUFFZAGUIULUGAUKUEUFUKUDBUCKUEUJUDBUCABCLMUDBUCNQORUFBAPSACTUA $. $} ${ @@ -39178,7 +39178,7 @@ this axiom (that is, Non-wellfounded Set Theory but in the absence of AZVMARZMVNWFWGVLWFAENVIWDWGVLVIWDWGUBZVIVLVIWDWGUCWHAVMDZVLLZVIVLLZWDVIWJ WGWDWIVLWCWJCAVMVTARWAWIWBVLVTAVMOVTAVKOUDPUEUFWGVIWJWKUGWDWGWIVIVLVMAAUH UJUIUKQULUMVNVMVJDZWGVNVMEDWLMBUNVMEVJUOUPBAVAUQSVBURVRWEBVQWDVNVQWAVPLZC - IWDVPCVMUSWMWCCVPWBWACBVKUTVCTVDVETSVNCBVFVGVNVLBAAVMAVKOPQVIAENVH $. + IWDVPCVMUSWMWCCVPWBWABCVKUTVCTVDVETSVNCBVFVGVNVLBAAVMAVKOPQVIAENVH $. $} $( Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. @@ -39291,7 +39291,7 @@ class of all ordinal numbers to be a set (so instead it is a proper WGAWEEZABGVCWGXPXQLZWGXPXRFXPXRJAGWENXPXROUGUHUISRZRWDWSXCWGWDWSXCUKZWBWG WBWCWSXCVDXTAWHEZWGJZWBWGJZWSWDYBXCWSYAWGWRYBDAWHWOAKWPYAWQWGWOAWHPWOAWFP ULQUNUOXCWDYBYCUPWSXCYAWBWGWHBAUQURUSUTTVAVBXBXCVOVEWIWHWEEZXDWIWHGEYDLCV - FZWHGWENVGWHABYEVHVIVJVKVLWMWTCWLWSWIWLWPWKJZDIWSWKDWHVMYFWRDWKWQWPDCWFVN + FZWHGWENVGWHABYEVHVIVJVKVLWMWTCWLWSWIWLWPWKJZDIWSWKDWHVMYFWRDWKWQWPCDWFVN VPVQVRVSVQVJWIDCVTSWBWJWGJWCWIWGCABWHAWFPQRTXSWA $. $} @@ -39541,7 +39541,7 @@ class of all ordinal numbers to be a set (so instead it is a proper wss ax-setind dfss2 sylibr sylbir df-frfor mpbir mpgbir ) AEFAEBGZHZBAEBI URCGZDGZEUAZCBJZKZCALZDBJZKZDALZAUQUIZKVGUTAMZVEKZDCNZCUTLZVJKZDQZVHVNVLV EKZDALZVGVNVIVOKZDQVPVMVQDVLVIVEUBUCVODAUDOVOVFDAVLVDVEVLCDJZVBKZCALZVDVL - USAMZVBKZCUTLVTVKWBCUTVKVIDCNZVEDCNZKWBVIVEDCUEWCWAWDVBCDAPCDUQPUFRSVBCUT + USAMZVBKZCUTLVTVKWBCUTVKVIDCNZVEDCNZKWBVIVEDCUEWCWAWDVBDCAPDCUQPUFRSVBCUT AUGRVCVSCAVAVRVBCDUHTSOTSRVNVJDQVHVJCDUJDAUQUKULUMDCAEUQUNUOUP $. $} @@ -39678,7 +39678,7 @@ can deduce (outside the formal system, since we cannot quantify over VJWPWCCVIBRUCWCWGCUDUEOMNWJWEAWBWIWDWAWHCVQVRJZVSHVQWCJZVSHZWAWHWRWQVSWRV QVRVQWCUFWRVRHZAWTAKZCDUGXACKUHCADUIUJPPVAQVQVRVSSWSVQWCVSHHWHVQWCVSSVQWC VSUKNULUMQUMUNUOWFWDAKZVNWFWDACTZCVIIZWDHZAKXBXEWEAXDWBWDXDVTCVIIWBXCVTCV - IXCWCACTZVKACTZHVTWCVKACVBXFVRXGVSCADUPCABUPUQNURVTCVILNOMWDCAUSUTADBRVCV + IXCWCACTZVKACTZHVTWCVKACVBXFVRXGVSACDUPACBUPUQNURVTCVILNOMWDCAUSUTADBRVCV DVOVHVNJBDVEVFVG $. $} @@ -39860,7 +39860,7 @@ The natural numbers (i.e. finite ordinals) peano1 $p |- (/) e. _om $= ( vy vx vz c0 cv wcel csuc wral wa cab com wi 0ex elint wsb df-clab simpl cint sbimi clelsb4 sylib sylbi mpgbir dfom3 eleqtrri ) DDAEZFZBEGUFFBUFHZ - IZAJZRZKDUKFCEZUJFZDULFZLCCDUJMNUMUIACOZUNUICAPUOUGACOUNUIUGACUGUHQSCADTU + IZAJZRZKDUKFCEZUJFZDULFZLCCDUJMNUMUIACOZUNUICAPUOUGACOUNUIUGACUGUHQSACDTU AUBUCABUDUE $. $( $j usage 'peano1' avoids 'ax-iinf' 'ax-setind'; $) $} @@ -39871,17 +39871,17 @@ The natural numbers (i.e. finite ordinals) five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.) $) peano2 $p |- ( A e. _om -> suc A e. _om ) $= - ( vy vx vz cvv wcel com csuc cv wa wi wb imbi12d adantl wsb wal sylib nfv - wral nfan elex c0 cint simpl wceq eleq1 suceq eleq1d df-clab simpr df-ral - cab sbimi sbim elsb4 clelsb4 imbi12i bitri sbalv sylbi 19.21bi nfra1 nfvd - nfsab nfcvd vtocldf ralrimiva ralim elintg sucexg syl syl5ibr mpd 3imtr4g - dfom3 eleq2i mpcom ) AEFZAGFZAHZGFZAGUAVRAUBBIZFZCIZHZWBFZCWBSZJZBULZUCZF - ZVTWJFZVSWAVRADIZFZVTWMFZKZDWISZWKWLKZVRWPDWIVRWMWIFZJZWDWMFZWEWMFZKZWPCA - EVRWSUDWDAUEZXCWPLWTXDXAWNXBWOWDAWMUFXDWEVTWMWDAUGUHMNWSXCVRWSXCCWSWHBDOZ - XCCPZWHDBUIXEWDWBFZWFKZCPZBDOXFWHXIBDWHWGXIWCWGUJWFCWBUKQUMXHXCBDCXHBDOXG - BDOZWFBDOZKXCXGWFBDUNXJXAXKXBDBCUODBWEUPUQURUSQUTVANVRWSCVRCRWHCBDWCWGCWC - CRWFCWBVBTVDTWTCAVEWTWPCVCVFVGWQWRVRWNDWISZWODWISZKWNWODWIVHVRWKXLWLXMDAW - IEVIVRVTEFWLXMLAEVJDVTWIEVIVKMVLVMGWJABCVOZVPGWJVTXNVPVNVQ $. + ( vy vx vz cvv wcel com csuc cv wral wa wi imbi12d adantl wsb wal clelsb4 + wb sylib nfv elex c0 cab cint simpl wceq eleq1 suceq eleq1d df-clab simpr + df-ral sbimi sbim imbi12i bitri sbalv sylbi 19.21bi nfra1 nfan nfsab nfvd + nfcvd vtocldf ralrimiva ralim elintg sucexg syl syl5ibr mpd dfom3 3imtr4g + eleq2i mpcom ) AEFZAGFZAHZGFZAGUAVQAUBBIZFZCIZHZWAFZCWAJZKZBUCZUDZFZVSWIF + ZVRVTVQADIZFZVSWLFZLZDWHJZWJWKLZVQWODWHVQWLWHFZKZWCWLFZWDWLFZLZWOCAEVQWRU + EWCAUFZXBWORWSXCWTWMXAWNWCAWLUGXCWDVSWLWCAUHUIMNWRXBVQWRXBCWRWGBDOZXBCPZW + GDBUJXDWCWAFZWELZCPZBDOXEWGXHBDWGWFXHWBWFUKWECWAULSUMXGXBBDCXGBDOXFBDOZWE + BDOZLXBXFWEBDUNXIWTXJXABDWCQBDWDQUOUPUQSURUSNVQWRCVQCTWGCBDWBWFCWBCTWECWA + UTVAVBVAWSCAVDWSWOCVCVEVFWPWQVQWMDWHJZWNDWHJZLWMWNDWHVGVQWJXKWKXLDAWHEVHV + QVSEFWKXLRAEVIDVSWHEVHVJMVKVLGWIABCVMZVOGWIVSXMVOVNVP $. $( $j usage 'peano2' avoids 'ax-iinf' 'ax-setind'; $) $} @@ -45103,8 +45103,8 @@ Definite description binder (inverted iota) ( vz vw weq wal cab cuni wsb cio nfv sb8 sbbi nfsb equsb3 nfxfr dfiota2 wb nfbi sbequ cbval sblbis albii 3bitri abbii unieqi 3eqtr4i ) ABEGZTZBHZ EIZJABCKZCEGZTZCHZEIZJABLUNCLUMURULUQEULUKBFKZFHUKBCKZCHUQUKBFUKFMNUSUTFC - USABFKZUJBFKZTCAUJBFOVAVBCABFCDPVBFEGZCFBEQVCCMRUARUTFMUKFCBUBUCUTUPCUJUO - ABCCBEQUDUEUFUGUHABESUNCESUI $. + USABFKZUJBFKZTCAUJBFOVAVBCABFCDPVBFEGZCBFEQVCCMRUARUTFMUKFCBUBUCUTUPCUJUO + ABCBCEQUDUEUFUGUHABESUNCESUI $. $} ${ @@ -143148,7 +143148,7 @@ with definitions ( ` B ` is the definiendum that one wants to prove bdcab ax-mp ) BCHZAIZBJZABCKZUAVGBLZUBZVHFKVJUCZGFHZMZFNZGLVKVOGABFOZVMMZ FVIUDZVOVQFCVPVMABFDUEGFUFUGUHVRVGBFOZVMMZFNZVOVRFCHZVPIZVMMZFNZWAVRWBVQM ZFNWEVQFVIUIWFWDFWDWFWBVPVMUJPQRWDVTFWCVSVMVSWCVSVFBFOZVPIWCVFABFULWGWBVP - FBVIUKUMRPSQRVTVNFVSVLVMVLVSVGFBUNPSQRUOVDGFVJUPTVGBUQZVHVKURABVIUSWHEABV + BFVIUKUMRPSQRVTVNFVSVLVMVLVSVGFBUNPSQRUOVDGFVJUPTVGBUQZVHVKURABVIUSWHEABV IUTVAVGBVBVETABVIVCT $. $} From 4f084edfbc4ddf032ec217cb7afae6bfefd09f49 Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Thu, 12 Oct 2023 00:46:55 +0200 Subject: [PATCH 3/3] replaced '|- ( [ x / y ]' with '|- ( [ y / x ]' in nf.mm --- nf.mm | 329 +++++++++++++++++++++++++++++----------------------------- 1 file changed, 164 insertions(+), 165 deletions(-) diff --git a/nf.mm b/nf.mm index c8b12aa451..63828535df 100644 --- a/nf.mm +++ b/nf.mm @@ -16746,39 +16746,39 @@ primitive connectives (no defined terms) on the right-hand side. $} ${ - $d y z $. $d x y $. + $d x z $. $d x y $. $( Lemma for ~ equsb3 . (Contributed by Raph Levien and FL, 4-Dec-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - equsb3lem $p |- ( [ x / y ] y = z <-> x = z ) $= - ( weq nfv equequ1 sbie ) BCDACDZBAHBEBACFG $. + equsb3lem $p |- ( [ y / x ] x = z <-> y = z ) $= + ( weq nfv equequ1 sbie ) ACDBCDZABHAEABCFG $. $} ${ - $d w y z $. $d w x $. + $d w x z $. $d w y $. $( Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.) $) - equsb3 $p |- ( [ x / y ] y = z <-> x = z ) $= - ( vw weq wsb equsb3lem sbbii nfv sbco2 3bitr3i ) BCEZBDFZDAFDCEZDAFLBAFAC - EMNDADBCGHLBADLDIJADCGK $. + equsb3 $p |- ( [ y / x ] x = z <-> y = z ) $= + ( vw weq wsb equsb3lem sbbii nfv sbco2 3bitr3i ) ACEZADFZDBFDCEZDBFLABFBC + EMNDBADCGHLABDLDIJDBCGK $. $} ${ - $d w y z $. $d w x $. + $d w x z $. $d w y $. $( Substitution applied to an atomic membership wff. (Contributed by NM, 7-Nov-2006.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - elsb3 $p |- ( [ x / y ] y e. z <-> x e. z ) $= - ( vw wel wsb nfv sbco2 elequ1 sbie sbbii 3bitr3i ) DCEZDBFZBAFMDAFBCEZBAF - ACEZMDABMBGHNOBAMODBODGDBCIJKMPDAPDGDACIJL $. + elsb3 $p |- ( [ y / x ] x e. z <-> y e. z ) $= + ( vw wel wsb nfv sbco2 elequ1 sbie sbbii 3bitr3i ) DCEZDAFZABFMDBFACEZABF + BCEZMDBAMAGHNOABMODAODGDACIJKMPDBPDGDBCIJL $. $} ${ - $d w y z $. $d w x $. + $d w x z $. $d w y $. $( Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - elsb4 $p |- ( [ x / y ] z e. y <-> z e. x ) $= - ( vw wel wsb nfv sbco2 elequ2 sbie sbbii 3bitr3i ) CDEZDBFZBAFMDAFCBEZBAF - CAEZMDABMBGHNOBAMODBODGDBCIJKMPDAPDGDACIJL $. + elsb4 $p |- ( [ y / x ] z e. x <-> z e. y ) $= + ( vw wel wsb nfv sbco2 elequ2 sbie sbbii 3bitr3i ) CDEZDAFZABFMDBFCAEZABF + CBEZMDBAMAGHNOABMODAODGDACIJKMPDBPDGDBCIJL $. $} ${ @@ -18212,7 +18212,7 @@ an axiom since it can be proved from our other axioms (although the proof, ( vz vw cv wceq wb wal wex wsb weu nfv sb8 sbbi nfsb equsb3 nfxfr df-eu nfbi sbequ cbval sblbis albii 3bitri exbii 3bitr4i ) ABGEGZHZIZBJZEKABCLZ CGUIHZIZCJZEKABMUMCMULUPEULUKBFLZFJUKBCLZCJUPUKBFUKFNOUQURFCUQABFLZUJBFLZ - ICAUJBFPUSUTCABFCDQUTFGUIHZCFBERVACNSUASURFNUKFCBUBUCURUOCUJUNABCCBERUDUE + ICAUJBFPUSUTCABFCDQUTFGUIHZCBFERVACNSUASURFNUKFCBUBUCURUOCUJUNABCBCERUDUE UFUGABETUMCETUH $. $( Variable substitution in uniqueness quantifier. (Contributed by @@ -20116,7 +20116,7 @@ of logic but rather presupposes the Axiom of Extensionality (see theorem (Contributed by NM, 7-Nov-2006.) $) cvjust $p |- x = { y | y e. x } $= ( vz cv wcel cab wceq wb dfcleq wsb df-clab elsb3 bitr2i mpgbir ) ADZBDOE - ZBFZGCDZOEZRQEZHCCOQITPBCJSPCBKCBALMN $. + ZBFZGCDZOEZRQEZHCCOQITPBCJSPCBKBCALMN $. $} ${ @@ -21021,30 +21021,30 @@ This law is thought to have originated with Aristotle (_Metaphysics_, ( wcel wceq eleq2 biimpcd con3and ) ABDZBCEZACDZJIKBCAFGH $. ${ - $d x y $. $d y A $. + $d x y $. $d x A $. $( Lemma for ~ eqsb3 . (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - eqsb3lem $p |- ( [ x / y ] y = A <-> x = A ) $= - ( cv wceq nfv eqeq1 sbie ) BDZCEADZCEZBAKBFIJCGH $. + eqsb3lem $p |- ( [ y / x ] x = A <-> y = A ) $= + ( cv wceq nfv eqeq1 sbie ) ADZCEBDZCEZABKAFIJCGH $. $} ${ - $d y A $. $d w y $. $d w A $. $d x w $. + $d x A $. $d w x $. $d w A $. $d y w $. $( Substitution applied to an atomic wff (class version of ~ equsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010.) $) - eqsb3 $p |- ( [ x / y ] y = A <-> x = A ) $= - ( vw cv wceq wsb eqsb3lem sbbii nfv sbco2 3bitr3i ) BECFZBDGZDAGDECFZDAGM - BAGAECFNODADBCHIMBADMDJKADCHL $. + eqsb3 $p |- ( [ y / x ] x = A <-> y = A ) $= + ( vw cv wceq wsb eqsb3lem sbbii nfv sbco2 3bitr3i ) AECFZADGZDBGDECFZDBGM + ABGBECFNODBADCHIMABDMDJKDBCHL $. $} ${ - $d y A $. $d w y $. $d w A $. $d w x $. + $d x A $. $d w x $. $d w A $. $d w y $. $( Substitution applied to an atomic wff (class version of ~ elsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) $) - clelsb3 $p |- ( [ x / y ] y e. A <-> x e. A ) $= - ( vw cv wcel wsb nfv sbco2 eleq1 sbie sbbii 3bitr3i ) DEZCFZDBGZBAGODAGBE - ZCFZBAGAEZCFZODABOBHIPRBAORDBRDHNQCJKLOTDATDHNSCJKM $. + clelsb3 $p |- ( [ y / x ] x e. A <-> y e. A ) $= + ( vw cv wcel wsb nfv sbco2 eleq1 sbie sbbii 3bitr3i ) DEZCFZDAGZABGODBGAE + ZCFZABGBEZCFZODBAOAHIPRABORDARDHNQCJKLOTDBTDHNSCJKM $. $} ${ @@ -21065,7 +21065,7 @@ This law is thought to have originated with Aristotle (_Metaphysics_, 11-Jul-2011.) $) hblem $p |- ( z e. A -> A. x z e. A ) $= ( cv wcel wsb wal hbsb clelsb3 albii 3imtr3i ) BFDGZBCHZOAICFDGZPAINBCAEJ - CBDKZOPAQLM $. + BCDKZOPAQLM $. $} ${ @@ -24142,7 +24142,7 @@ This law is thought to have originated with Aristotle (_Metaphysics_, ( vz cv wcel wa weu wreu wsb nfv sb8eu sban eubii df-reu anbi1i nfsb nfan clelsb3 wceq eleq1 sbequ sbie syl6bb anbi12d cbveu bitri 3bitri 3bitr4i ) CJEKZALZCMZDJZEKZBLZDMZACENBDENUQUPCIOZIMUOCIOZACIOZLZIMZVAUPCIUPIPQVBVEI - UOACIRSVFIJZEKZVDLZIMVAVEVIIVCVHVDICEUDUASVIUTIDVHVDDVHDPACIDFUBUCUTIPVGU + UOACIRSVFIJZEKZVDLZIMVAVEVIIVCVHVDCIEUDUASVIUTIDVHVDDVHDPACIDFUBUCUTIPVGU RUEZVHUSVDBVGUREUFVJVDACDOBAIDCUGABCDGHUHUIUJUKULUMACETBDETUN $. $( Change the bound variable of restricted "at most one" using implicit @@ -24273,14 +24273,14 @@ This law is thought to have originated with Aristotle (_Metaphysics_, $} ${ - $d x y z $. $d y z ph $. $d x z ps $. + $d x y z $. $d x z ph $. $d y z ps $. sbralie.1 $e |- ( x = y -> ( ph <-> ps ) ) $. $( Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.) $) - sbralie $p |- ( [ x / y ] A. x e. y ph <-> A. y e. x ps ) $= - ( vz cv wral wsb cbvralsv sbbii nfv raleq sbie bitri sbco2 ralbii ) ACDGZ - HZDCIZACFIZFCGZHZBDUBHZTUAFRHZDCIUCSUEDCACFRJKUEUCDCUCDLUAFRUBMNOUCUAFDIZ - DUBHUDUAFDUBJUFBDUBUFACDIBACDFAFLPABCDBCLENOQOO $. + sbralie $p |- ( [ y / x ] A. y e. x ph <-> A. x e. y ps ) $= + ( vz cv wral wsb cbvralsv sbbii nfv raleq sbie bitri sbco2 eqcoms ralbii + wb ) ADCGZHZCDIZADFIZFDGZHZBCUDHZUBUCFTHZCDIUEUAUGCDADFTJKUGUECDUECLUCFTU + DMNOUEUCFCIZCUDHUFUCFCUDJUHBCUDUHADCIBADCFAFLPABDCBDLABSTUDEQNOROO $. $} ${ @@ -25762,7 +25762,7 @@ This law is thought to have originated with Aristotle (_Metaphysics_, ( vy cv wceq wal eqeq1 eqeq2 bibi1d albidv alrimiv wsb stdpc4 sbbi bibi2i wb eqsb3 sylbi equsb1 bi1 mpi syl impbii vtoclbg ) EFZCGZAFZUGGZUICGZRZAH ZBCGUIBGZUKRZAHEBDUGBCIUGBGZULUOAUPUJUNUKUGBUIJKLUHUMUHULAUGCUIJMUMULAENZ - UHULAEOUQUJAENZUKAENZRZUHUJUKAEPUTURUHRZUHUSUHUREACSQVAURUHAEUAURUHUBUCTT + UHULAEOUQUJAENZUKAENZRZUHUJUKAEPUTURUHRZUHUSUHURAECSQVAURUHAEUAURUHUBUCTT UDUEUF $. $} @@ -27014,7 +27014,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use (Contributed by Andrew Salmon, 29-Jun-2011.) $) eqsbc3 $p |- ( A e. V -> ( [. A / x ]. x = B <-> A = B ) ) $= ( vy cv wceq wsbc dfsbcq eqeq1 wsb sbsbc eqsb3 bitr3i vtoclbg ) AFCGZAEFZ - HZQCGZPABHBCGEBDPAQBIQBCJRPAEKSPAELEACMNO $. + HZQCGZPABHBCGEBDPAQBIQBCJRPAEKSPAELAECMNO $. $} ${ @@ -27184,7 +27184,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) $) sbcel1gv $p |- ( A e. V -> ( [. A / x ]. x e. B <-> A e. B ) ) $= ( vy cv wcel wsb wsbc dfsbcq2 eleq1 clelsb3 vtoclbg ) AFCGZAEHEFZCGNABIBC - GEBDNAEBJOBCKEACLM $. + GEBDNAEBJOBCKAECLM $. $} ${ @@ -27472,7 +27472,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use wal weq df-rmo sban clelsb3 anbi2i an4 ancom r19.21v 3bitr2i nfv nfan mo3 imbi1i 3bitr4i ) ABDFBGDHZAIZBJZAABCKZIZBCUAZLZCDMZBDMZABDUBUPUPBCKZIZUTL ZCTZBTUOVBLZBTUQVCVGVHBVGCGDHZUOVALZLZCTVJCDMVHVFVKCVFVIUOIZUSIZUTLVLVALV - KVEVMUTVEUPVIURIZIUOVIIZUSIVMVDVNUPVDUOBCKZURIVNUOABCUCVPVIURCBDUDNOUEUOA + KVEVMUTVEUPVIURIZIUOVIIZUSIVMVDVNUPVDUOBCKZURIVNUOABCUCVPVIURBCDUDNOUEUOA VIURUFVOVLUSUOVIUGNPUMVLUSUTQVIUOVAQPRVJCDSUOVACDUHUIRUPBCUOACUOCUJEUKULV BBDSUNO $. $} @@ -38050,11 +38050,11 @@ Definite description binder (inverted iota) $( Variable substitution in description binder. Compare ~ sb8eu . (Contributed by NM, 18-Mar-2013.) $) sb8iota $p |- ( iota x ph ) = ( iota y [ y / x ] ph ) $= - ( vz vw cv wceq wb wal cab cuni wsb cio nfv sb8 sbbi nfsb nfxfr dfiota2 - eqsb3 nfbi sbequ cbval equsb3 sblbis albii 3bitri abbii unieqi 3eqtr4i ) - ABGEGZHZIZBJZEKZLABCMZCGULHZIZCJZEKZLABNUQCNUPVAUOUTEUOUNBFMZFJUNBCMZCJUT - UNBFUNFOPVBVCFCVBABFMZUMBFMZICAUMBFQVDVECABFCDRVEFGULHZCFBULUAVFCOSUBSVCF - OUNFCBUCUDVCUSCUMURABCCBEUEUFUGUHUIUJABETUQCETUK $. + ( vz vw weq wal cab cuni wsb cio nfv sb8 sbbi nfsb equsb3 nfxfr dfiota2 + wb nfbi sbequ cbval sblbis albii 3bitri abbii unieqi 3eqtr4i ) ABEGZTZBHZ + EIZJABCKZCEGZTZCHZEIZJABLUNCLUMURULUQEULUKBFKZFHUKBCKZCHUQUKBFUKFMNUSUTFC + USABFKZUJBFKZTCAUJBFOVAVBCABFCDPVBFEGZCBFEQVCCMRUARUTFMUKFCBUBUCUTUPCUJUO + ABCBCEQUDUEUFUGUHABESUNCESUI $. $} ${ @@ -39290,47 +39290,46 @@ Definite description binder (inverted iota) preaddccan2lem1 $p |- ( ( N e. Nn /\ P e. Nn ) -> { m | ( ( ( m +c N ) =/= (/) /\ ( m +c N ) = ( m +c P ) ) -> N = P ) } e. _V ) $= - ( vt cv cplc c0 wceq wa cab cvv wcel cpw1 cimak copk 3bitr4i bitri pw1ex - wn vex vn vp wne cnnc addceq2 neeq1d eqeq1d anbi12d imbi1d abbidv eleq1d - wi eqeq2d anbi2d cun imor abbii unab eqtr4i cssetk cins3k cins2k cin c1c - wo ccompl csik csymdif cdif cimagek ccnvk csn elcompl elin 0ex opkelcnvk - elimaksn dfaddc2 eqeq2i eqcom opkelimagek notbii df-ne wrex rexv anbi12i - wex bitr4i exbii elimak addcex eqvinc abbi2i imakex imagekex cnvkex snex - addcexlem complex inex vvex eqeltrri abexv unex eqeltri vtocl2g ) BEZUAE - ZFZGUCZXIXGUBEZFZHZIZCAHZULZBJZKLXGCFZGUCZXRXLHZIZXOULZBJZKLXSXRXGAFZHZI - ZXOULZBJZKLUAUBCAUDUDXHCHZXQYCKYIXPYBBYIXNYAXOYIXJXSXMXTYIXIXRGXHCXGUEZU - FYIXIXRXLYJUGUHUIUJUKXKAHZYCYHKYKYBYGBYKYAYFXOYKXTYEXSYKXLYDXRXKAXGUEUMU - NUIUJUKXQXNSZBJZXOBJZUOZKXQYLXOVEZBJYOXPYPBXNXOUPUQYLXOBURUSYMYNUTVAZUTV - BZVCVDMMZNVFVAYRVBYQVBUTVGVGVAUOVHYSMMNVIZXHMZMZNZVJZVKZGVLZNZVFZUUDYTXK - MZMZNZVJZVCZVKZKNZVCZVFZYMKYLBUUQXGUUQLXGUUPLZSYLXGUUPBTZVMUURXNUURXGUUH - LZXGUUOLZIXNXGUUHUUOVNUUTXJUVAXMXGUUGLZSXIGHZSUUTXJUVBUVCGXGOUUELXGGOUUD - LZUVBUVCGXGUUDVOUUSVPUUEGXGVOUUSVQGXIHGUUCXGNZHUVCUVDXIUVEGXGXHVRZVSXIGV - TXGGUUCUUSVOWAPPWBXGUUGUUSVMXIGWCPDEZXGOUUNLZDKWDZUVGXIHZUVGXLHZIZDWGZUV - AXMUVIUVHDWGUVMUVHDWEUVHUVLDUVHXGUVGOZUUMLZUVLUVGXGUUMDTZUUSVPUVOUVNUUDL - ZUVNUULLZIUVLUVNUUDUULVNUVQUVJUVRUVKUVQUVGUVEHUVJXGUVGUUCUUSUVPWAXIUVEUV - GUVFVSWHUVRUVGUUKXGNZHUVKXGUVGUUKUUSUVPWAXLUVSUVGXGXKVRVSWHWFQQWIQDUUNKX - GUUSWJDXIXLXGXHUUSUATZWKWLPWFQWBQWMUUPUUHUUOUUGUUEUUFUUDUUCYTUUBWRUUAXHU - VTRRWNWOZWPGWQWNWSUUNKUUMUUDUULUWAUUKYTUUJWRUUIXKUBTRRWNWOWTWPXAWNWTWSXB - XOBXCXDXEXF $. + ( vt cv cplc c0 wceq wa cab cvv wcel wn cpw1 cimak vex copk 3bitr4i bitri + pw1ex vn vp wne wi cnnc addceq2 neeq1d eqeq1d imbi1d abbidv eleq1d eqeq2d + anbi12d anbi2d cun wo imor abbii unab eqtr4i cssetk cins3k cins2k cin c1c + ccompl csik csymdif cdif cimagek ccnvk csn elcompl 0ex opkelcnvk elimaksn + elin dfaddc2 eqeq2i eqcom opkelimagek notbii wrex wex rexv bitr4i anbi12i + df-ne exbii elimak addcex eqvinc abbi2i addcexlem imakex imagekex complex + cnvkex snex inex vvex eqeltrri abexv unex eqeltri vtocl2g ) BEZUAEZFZGUCZ + XIXGUBEZFZHZIZCAHZUDZBJZKLXGCFZGUCZXRXLHZIZXOUDZBJZKLXSXRXGAFZHZIZXOUDZBJ + ZKLUAUBCAUEUEXHCHZXQYCKYIXPYBBYIXNYAXOYIXJXSXMXTYIXIXRGXHCXGUFZUGYIXIXRXL + YJUHUMUIUJUKXKAHZYCYHKYKYBYGBYKYAYFXOYKXTYEXSYKXLYDXRXKAXGUFULUNUIUJUKXQX + NMZBJZXOBJZUOZKXQYLXOUPZBJYOXPYPBXNXOUQURYLXOBUSUTYMYNVAVBZVAVCZVDVENNZOV + FVBYRVCYQVCVAVGVGVBUOVHYSNNOVIZXHNZNZOZVJZVKZGVLZOZVFZUUDYTXKNZNZOZVJZVDZ + VKZKOZVDZVFZYMKYLBUUQXGUUQLXGUUPLZMYLXGUUPBPZVMUURXNUURXGUUHLZXGUUOLZIXNX + GUUHUUOVQUUTXJUVAXMXGUUGLZMXIGHZMUUTXJUVBUVCGXGQUUELXGGQUUDLZUVBUVCGXGUUD + VNUUSVOUUEGXGVNUUSVPGXIHGUUCXGOZHUVCUVDXIUVEGXGXHVRZVSXIGVTXGGUUCUUSVNWAR + RWBXGUUGUUSVMXIGWHRDEZXGQUUNLZDKWCZUVGXIHZUVGXLHZIZDWDZUVAXMUVIUVHDWDUVMU + VHDWEUVHUVLDUVHXGUVGQZUUMLZUVLUVGXGUUMDPZUUSVOUVOUVNUUDLZUVNUULLZIUVLUVNU + UDUULVQUVQUVJUVRUVKUVQUVGUVEHUVJXGUVGUUCUUSUVPWAXIUVEUVGUVFVSWFUVRUVGUUKX + GOZHUVKXGUVGUUKUUSUVPWAXLUVSUVGXGXKVRVSWFWGSSWISDUUNKXGUUSWJDXIXLXGXHUUSU + APZWKWLRWGSWBSWMUUPUUHUUOUUGUUEUUFUUDUUCYTUUBWNUUAXHUVTTTWOWPZWRGWSWOWQUU + NKUUMUUDUULUWAUUKYTUUJWNUUIXKUBPTTWOWPWTWRXAWOWTWQXBXOBXCXDXEXF $. $( Cancellation law for natural addition with a non-null condition. (Contributed by SF, 29-Jan-2015.) $) preaddccan2 $p |- ( ( ( M e. Nn /\ N e. Nn /\ P e. Nn ) /\ ( M +c N ) =/= (/) ) -> ( ( M +c N ) = ( M +c P ) <-> N = P ) ) $= - ( vm vk cnnc wcel cplc c0 wne wa wceq wi c0c c1c addceq1 eqeq12d anbi12d - neeq1d imbi1d w3a cv cvv preaddccan2lem1 weq addc32 syl6eq biimpi adantl - addcid2 eqeq12i addcnnul simpld simpll simplrl nncaddccl syl2anc simplrr - a1i ad2antrl simprr simprl prepeano4 syl22anc jca ex imim1d findsd 3impb - expdimp addceq2 impbid1 ) BFGZCFGZAFGZUAZBCHZIJZKVQBAHZLZCALZVPVRVTWAVMV - NVOVRVTKZWAMZDUBZCHZIJZWEWDAHZLZKZWAMNCHZIJZWJNAHZLZKZWAMZEUBZCHZIJZWQWP - AHZLZKZWAMWQOHZIJZXBWSOHZLZKZWAMWCVNVOKZDEBUCADCUDWDNLZWIWNWAXHWFWKWHWMX - HWEWJIWDNCPZSXHWEWJWGWLXIWDNAPQRTDEUEZWIXAWAXJWFWRWHWTXJWEWQIWDWPCPZSXJW - EWQWGWSXKWDWPAPQRTWDWPOHZLZWIXFWAXMWFXCWHXEXMWEXBIXMWEXLCHXBWDXLCPWPOCUF - UGZSXMWEXBWGXDXNXMWGXLAHXDWDXLAPWPOAUFUGQRTWDBLZWIWBWAXOWFVRWHVTXOWEVQIW - DBCPZSXOWEVQWGVSXPWDBAPQRTWOXGWMWAWKWMWAWJCWLACUJAUJUKUHUIUSWPFGZXGKZXFX - AWAXRXFXAXRXFKZWRWTXCWRXRXEXCWROIJWQOULUMUTXSWQFGZWSFGZXEXCWTXSXQVNXTXQX - GXFUNZXQVNVOXFUOWPCUPUQXSXQVOYAYBXQVNVOXFURWPAUPUQXRXCXEVAXRXCXEVBWQWSVC - VDVEVFVGVHVIVJCABVKVL $. + ( vm vk cnnc wcel cplc c0 wne wceq c0c c1c addceq1 neeq1d eqeq12d anbi12d + wa wi imbi1d w3a cv cvv preaddccan2lem1 weq addc32 syl6eq addcid2 eqeq12i + biimpi adantl a1i addcnnul simpld ad2antrl simpll simplrl syl2anc simplrr + nncaddccl simprr simprl prepeano4 syl22anc ex imim1d findsd 3impb expdimp + jca addceq2 impbid1 ) BFGZCFGZAFGZUAZBCHZIJZRVQBAHZKZCAKZVPVRVTWAVMVNVOVR + VTRZWASZDUBZCHZIJZWEWDAHZKZRZWASLCHZIJZWJLAHZKZRZWASZEUBZCHZIJZWQWPAHZKZR + ZWASWQMHZIJZXBWSMHZKZRZWASWCVNVORZDEBUCADCUDWDLKZWIWNWAXHWFWKWHWMXHWEWJIW + DLCNZOXHWEWJWGWLXIWDLANPQTDEUEZWIXAWAXJWFWRWHWTXJWEWQIWDWPCNZOXJWEWQWGWSX + KWDWPANPQTWDWPMHZKZWIXFWAXMWFXCWHXEXMWEXBIXMWEXLCHXBWDXLCNWPMCUFUGZOXMWEX + BWGXDXNXMWGXLAHXDWDXLANWPMAUFUGPQTWDBKZWIWBWAXOWFVRWHVTXOWEVQIWDBCNZOXOWE + VQWGVSXPWDBANPQTWOXGWMWAWKWMWAWJCWLACUHAUHUIUJUKULWPFGZXGRZXFXAWAXRXFXAXR + XFRZWRWTXCWRXRXEXCWRMIJWQMUMUNUOXSWQFGZWSFGZXEXCWTXSXQVNXTXQXGXFUPZXQVNVO + XFUQWPCUTURXSXQVOYAYBXQVNVOXFUSWPAUTURXRXCXEVAXRXCXEVBWQWSVCVDVJVEVFVGVHV + ICABVKVL $. $} ${ @@ -42395,12 +42394,12 @@ Definite description binder (inverted iota) $( The first projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.) $) proj1ex $p |- Proj1 A e. _V $= - ( cvv wcel cproj1 proj1exg ax-mp ) ACDAECDBACFG $. + ( cvv wcel cproj1 proj1exg ax-mp ) ACDAECDBACFG $. $( The second projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.) $) proj2ex $p |- Proj2 A e. _V $= - ( cvv wcel cproj2 proj2exg ax-mp ) ACDAECDBACFG $. + ( cvv wcel cproj2 proj2exg ax-mp ) ACDAECDBACFG $. $} @@ -42734,17 +42733,17 @@ Definite description binder (inverted iota) $( Any class is equal to an ordered pair. (Contributed by Scott Fenton, 8-Apr-2021.) $) opeq $p |- A = <. Proj1 A , Proj2 A >. $= - ( vx vy vz cv cphi wceq wrex cab cun wex crab wcel wa rexeqi rexab ancom - eleq1d 3bitri eqtr4i cproj1 cop c0c csn df-op df-proj1 weq phieq pm5.32i - cproj2 eleq1 bitr4i exbii 19.41v abbii df-rab df-proj2 uneq1d uneq12i wo - unrab rabid2 vex phiall 19.43 mpbi a1i mprgbir 3eqtrri ) AUAZAUJZUBBEZCE - ZFZGZCVJHZBIZVLVNUCUDZJZGZCVKHZBIZJVOCKZBALZVTCKZBALZJZABCVJVKUEVQWDWBWF - VQVLAMZWCNZBIWDVPWIBVPVOCDEZFZAMZDIZHVNAMZVONZCKZWIVOCVJWMDAUFOWLWNVOCDD - CUGZWKVNAWJVMUHZRPWPVOWHNZCKWCWHNWIWOWSCWOVOWNNWSWNVOQVOWHWNVLVNAUKUIULU - MVOWHCUNWCWHQSSUOWCBAUPTWBWHWENZBIWFWAWTBWAVTCWKVRJZAMZDIZHVSAMZVTNZCKZW - TVTCVKXCDAUQOXBXDVTCDWQXAVSAWQWKVNVRWRURRPXFVTWHNZCKWEWHNWTXEXGCXEVTXDNX - GXDVTQVTWHXDVLVSAUKUIULUMVTWHCUNWEWHQSSUOWEBAUPTUSWGWCWEUTZBALZAWCWEBAVA - AXIGXHBAXHBAVBXHWHVOVTUTCKXHCVLBVCVDVOVTCVEVFVGVHTVI $. + ( vx vy vz cv cphi wceq wrex cab cun wex crab wcel wa rexeqi eleq1d rexab + ancom 3bitri eqtr4i cproj1 cop c0c csn df-op df-proj1 phieq eleq1 pm5.32i + cproj2 weq bitr4i exbii 19.41v abbii df-rab df-proj2 uneq1d uneq12i unrab + wo rabid2 vex phiall 19.43 mpbi a1i mprgbir 3eqtrri ) AUAZAUJZUBBEZCEZFZG + ZCVJHZBIZVLVNUCUDZJZGZCVKHZBIZJVOCKZBALZVTCKZBALZJZABCVJVKUEVQWDWBWFVQVLA + MZWCNZBIWDVPWIBVPVOCDEZFZAMZDIZHVNAMZVONZCKZWIVOCVJWMDAUFOWLWNVOCDDCUKZWK + VNAWJVMUGZPQWPVOWHNZCKWCWHNWIWOWSCWOVOWNNWSWNVORVOWHWNVLVNAUHUIULUMVOWHCU + NWCWHRSSUOWCBAUPTWBWHWENZBIWFWAWTBWAVTCWKVRJZAMZDIZHVSAMZVTNZCKZWTVTCVKXC + DAUQOXBXDVTCDWQXAVSAWQWKVNVRWRURPQXFVTWHNZCKWEWHNWTXEXGCXEVTXDNXGXDVTRVTW + HXDVLVSAUHUIULUMVTWHCUNWEWHRSSUOWEBAUPTUSWGWCWEVAZBALZAWCWEBAUTAXIGXHBAXH + BAVBXHWHVOVTVACKXHCVLBVCVDVOVTCVEVFVGVHTVI $. $( A class is a set iff it is equal to an ordered pair. (Contributed by Scott Fenton, 19-Apr-2021.) $) @@ -45460,9 +45459,9 @@ We use their notation ("onto" under the arrow). For alternate $( The cross product of the universe with itself is the universe. (Contributed by Scott Fenton, 14-Apr-2021.) $) xpvv $p |- ( _V X. _V ) = _V $= - ( vx cvv cxp wceq cv wcel eqv cproj1 cproj2 cop vex proj1ex proj2ex opelxp - opeq mpbir2an eqeltri mpgbir ) BBCZBDAEZSFAASGTTHZTIZJZSTOUCSFUABFUBBFTAKZ - LTUDMUAUBBBNPQR $. + ( vx cvv cxp wceq cv wcel eqv cproj1 cproj2 cop opeq proj1ex proj2ex opelxp + vex mpbir2an eqeltri mpgbir ) BBCZBDAEZSFAASGTTHZTIZJZSTKUCSFUABFUBBFTAOZLT + UDMUAUBBBNPQR $. ${ $d x y z w A $. $d x y z w B $. @@ -45697,8 +45696,8 @@ We use their notation ("onto" under the arrow). For alternate rule). Compare ~ abbi2i . (Contributed by Scott Fenton, 18-Apr-2021.) $) opabbi2i $p |- A = { <. x , y >. | ph } $= - ( cv cop wcel copab opabid2 opabbii eqtr3i ) BFCFGDHZBCIDABCIBCDJMABCEKL - $. + ( cv cop wcel copab opabid2 opabbii eqtr3i ) BFCFGDHZBCIDABCIBCDJMABCEKL + $. $} ${ @@ -53314,10 +53313,10 @@ result of an operator (deduction version). (Contributed by Paul 19-Apr-2021.) $) oprabid2 $p |- { <. <. x , y >. , z >. | <. <. x , y >. , z >. e. A } = A $= - ( vw vt vu cv cop wcel coprab cvv wb vex weq opeq1 opeq1d opeq2 eloprabg - eleq1d mp3an eqoprriv ) EFGAHZBHZIZCHZIZDJZABCKZDEHZLJFHZLJGHZLJUJUKIZUL - IZUIJUNDJZMENFNGNUHUJUDIZUFIZDJUMUFIZDJUOABCUJUKULLLLAEOZUGUQDUSUEUPUFUC - UJUDPQTBFOZUQURDUTUPUMUFUDUKUJRQTCGOURUNDUFULUMRTSUAUB $. + ( vw vt vu cv cop wcel coprab cvv wb vex weq opeq1 opeq1d eleq1d eloprabg + opeq2 mp3an eqoprriv ) EFGAHZBHZIZCHZIZDJZABCKZDEHZLJFHZLJGHZLJUJUKIZULIZ + UIJUNDJZMENFNGNUHUJUDIZUFIZDJUMUFIZDJUOABCUJUKULLLLAEOZUGUQDUSUEUPUFUCUJU + DPQRBFOZUQURDUTUPUMUFUDUKUJTQRCGOURUNDUFULUMTRSUAUB $. $} ${ @@ -55044,9 +55043,9 @@ result of an operator (deduction version). (Contributed by Paul 19-Apr-2021.) $) composevalg $p |- ( ( A e. V /\ B e. W ) -> ( A Compose B ) = ( A o. B ) ) $= - ( vx vy wcel wa cvv ccom ccompose co wceq elex adantr adantl coexg coeq1 - cv coeq2 df-compose ovmpt2g syl3anc ) ACGZBDGZHAIGZBIGZABJZIGABKLUHMUDUF - UEACNOUEUGUDBDNPABCDQEFABIIESZFSZJUHKAUJJIUIAUJRUJBATEFUAUBUC $. + ( vx vy wcel wa cvv ccom ccompose co wceq adantr adantl coexg coeq1 coeq2 + elex cv df-compose ovmpt2g syl3anc ) ACGZBDGZHAIGZBIGZABJZIGABKLUHMUDUFUE + ACSNUEUGUDBDSOABCDPEFABIIETZFTZJUHKAUJJIUIAUJQUJBAREFUAUBUC $. $} ${ @@ -55054,11 +55053,11 @@ result of an operator (deduction version). (Contributed by Paul $( The compose function is a function over the universe. (Contributed by Scott Fenton, 19-Apr-2021.) $) composefn $p |- Compose Fn _V $= - ( vx vy vz ccompose cvv wfn cv wcel ccom wceq coprab copab weu vex eueq1 - wa coex a1i fnoprab wb cmpt2 df-compose df-mpt2 eqtri df-xp eqtr3i fneq1 - cxp xpvv fneq2 sylan9bb mp2an mpbir ) DEFZAGZEHBGZEHPZCGUOUPIZJZPABCKZUQ - ABLZFZUQUSABCUSCMUQCURUOUPANBNQORSDUTJZEVAJZUNVBTDABEEURUAUTABUBABCEEURU - CUDEEUHEVAUIABEEUEUFVCUNUTEFVDVBEDUTUGEVAUTUJUKULUM $. + ( vx vy vz ccompose cvv wfn cv wcel ccom wceq coprab copab weu coex eueq1 + wa vex a1i fnoprab wb cmpt2 df-compose df-mpt2 eqtri cxp xpvv df-xp fneq1 + eqtr3i fneq2 sylan9bb mp2an mpbir ) DEFZAGZEHBGZEHPZCGUOUPIZJZPABCKZUQABL + ZFZUQUSABCUSCMUQCURUOUPAQBQNORSDUTJZEVAJZUNVBTDABEEURUAUTABUBABCEEURUCUDE + EUEEVAUFABEEUGUIVCUNUTEFVDVBEDUTUHEVAUTUJUKULUM $. $} $( Binary relationship form of the compose function. (Contributed by Scott @@ -55074,38 +55073,38 @@ result of an operator (deduction version). (Contributed by Paul $( The compose function is a set. (Contributed by Scott Fenton, 19-Apr-2021.) $) composeex $p |- Compose e. _V $= - ( vx vy vw vu vt vv cvv csset cins2 c1c cv wbr wex wcel cop vex otelins2 - wa bitri ins2ex vz ccompose cxp c1st ccnv c2nd cin csi3 cins4 cswap cima - cid cins3 csymdif cdif ccom cmpt2 df-compose copab wceq csn elopab df-co - eleq2i elima1c elin opex oqelins4 otsnelsi3 opelxp mpbiran df-br 3bitr2i - brcnv anbi12i op1st2nd 3bitri snex wel df-clel opelssetsn exbii 3bitr4ri - brswap2 ideq otelins3 releqmpt2 eqtr4i vvex 1stex cnvex xpex 2ndex si3ex - inex ins4ex swapex ssetex 1cex imaex idex ins3ex mpt2exlem eqeltri ) UBG - GUCGUCHIZGUDUEZUCZUFUEZIZUGZUHZUIZUJUHZUIZXEIZIZIZUGZJUKZIZULUHZUIZHUMZI - ZIZIZIZUGZJUKZUGZJUKZUGZJUKZJUKZUMUNJUKUOZGUBABGGAKZBKZUPZUQYOABURABUAGG - YNYRUAKZCKZDKZYQLZUUAEKZYPLZRZDMZCEUSZNYSYTUUCOUTZUUFRZEMZCMZYSYRNYSVAZY - PYQOZOZYNNZUUFCEYSVBYRUUGYSCEDYPYQVCVDUUOYTVAZUUNOZYMNZCMUUKCUUNYMVEUURU - UJCUURUUCVAZUUQOZYLNZEMUUJEUUQYLVEUVAUUIEUVAUUTXLNZUUTYKNZRUUIUUTXLYKVFU - VBUUHUVCUUFUVBUUSUUPUULOOXKNUUCYTYSOZOZXJNZUUHUUSUUPUULUUMXKYPYQAPZBPZVG - ZVHUUCYTYSXJEPZCPZUAPVIUVFUVEXGNZUVEXINZRYSYTUDLZYSUUCUFLZRUUHUVEXGXIVFU - VLUVNUVMUVOUVLUVDXFNZYTYSXFLUVNUVLUUCGNUVPUVJUUCUVDGXFVJVKYTYSXFVLYTYSUD - VNVMUVMUUCYSOXHNUUCYSXHLUVOUUCYTYSXHUVKQUUCYSXHVLUUCYSUFVNVMVOYTUUCYSUVK - UVJVPVQVQUVCUUAVAZUUTOZYJNZDMUUFDUUTYJVEUVSUUEDUVSUVRXTNZUVRYINZRUUEUVRX - TYIVFUVTUUBUWAUUDUVTUVQUUQOZXSNZUUBUVQUUSUUQXSUUCVRZQYTUUAOZYQNUUCUWEUTZ - EBVSZRZEMZUUBUWCEUWEYQVTYTUUAYQVLUWCUUSUWBOZXRNZEMUWIEUWBXRVEUWKUWHEUWKU - WJXNNZUWJXQNZRUWHUWJXNXQVFUWLUWFUWMUWGUWLUUSUVQUUPOOXMNZUWFUUSUVQUUPUUNX - MUULUUMYSVRZUVIVGZVHUWNUUCUUAYTOZOUJNUUCUWQUJLUWFUUCUUAYTUJUVJDPZUVKVIUU - CUWQUJVLUUCUUAYTUWRUVKWDVMSUWMUUTXPNUUSUUNOXONZUWGUUSUVQUUQXPUUAVRZQUUSU - UPUUNXOYTVRZQUWSUUSUUMOXENUUSYQOHNUWGUUSUULUUMXEUWOQUUSYPYQHUVGQUUCYQUVJ - UVHWAVQVQVOSWBSWCSUUAUUCOZYPNFKZUXBUTZFAVSZRZFMZUUDUWAFUXBYPVTUUAUUCYPVL - UWAUXCVAZUVROZYHNZFMUXGFUVRYHVEUXJUXFFUXJUXIYBNZUXIYGNZRUXFUXIYBYGVFUXKU - XDUXLUXEUXKUXHUVQUUSOOYANZUXDUXHUVQUUSUUQYAUUPUUNUXAUWPVGVHUXMUXCUXBOULN - UXCUXBULLUXDUXCUUAUUCULFPZUWRUVJVIUXCUXBULVLUXCUXBUUAUUCUWRUVJVGWEVMSUXL - UXHUUTOYFNUXHUUQOYENZUXEUXHUVQUUTYFUWTQUXHUUSUUQYEUWDQUXOUXHUUNOYDNUXHUU - MOYCNZUXEUXHUUPUUNYDUXAQUXHUULUUMYCUWOQUXPUXHYPOHNUXEUXHYPYQHUVHWFUXCYPU - XNUVGWASVQVQVOSWBSWCVOSWBSVOSWBSWBSWCWGWHGGYNWIWIYMJYLJXLYKXKXJXGXIGXFWI - UDWJWKWLXHUFWMWKTWOWNWPYJJXTYIXSXRJXNXQXMUJWQWNWPXPXOXEHWRTTTTWOWSWTTYHJ - YBYGYAULXAWNWPYFYEYDYCHWRXBTTTTWOWSWTWOWSWTWOWSWTWSWTXCXD $. + ( vx vy vw vu vt vv cvv csset cins2 c1c cv wbr wa wex wcel otelins2 bitri + cop vex ins2ex vz ccompose cxp c1st ccnv c2nd csi3 cins4 cswap cima cins3 + cin cid csymdif cdif ccom cmpt2 df-compose copab wceq elopab df-co eleq2i + elima1c elin opex oqelins4 otsnelsi3 opelxp mpbiran df-br 3bitr2i anbi12i + csn brcnv op1st2nd 3bitri snex wel df-clel opelssetsn exbii 3bitr4ri ideq + brswap2 otelins3 releqmpt2 eqtr4i vvex 1stex cnvex xpex 2ndex inex ins4ex + si3ex swapex ssetex 1cex imaex idex ins3ex mpt2exlem eqeltri ) UBGGUCGUCH + IZGUDUEZUCZUFUEZIZULZUGZUHZUIUGZUHZXEIZIZIZULZJUJZIZUMUGZUHZHUKZIZIZIZIZU + LZJUJZULZJUJZULZJUJZJUJZUKUNJUJUOZGUBABGGAKZBKZUPZUQYOABURABUAGGYNYRUAKZC + KZDKZYQLZUUAEKZYPLZMZDNZCEUSZOYSYTUUCRUTZUUFMZENZCNZYSYROYSVNZYPYQRZRZYNO + ZUUFCEYSVAYRUUGYSCEDYPYQVBVCUUOYTVNZUUNRZYMOZCNUUKCUUNYMVDUURUUJCUURUUCVN + ZUUQRZYLOZENUUJEUUQYLVDUVAUUIEUVAUUTXLOZUUTYKOZMUUIUUTXLYKVEUVBUUHUVCUUFU + VBUUSUUPUULRRXKOUUCYTYSRZRZXJOZUUHUUSUUPUULUUMXKYPYQASZBSZVFZVGUUCYTYSXJE + SZCSZUASVHUVFUVEXGOZUVEXIOZMYSYTUDLZYSUUCUFLZMUUHUVEXGXIVEUVLUVNUVMUVOUVL + UVDXFOZYTYSXFLUVNUVLUUCGOUVPUVJUUCUVDGXFVIVJYTYSXFVKYTYSUDVOVLUVMUUCYSRXH + OUUCYSXHLUVOUUCYTYSXHUVKPUUCYSXHVKUUCYSUFVOVLVMYTUUCYSUVKUVJVPVQVQUVCUUAV + NZUUTRZYJOZDNUUFDUUTYJVDUVSUUEDUVSUVRXTOZUVRYIOZMUUEUVRXTYIVEUVTUUBUWAUUD + UVTUVQUUQRZXSOZUUBUVQUUSUUQXSUUCVRZPYTUUARZYQOUUCUWEUTZEBVSZMZENZUUBUWCEU + WEYQVTYTUUAYQVKUWCUUSUWBRZXROZENUWIEUWBXRVDUWKUWHEUWKUWJXNOZUWJXQOZMUWHUW + JXNXQVEUWLUWFUWMUWGUWLUUSUVQUUPRRXMOZUWFUUSUVQUUPUUNXMUULUUMYSVRZUVIVFZVG + UWNUUCUUAYTRZRUIOUUCUWQUILUWFUUCUUAYTUIUVJDSZUVKVHUUCUWQUIVKUUCUUAYTUWRUV + KWEVLQUWMUUTXPOUUSUUNRXOOZUWGUUSUVQUUQXPUUAVRZPUUSUUPUUNXOYTVRZPUWSUUSUUM + RXEOUUSYQRHOUWGUUSUULUUMXEUWOPUUSYPYQHUVGPUUCYQUVJUVHWAVQVQVMQWBQWCQUUAUU + CRZYPOFKZUXBUTZFAVSZMZFNZUUDUWAFUXBYPVTUUAUUCYPVKUWAUXCVNZUVRRZYHOZFNUXGF + UVRYHVDUXJUXFFUXJUXIYBOZUXIYGOZMUXFUXIYBYGVEUXKUXDUXLUXEUXKUXHUVQUUSRRYAO + ZUXDUXHUVQUUSUUQYAUUPUUNUXAUWPVFVGUXMUXCUXBRUMOUXCUXBUMLUXDUXCUUAUUCUMFSZ + UWRUVJVHUXCUXBUMVKUXCUXBUUAUUCUWRUVJVFWDVLQUXLUXHUUTRYFOUXHUUQRYEOZUXEUXH + UVQUUTYFUWTPUXHUUSUUQYEUWDPUXOUXHUUNRYDOUXHUUMRYCOZUXEUXHUUPUUNYDUXAPUXHU + ULUUMYCUWOPUXPUXHYPRHOUXEUXHYPYQHUVHWFUXCYPUXNUVGWAQVQVQVMQWBQWCVMQWBQVMQ + WBQWBQWCWGWHGGYNWIWIYMJYLJXLYKXKXJXGXIGXFWIUDWJWKWLXHUFWMWKTWNWPWOYJJXTYI + XSXRJXNXQXMUIWQWPWOXPXOXEHWRTTTTWNWSWTTYHJYBYGYAUMXAWPWOYFYEYDYCHWRXBTTTT + WNWSWTWNWSWTWNWSWTWSWTXCXD $. $} ${ @@ -62472,8 +62471,8 @@ the first case of his notation (simple exponentiation) and subscript it $( The domain of the singleton function. (Contributed by Scott Fenton, 20-Apr-2021.) $) dmsnfn $p |- dom ( x e. A |-> { x } ) = A $= - ( cv csn cvv wcel crab wa cab cmpt df-rab eqid dmmpt snex biantru abbi2i - cdm 3eqtr4i ) ACZDZEFZABGSBFZUAHZAIABTJZQBUAABKABTUDUDLMUCABUAUBSNOPR $. + ( cv csn cvv wcel crab cab cmpt cdm df-rab eqid dmmpt snex biantru abbi2i + wa 3eqtr4i ) ACZDZEFZABGSBFZUAQZAHABTIZJBUAABKABTUDUDLMUCABUAUBSNOPR $. $} ${ @@ -62481,8 +62480,8 @@ the first case of his notation (simple exponentiation) and subscript it $( Version of ~ epelc with a restriction in place. (Contributed by Scott Fenton, 20-Apr-2021.) $) epelcres $p |- ( X e. A -> ( X ( _E |` A ) Y <-> X e. Y ) ) $= - ( wcel cep wbr wa cres iba bicomd brres epelc bicomi 3bitr4g ) BAEZBCFGZ - PHZQBCFAIGBCEZPQRPQJKBCFALQSBCDMNO $. + ( wcel cep wbr wa cres iba bicomd brres epelc bicomi 3bitr4g ) BAEZBCFGZP + HZQBCFAIGBCEZPQRPQJKBCFALQSBCDMNO $. $} ${ @@ -62490,16 +62489,16 @@ the first case of his notation (simple exponentiation) and subscript it $( Membership in the class of Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.) $) elcan $p |- ( A e. Can <-> ~P1 A ~~ A ) $= - ( vx ccan wcel cvv cpw1 cen wbr elex brrelrnex wceq pw1eq breq12d df-can - cv id elab2g pm5.21nii ) ACDAEDAFZAGHZACISAGJBOZFZUAGHTBACEUAAKZUBSUAAGU - AALUCPMBNQR $. + ( vx ccan wcel cvv cpw1 cen wbr elex brrelrnex cv pw1eq id breq12d df-can + wceq elab2g pm5.21nii ) ACDAEDAFZAGHZACISAGJBKZFZUAGHTBACEUAAPZUBSUAAGUAA + LUCMNBOQR $. $( Membership in the class of strongly Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.) $) elscan $p |- ( A e. SCan <-> ( x e. A |-> { x } ) e. _V ) $= - ( vy cscan wcel cvv csn cmpt elex cdm dmsnfn dmexg syl5eqelr wceq mpteq1 - cv eleq1d df-scan elab2g pm5.21nii ) BDEBFEABAPGZHZFEZBDIUCBUBJFABKUBFLM - ACPZUAHZFEUCCBDFUDBNUEUBFAUDBUAOQCARST $. + ( vy cscan wcel cvv cv csn cmpt elex dmsnfn dmexg syl5eqelr mpteq1 eleq1d + cdm wceq df-scan elab2g pm5.21nii ) BDEBFEABAGHZIZFEZBDJUCBUBPFABKUBFLMAC + GZUAIZFEUCCBDFUDBQUEUBFAUDBUANOCARST $. $} ${ @@ -62507,29 +62506,29 @@ the first case of his notation (simple exponentiation) and subscript it $( Strongly Cantorian implies Cantorian. Observation from [Holmes], p. 134. (Contributed by Scott Fenton, 19-Apr-2021.) $) scancan $p |- ( A e. SCan -> A e. Can ) $= - ( vx vy vz cv csn cmpt cvv wcel cpw1 cen wbr cscan wfn ccnv wceq weu wa - weq copab ccan wf1o snex eqid fnmpti wrex elpw1 euequ1 eqeq1 vex equcom - sneqb bitri syl6bb eubidv mpbiri rexlimivw sylbi df-mpt cnvopab snelpw1 - cnveqi eleq1 syl6rbb pm5.32ri opabbii 3eqtri fnopab dff1o4 f1oeng mpan2 - mpbir2an ensymi syl elscan elcan 3imtr4i ) BABEZFZGZHIZAJZAKLZAMIAUAIWA - AWBKLZWCWAAWBVTUBZWDWEVTANVTOZWBNBAVSVTVRUCVTUDUECEZVSPZCBWBWFWGWBIZWGD - EZFZPZDAUFWHBQZDWGAUGWLWMDAWLWMBDSZBQBDUHWLWHWNBWLWHWKVSPZWNWGWKVSUIWOD - BSWNWJVRDUJULDBUKUMUNUOUPUQURWFVRAIZWHRZBCTZOWQCBTWIWHRZCBTVTWRBCAVSUSV - BWQBCUTWQWSCBWHWPWIWHWIVSWBIWPWGVSWBVCVRAVAVDVEVFVGVHAWBVTVIVLAWBHVTVJV - KAWBVMVNBAVOAVPVQ $. + ( vx vy vz cv csn cmpt cvv wcel cpw1 cen wbr cscan wfn ccnv weu weq copab + wceq wa ccan wf1o snex eqid fnmpti elpw1 euequ1 eqeq1 sneqb equcom syl6bb + wrex vex bitri eubidv mpbiri rexlimivw sylbi df-mpt cnvopab eleq1 snelpw1 + cnveqi syl6rbb pm5.32ri 3eqtri fnopab dff1o4 mpbir2an f1oeng mpan2 ensymi + opabbii syl elscan elcan 3imtr4i ) BABEZFZGZHIZAJZAKLZAMIAUAIWAAWBKLZWCWA + AWBVTUBZWDWEVTANVTOZWBNBAVSVTVRUCVTUDUECEZVSSZCBWBWFWGWBIZWGDEZFZSZDAULWH + BPZDWGAUFWLWMDAWLWMBDQZBPBDUGWLWHWNBWLWHWKVSSZWNWGWKVSUHWODBQWNWJVRDUMUID + BUJUNUKUOUPUQURWFVRAIZWHTZBCRZOWQCBRWIWHTZCBRVTWRBCAVSUSVCWQBCUTWQWSCBWHW + PWIWHWIVSWBIWPWGVSWBVAVRAVBVDVEVMVFVGAWBVTVHVIAWBHVTVJVKAWBVLVNBAVOAVPVQ + $. $} $( The cardinality of a Cantorian set is equal to the cardinality of its unit power set. (Contributed by Scott Fenton, 23-Apr-2021.) $) canncb $p |- ( A e. V -> ( A e. Can <-> Nc ~P1 A = Nc A ) ) $= - ( wcel cpw1 cnc wceq cen wbr ccan cvv wb pw1exg eqncg syl elcan syl6rbbr ) - ABCZADZEAEFZRAGHZAICQRJCSTKABLRAJMNAOP $. + ( wcel cpw1 cnc wceq cen wbr ccan cvv wb pw1exg eqncg syl elcan syl6rbbr ) + ABCZADZEAEFZRAGHZAICQRJCSTKABLRAJMNAOP $. $( The cardinality of a Cantorian set is equal to the cardinality of its unit power set. (Contributed by Scott Fenton, 21-Apr-2021.) $) cannc $p |- ( A e. Can -> Nc ~P1 A = Nc A ) $= - ( ccan wcel cpw1 cnc wceq canncb ibi ) ABCADEAEFABGH $. + ( ccan wcel cpw1 cnc wceq canncb ibi ) ABCADEAEFABGH $. $( The cardinality of a Cantorian set is strictly less than the cardinality of its power set. (Contributed by Scott Fenton, 21-Apr-2021.) $)