From 380eecbbed1b9ee25556964c25773fbdd5612178 Mon Sep 17 00:00:00 2001 From: Benoit <41090811+benjub@users.noreply.github.com> Date: Fri, 29 Dec 2023 11:24:39 +0100 Subject: [PATCH] Comment edits; epsilon-->membership, rephrasings. (#3717) --- set.mm | 281 +++++++++++++++++++++++++++++++-------------------------- 1 file changed, 154 insertions(+), 127 deletions(-) diff --git a/set.mm b/set.mm index 0a15057485..95b616b3bc 100644 --- a/set.mm +++ b/set.mm @@ -25633,7 +25633,7 @@ the definition of class equality ( ~ df-cleq ). Its forward implication ( wceq wb eqeq2 ax-mp ) ABECAECBEFDABCGH $. $} - $( Equality relationship among 4 classes. (Contributed by NM, + $( Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.) $) eqeq12 $p |- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) ) $= ( wceq eqeq1 eqeq2 sylan9bb ) ABEACEBCECDEBDEABCFCDBGH $. @@ -36183,12 +36183,12 @@ technically classes despite morally (and provably) being sets, like ` 1 ` dfss $p |- ( A C_ B <-> A = ( A i^i B ) ) $= ( wss cin wceq df-ss eqcom bitri ) ABCABDZAEAIEABFIAGH $. - $( Define proper subclass relationship between two classes. Definition 5.9 - of [TakeutiZaring] p. 17. For example, ` { 1 , 2 } C. { 1 , 2 , 3 } ` - ( ~ ex-pss ). Note that ` -. A C. A ` (proved in ~ pssirr ). Contrast - this relationship with the relationship ` A C_ B ` (as defined in - ~ df-ss ). Other possible definitions are given by ~ dfpss2 and - ~ dfpss3 . (Contributed by NM, 7-Feb-1996.) $) + $( Define proper subclass (or strict subclass) relationship between two + classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, + ` { 1 , 2 } C. { 1 , 2 , 3 } ` ( ~ ex-pss ). Note that ` -. A C. A ` + (proved in ~ pssirr ). Contrast this relationship with the relationship + ` A C_ B ` (as defined in ~ df-ss ). Other possible definitions are given + by ~ dfpss2 and ~ dfpss3 . (Contributed by NM, 7-Feb-1996.) $) df-pss $a |- ( A C. B <-> ( A C_ B /\ A =/= B ) ) $. ${ @@ -36257,7 +36257,7 @@ technically classes despite morally (and provably) being sets, like ` 1 ` ${ sseli.1 $e |- A C_ B $. - $( Membership inference from subclass relationship. (Contributed by NM, + $( Membership implication from subclass relationship. (Contributed by NM, 5-Aug-1993.) $) sseli $p |- ( C e. A -> C e. B ) $= ( wss wcel wi ssel ax-mp ) ABECAFCBFGDABCHI $. @@ -36346,16 +36346,16 @@ technically classes despite morally (and provably) being sets, like ` 1 ` ${ $d x A $. $d x B $. $d x C $. - $( Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. - (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, - 14-Jun-2011.) $) + $( Transitivity of subclass relationship. Exercise 5 of [TakeutiZaring] + p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew + Salmon, 14-Jun-2011.) $) sstr2 $p |- ( A C_ B -> ( B C_ C -> A C_ C ) ) $= ( vx wss cv wcel wi wal ssel imim1d alimdv dfss2 3imtr4g ) ABEZDFZBGZPCGZ HZDIPAGZRHZDIBCEACEOSUADOTQRABPJKLDBCMDACMN $. $} - $( Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by - NM, 5-Sep-2003.) $) + $( Transitivity of subclass relationship. Theorem 6 of [Suppes] p. 23. + (Contributed by NM, 5-Sep-2003.) $) sstr $p |- ( ( A C_ B /\ B C_ C ) -> A C_ C ) $= ( wss sstr2 imp ) ABDBCDACDABCEF $. @@ -36436,9 +36436,9 @@ technically classes despite morally (and provably) being sets, like ` 1 ` ( wss wceq eqss sylanbrc ) ABCFCBFBCGDEBCHI $. $} - $( If a class is a subclass of another class, the classes are equal iff the - other class is a subclass of the first class. (Contributed by AV, - 23-Dec-2020.) $) + $( If a class is a subclass of another class, then the classes are equal if + and only if the other class is a subclass of the first class. + (Contributed by AV, 23-Dec-2020.) $) sssseq $p |- ( B C_ A -> ( A C_ B <-> A = B ) ) $= ( wceq wss eqss rbaibr ) ABCABDBADABEF $. @@ -50563,9 +50563,13 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few $d x y z R $. $d x y z A $. $( Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see ~ dffr2 and - ~ dffr3 . (Contributed by NM, 3-Apr-1994.) $) + ~ dffr3 . A class is called well-founded when the membership relation + ` _E ` (see ~ df-eprel ) is well-founded on it, that is, ` A ` is + well-founded if ` _E Fr A ` (some sources request that the membership + relation be well-founded on its transitive closure). (Contributed by + NM, 3-Apr-1994.) $) df-fr $a |- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> - E. y e. x A. z e. x -. z R y ) ) $. + E. y e. x A. z e. x -. z R y ) ) $. $( Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.) $) @@ -50772,14 +50776,13 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few PVHBWAVOVGVNVFVEFUKULUMUNUOUPURUQUSUTVA $. $} - $( Irreflexivity of the epsilon relation: a class founded by epsilon is not a - member of itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario - Carneiro, 22-Jun-2015.) $) + $( A well-founded class does not belong to itself. (Contributed by NM, + 18-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) $) efrirr $p |- ( _E Fr A -> -. A e. A ) $= ( cep wfr wcel wa wbr frirr wb epelg adantl mtbid pm2.01da ) ABCZAADZMNEAAB FZNAABGNONHMAAAIJKL $. - $( A set founded by epsilon contains no 2-cycle loops. (Contributed by NM, + $( A well-founded class contains no 2-cycle loops. (Contributed by NM, 19-Apr-1994.) $) efrn2lp $p |- ( ( _E Fr A /\ ( B e. A /\ C e. A ) ) -> -. ( B e. C /\ C e. B ) ) $= @@ -50788,8 +50791,8 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few ${ $d x y A $. - $( The epsilon relation is set-like on any class. (This is the origin of - the term "set-like": a set-like relation "acts like" the epsilon + $( The membership relation is set-like on any class. (This is the origin + of the term "set-like": a set-like relation "acts like" the membership relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.) $) epse $p |- _E Se A $= @@ -50798,8 +50801,8 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few UHIUEBUDUEUCUDJCUCMNOCQPUEBARSTCBADUAUB $. $} - $( Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom - of Regularity is not required due to antecedent ` _E Fr A ` . + $( Similar to Theorem 7.2 of [TakeutiZaring] p. 35, except that the Axiom of + Regularity is not required due to the antecedent ` _E Fr A ` . (Contributed by NM, 4-May-1994.) $) tz7.2 $p |- ( ( Tr A /\ _E Fr A /\ B e. A ) -> ( B C_ A /\ B =/= A ) ) $= ( wtr cep wfr wcel wss wne wa trss wn wceq efrirr eleq1 syl5ibrcom necon2ad @@ -50809,7 +50812,7 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few ${ $d x y z A $. - $( An alternate way of saying that the epsilon relation is well-founded. + $( An alternate way of saying that the membership relation is well-founded. (Contributed by NM, 17-Feb-2004.) (Revised by Mario Carneiro, 23-Jun-2015.) $) dfepfr $p |- ( _E Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> @@ -50823,9 +50826,8 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few ${ $d x y A $. $d x y B $. epfrc.1 $e |- B e. _V $. - $( A subset of an epsilon-founded class has a minimal element. - (Contributed by NM, 17-Feb-2004.) (Revised by David Abernethy, - 22-Feb-2011.) $) + $( A subset of a well-founded class has a minimal element. (Contributed by + NM, 17-Feb-2004.) (Revised by David Abernethy, 22-Feb-2011.) $) epfrc $p |- ( ( _E Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) ) $= ( vy cep wfr wss c0 wne w3a cv wbr crab wceq wrex cin frc wel dfin5 epel @@ -50860,16 +50862,16 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few weso $p |- ( R We A -> R Or A ) $= ( wwe wfr wor df-we simprbi ) ABCABDABEABFG $. - $( The elements of an epsilon well-ordering are comparable. (Contributed by - NM, 17-May-1994.) $) + $( The elements of a class well-ordered by membership are comparable. + (Contributed by NM, 17-May-1994.) $) wecmpep $p |- ( ( _E We A /\ ( x e. A /\ y e. A ) ) -> ( x e. y \/ x = y \/ y e. x ) ) $= ( cep wwe wor cv wcel wa weq w3o weso solin epel biid 3orbi123i sylib sylan wbr ) CDECDFZAGZCHBGZCHIZUAUBHZABJZUBUAHZKZCDLTUCIUAUBDSZUEUBUADSZKUGCUAUBD MUHUDUEUEUIUFBUANUEOAUBNPQR $. - $( An epsilon well-ordering is a transitive relation. (Contributed by NM, - 22-Apr-1994.) $) + $( On a class well-ordered by membership, the membership predicate is + transitive. (Contributed by NM, 22-Apr-1994.) $) wetrep $p |- ( ( _E We A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x e. y /\ y e. z ) -> x e. z ) ) $= ( cep wwe cv wcel w3a wa wbr wel wor weso sotr sylan epel anbi12i 3imtr3g @@ -50878,9 +50880,9 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few ${ $d y z A $. $d x y z B $. - $( A nonempty (possibly proper) subclass of a class well-ordered by ` _E ` - has a minimal element. Special case of Proposition 6.26 of - [TakeutiZaring] p. 31. (Contributed by NM, 17-Feb-2004.) $) + $( A nonempty subclass of a class well-ordered by membership has a minimal + element. Special case of Proposition 6.26 of [TakeutiZaring] p. 31. + (Contributed by NM, 17-Feb-2004.) $) wefrc $p |- ( ( _E We A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) ) $= ( vy vz cep wwe wss c0 wne cv cin wceq wrex wi wcel wa eqeq1d ex wel wess @@ -50917,10 +50919,10 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few UTVAVDUSVFUTVAVDSSUSVFMUTVAVDABCDFEUDUFUGUHUIURUSUTVEVAURUTMDETZVEURCETUT VGCEUJDCEUKULABDEUMUNUOVCADUQUP $. - $( All nonempty (possibly proper) subclasses of ` A ` , which has a - well-founded relation ` R ` , have ` R `-minimal elements. Proposition - 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, - 29-Jan-2011.) (Revised by Mario Carneiro, 24-Jun-2015.) $) + $( All nonempty subclasses of a class having a well-ordered and set-like + relation have a minimal element for that relation. Proposition 6.26 of + [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) + (Revised by Mario Carneiro, 24-Jun-2015.) $) wereu2 $p |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E! x e. B A. y e. B -. y R x ) $= ( vz vw wa c0 cv wbr wn wral wrex wcel wi breq1 syl5bi sylc ad2antrr wrmo @@ -51053,7 +51055,10 @@ Contrast with domain (defined in ~ df-dm ). For alternate definitions, which normally allows the exponent to be a complex number). Another example is that ` ( F = { <. 2 , 6 >. , <. 3 , 9 >. } ` ` /\ B = { 1 , 2 } ) -> ( F |`` B ) = { <. 2 , 6 >. } ` ( ~ ex-res ). - (Contributed by NM, 2-Aug-1994.) $) + We do not introduce a special syntax for the corestriction of a class: + it will be expressed either as the intersection + ` ( A i^i ( _V X. B ) ) ` or as the converse of the restricted converse + (see ~ cnvrescnv ). (Contributed by NM, 2-Aug-1994.) $) df-res $a |- ( A |` B ) = ( A i^i ( B X. _V ) ) $. $( Define the image of a class (as restricted by another class). @@ -52234,8 +52239,8 @@ Contrast with domain (defined in ~ df-dm ). For alternate definitions, ${ $d A y $. $d B y $. $d x y $. - $( The maps-to notation always describes a relationship. (Contributed by - Scott Fenton, 16-Apr-2012.) $) + $( The maps-to notation always describes a binary relation. (Contributed + by Scott Fenton, 16-Apr-2012.) $) mptrel $p |- Rel ( x e. A |-> B ) $= ( vy cv wcel wceq wa cmpt df-mpt relopabi ) AEBFDECGHADABCIADBCJK $. $} @@ -54415,7 +54420,7 @@ the restriction (of the relation) to the singleton containing this ${ $d A x $. epini.1 $e |- A e. _V $. - $( Any set is equal to its preimage under the converse epsilon relation. + $( Any set is equal to its preimage under the converse membership relation. (Contributed by Mario Carneiro, 9-Mar-2013.) $) epini $p |- ( `' _E " { A } ) = A $= ( vx cep ccnv csn cima cv wbr cvv wb vex eliniseg ax-mp epeli bitri eqriv @@ -55092,8 +55097,9 @@ the restriction (of the relation) to the singleton containing this ( cxp crn wceq c0 rn0 xpeq2 xp0 syl6eq rneqd id 3eqtr4a rnxp pm2.61ine ) AA BZCZADAEAEDZECEPAFQOEQOAEBEAEAGAHIJQKLAAMN $. - $( A Cartesian product subclass relationship is equivalent to the - relationship for it components. (Contributed by NM, 17-Dec-2008.) $) + $( A Cartesian product subclass relationship is equivalent to the conjunction + of the analogous relationships for the factors. (Contributed by NM, + 17-Dec-2008.) $) ssxpb $p |- ( ( A X. B ) =/= (/) -> ( ( A X. B ) C_ ( C X. D ) <-> ( A C_ C /\ B C_ D ) ) ) $= ( cxp c0 wne wss wa cdm wceq xpnz dmxp adantl sylbir adantr eqsstrrd syl6ss @@ -55102,8 +55108,10 @@ the restriction (of the relation) to the singleton containing this MNOPULURUQHUJUIUKSNQCDUARUPBUKTZDUPBUITZVDUJVEBKZULUJVBVFVCUTVFVAABUBPOPULV EVDHUJUIUKUCNQCDUDRUEUFACBDUGUH $. - $( The Cartesian product of nonempty classes is one-to-one. (Contributed by - NM, 31-May-2008.) $) + $( The Cartesian product of nonempty classes is a one-to-one "function" of + its two "arguments". In other words, two Cartesian products, at least one + with nonempty factors, are equal if and only if their respective factors + are equal. (Contributed by NM, 31-May-2008.) $) xp11 $p |- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( A X. B ) = ( C X. D ) <-> ( A = C /\ B = D ) ) ) $= ( c0 wne wa cxp wceq wi xpnz anidm neeq1 anbi2d syl5bbr wss ssxpb syl5ibcom @@ -55135,8 +55143,12 @@ the restriction (of the relation) to the singleton containing this ${ $d x y A $. $d x y B $. $d x y C $. - $( Subset of the range of a restriction. (Contributed by NM, 16-Jan-2006.) - (Proof shortened by Peter Mazsa, 2-Oct-2022.) $) + $( Two ways to express surjectivity of a restricted and corestricted binary + relation (intersection of a binary relation with a Cartesian product): + the LHS expresses inclusion in the range of the restricted relation, + while the RHS expresses equality with the range of the restricted and + corestricted relation. (Contributed by NM, 16-Jan-2006.) (Proof + shortened by Peter Mazsa, 2-Oct-2022.) $) ssrnres $p |- ( B C_ ran ( C |` A ) <-> ran ( C i^i ( A X. B ) ) = B ) $= ( vy vx cxp cin crn wceq wss cres inss2 rnssi rnxpss sstri cv wcel wex wa elrn2 eqss mpbiran inxpssres sstr mpan2 cop ssel syl6ib opelinxp opelresi @@ -55149,8 +55161,10 @@ the restriction (of the relation) to the singleton containing this ${ $d x y A $. $d y B $. $d x y C $. - $( Range of the intersection with a Cartesian product. (Contributed by NM, - 17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) $) + $( Two ways to express surjectivity of a restricted and corestricted binary + relation (intersection of a binary relation with a Cartesian product). + (Contributed by NM, 17-Jan-2006.) (Proof shortened by Andrew Salmon, + 27-Aug-2011.) $) rninxp $p |- ( ran ( C i^i ( A X. B ) ) = B <-> A. y e. B E. x e. A x C y ) $= ( cres crn wss wcel wral cxp cin wceq wbr wrex dfss3 ssrnres cima df-ima @@ -55160,8 +55174,9 @@ the restriction (of the relation) to the singleton containing this ${ $d x A $. $d x y B $. $d x y C $. - $( Domain of the intersection with a Cartesian product. (Contributed by - NM, 17-Jan-2006.) $) + $( Two ways to express totality of a restricted and corestricted binary + relation (intersection of a binary relation with a Cartesian product). + (Contributed by NM, 17-Jan-2006.) $) dminxp $p |- ( dom ( C i^i ( A X. B ) ) = A <-> A. x e. A E. y e. B x C y ) $= ( cxp cin cdm wceq ccnv crn cv wbr wrex wral dfdm4 cnvin cnvxp eqtri vex @@ -55170,8 +55185,9 @@ the restriction (of the relation) to the singleton containing this QVCUMULCDRUASUBSUCBADCULUDUSVAACURUTBDUPUQEBTATUEUFUGUH $. $} - $( Image of a relation restricted to a rectangular region. (Contributed by - Stefan O'Rear, 19-Feb-2015.) $) + $( Image by a restricted and corestricted binary relation (intersection of a + binary relation with a Cartesian product). (Contributed by Stefan O'Rear, + 19-Feb-2015.) $) imainrect $p |- ( ( G i^i ( A X. B ) ) " Y ) = ( ( G " ( Y i^i A ) ) i^i B ) $= ( cxp cin cres crn cima df-res rneqi df-ima eqtri ineq1i ccnv ineq2i eqtr4i @@ -55183,8 +55199,8 @@ the restriction (of the relation) to the singleton containing this DVEWECDARUGPCUSVSUHQNVRVSVNUHMUIUKVKVJBREZFVQVJBJVPWFVJRBULPQTUMBVJSZFWGBFV LVHBWGUDVJBUNVGWGBVFUONTUTUOTQUI $. - $( The image by a constant function (or other Cartesian product). - (Contributed by Thierry Arnoux, 4-Feb-2017.) $) + $( Direct image by a Cartesian product. (Contributed by Thierry Arnoux, + 4-Feb-2017.) $) xpima $p |- ( ( A X. B ) " C ) = if ( ( A i^i C ) = (/) , (/) , B ) $= ( cxp cima cin c0 wceq cif wa wn wo exmid crn cvv rneqi syl6eq syl5eq ancli cres df-ima df-res eqtri inxp inv1 xpeq2i 3eqtri xpeq1 0xp rneqd df-ne rnxp @@ -55193,20 +55209,20 @@ the restriction (of the relation) to the singleton containing this CUAVPVLUTCUBPUCVLVOABCOUDPVOVJVNBVBBUEUFPUGZVCVKGNGVCVJGVCVJGBDGVBGBUHBUIQU JUMQRSVFVGVFVAVKBVQVFVBGUNVKBHVBGUKVBBULUORSUPUQVCVAGBURUS $. - $( The image by a Cartesian product. (Contributed by Thierry Arnoux, - 16-Dec-2017.) $) + $( Direct image by a Cartesian product (case of empty intersection with the + domain). (Contributed by Thierry Arnoux, 16-Dec-2017.) $) xpima1 $p |- ( ( A i^i C ) = (/) -> ( ( A X. B ) " C ) = (/) ) $= ( cin c0 wceq cxp cima cif xpima iftrue syl5eq ) ACDEFZABGCHMEBIEABCJMEBKL $. - $( The image by a Cartesian product. (Contributed by Thierry Arnoux, - 16-Dec-2017.) $) + $( Direct image by a Cartesian product (case of nonempty intersection with + the domain). (Contributed by Thierry Arnoux, 16-Dec-2017.) $) xpima2 $p |- ( ( A i^i C ) =/= (/) -> ( ( A X. B ) " C ) = B ) $= ( cin c0 wne cxp cima wceq cif xpima ifnefalse syl5eq ) ACDZEFABGCHNEIEBJBA BCKNEEBLM $. - $( The image of a singleton by a Cartesian product. (Contributed by Thierry - Arnoux, 14-Jan-2018.) (Proof shortened by BJ, 6-Apr-2019.) $) + $( Direct image of a singleton by a Cartesian product. (Contributed by + Thierry Arnoux, 14-Jan-2018.) (Proof shortened by BJ, 6-Apr-2019.) $) xpimasn $p |- ( X e. A -> ( ( A X. B ) " { X } ) = B ) $= ( wcel csn cin c0 wne cxp cima wceq disjsn necon3abii notnotb bitr4i xpima2 wn sylbir ) CADZACEZFZGHZABITJBKUBSQZQSUCUAGACLMSNOABTPR $. @@ -55296,6 +55312,14 @@ the restriction (of the relation) to the singleton containing this cnvcnvss $p |- `' `' A C_ A $= ( ccnv cvv cxp cin cnvcnv inss1 eqsstri ) ABBACCDZEAAFAIGH $. + $( Two ways to express the corestriction of a class. (Contributed by BJ, + 28-Dec-2023.) $) + cnvrescnv $p |- `' ( `' R |` B ) = ( R i^i ( _V X. B ) ) $= + ( ccnv cres cvv cxp cin df-res cnveqi cnvin cnvcnv cnvxp ineq12i inass inxp + inv1 eqcomi ssv ssid 3eqtri ssini inss2 eqssi xpeq12i eqtr4i ineq2i ) BCZAD + ZCUGAEFZGZCUGCZUICZGZBEAFZGZUHUJUGAHIUGUIJUMBEEFZGZUNGBUPUNGZGUOUKUQULUNBKA + ELMBUPUNNURUNBUREEGZEAGZFUNEEEAOEUSAUTUSEEPQAUTAEAARASUAEAUBUCUDUEUFTT $. + $( Equality theorem for converse. (Contributed by FL, 19-Sep-2011.) $) cnveqb $p |- ( ( Rel A /\ Rel B ) -> ( A = B <-> `' A = `' B ) ) $= ( wrel wa wceq ccnv cnveq wi dfrel2 eqeq2 syl5ibr eqcoms sylbi eqeq1 imbi2d @@ -56144,8 +56168,8 @@ singleton of the first member (with no sethood assumptions on ` B ` ). $( The predecessors symbol. $) cpred $a class Pred ( R , A , X ) $. - $( Define the predecessor class of a relationship. This is the class of all - elements ` y ` of ` A ` such that ` y R X ` (see ~ elpred ) . + $( Define the predecessor class of a binary relation. This is the class of + all elements ` y ` of ` A ` such that ` y R X ` (see ~ elpred ) . (Contributed by Scott Fenton, 29-Jan-2011.) $) df-pred $a |- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) ) $. @@ -56362,7 +56386,7 @@ singleton of the first member (with no sethood assumptions on ` B ` ). ${ $d X y $. $d B y $. - $( The predecessor under the epsilon relationship is equivalent to an + $( The predecessor under the membership relation is equivalent to an intersection. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) $) predep $p |- ( X e. B -> Pred ( _E , A , X ) = ( A i^i X ) ) $= @@ -56377,8 +56401,7 @@ singleton of the first member (with no sethood assumptions on ` B ` ). $( A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011.) $) preddowncl $p |- ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) -> - ( X e. B -> - Pred ( R , B , X ) = Pred ( R , A , X ) ) ) $= + ( X e. B -> Pred ( R , B , X ) = Pred ( R , A , X ) ) ) $= ( vy vz wss cv cpred wral wa wcel wceq eleq1 predeq3 eqeq12d imbi2d vex wi imbi12d predpredss ad2antrr wbr weq sseq1d rspccva sseld elpredim jca2 wb elpred adantl mpbird ssrdv adantll eqssd ex vtoclg pm2.43b ) CBHZBDAIZ @@ -56389,15 +56412,15 @@ singleton of the first member (with no sethood assumptions on ` B ` ). TGSULRUMUNUOUPUQURUSUT $. $} - $( Given a partial ordering, ` X ` is not a member of its predecessor class. - (Contributed by Scott Fenton, 17-Apr-2011.) $) + $( Given a partial ordering, a class is not a member of its predecessor + class. (Contributed by Scott Fenton, 17-Apr-2011.) $) predpoirr $p |- ( R Po A -> -. X e. Pred ( R , A , X ) ) $= ( wpo wcel cpred wn wa wbr poirr elpredg anidms notbid syl5ibr expd pm2.43b wb predel con3i pm2.61d1 ) ABDZCAEZCABCFEZGZUAUBUDUBUAUBUDUAUBHUDUBCCBIZGAC BJUBUCUEUBUCUEQAABCCKLMNOPUCUBABCCRST $. - $( Given a well-founded relationship, ` X ` is not a member of its - predecessor class. (Contributed by Scott Fenton, 22-Apr-2011.) $) + $( Given a well-founded relation, a class is not a member of its predecessor + class. (Contributed by Scott Fenton, 22-Apr-2011.) $) predfrirr $p |- ( R Fr A -> -. X e. Pred ( R , A , X ) ) $= ( wfr wcel cpred wn wa wbr frirr elpredg anidms notbid syl5ibr expd pm2.43b wb predel con3i pm2.61d1 ) ABDZCAEZCABCFEZGZUAUBUDUBUAUBUDUAUBHUDUBCCBIZGAC @@ -56417,10 +56440,10 @@ singleton of the first member (with no sethood assumptions on ` B ` ). ${ $d x y A $. $d x y B $. $d x y R $. - $( All nonempty (possibly proper) subclasses of ` A ` , which has a - well-founded relation ` R ` , have ` R `-minimal elements. Proposition - 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, - 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) $) + $( All nonempty subclasses of a class having a well-ordered set-like + relation have minimal elements for that relation. Proposition 6.26 of + [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) + (Revised by Mario Carneiro, 26-Jun-2015.) $) tz6.26 $p |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) ) $= ( vx wwe wse wa wss c0 wne cv wbr wn wral wrex cpred wceq wreu wereu2 syl @@ -56434,10 +56457,10 @@ singleton of the first member (with no sethood assumptions on ` B ` ). $d A y $. $d B y $. $d R y $. tz6.26i.1 $e |- R We A $. tz6.26i.2 $e |- R Se A $. - $( All nonempty (possibly proper) subclasses of ` A ` , which has a - well-founded relation ` R ` , have ` R `-minimal elements. Proposition - 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, - 14-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) $) + $( All nonempty subclasses of a class having a well-founded set-like + relation ` R ` have ` R `-minimal elements. Proposition 6.26 of + [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 14-Apr-2011.) + (Revised by Mario Carneiro, 26-Jun-2015.) $) tz6.26i $p |- ( ( B C_ A /\ B =/= (/) ) -> E. y e. B Pred ( R , B , y ) = (/) ) $= ( wwe wse wss c0 wne wa cv cpred wceq wrex tz6.26 mpanl12 ) BDGBDHCBICJKL @@ -56607,7 +56630,7 @@ singleton of the first member (with no sethood assumptions on ` B ` ). csuc $a class suc A $. $( Define the ordinal predicate, which is true for a class that is transitive - and is well-ordered by the epsilon relation. Variant of definition of + and is well-ordered by the membership relation. Variant of definition of [BellMachover] p. 468. (Contributed by NM, 17-Sep-1993.) $) df-ord $a |- ( Ord A <-> ( Tr A /\ _E We A ) ) $. @@ -56678,7 +56701,7 @@ with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] id 3bitr4g ) ABCZADZAEFZAAGZCZHBDZBEFZBBGZCZHAIBIRSUCTUDUBUFABJABEKRABUAUER PABLMNAOBOQ $. - $( Epsilon well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] + $( Membership well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.) $) ordwe $p |- ( Ord A -> _E We A ) $= ( word wtr cep wwe df-ord simprbi ) ABACADEAFG $. @@ -56687,8 +56710,8 @@ with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] ordtr $p |- ( Ord A -> Tr A ) $= ( word wtr cep wwe df-ord simplbi ) ABACADEAFG $. - $( Epsilon is well-founded on an ordinal class. (Contributed by NM, - 22-Apr-1994.) $) + $( Membership is well-founded on an ordinal class. In other words, an + ordinal class is well-founded. (Contributed by NM, 22-Apr-1994.) $) ordfr $p |- ( Ord A -> _E Fr A ) $= ( word cep wwe wfr ordwe wefr syl ) ABACDACEAFACGH $. @@ -56703,10 +56726,10 @@ with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] ( wtr wss word w3a cep wwe wa wess ordwe impel anim2i 3impb df-ord sylibr ) ACZABDZBEZFQAGHZIZAEQRSUARSITQRBGHTSABGJBKLMNAOP $. - $( Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. - Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. We prove - this without invoking the Axiom of Regularity. (Contributed by NM, - 2-Jan-1994.) $) + $( No ordinal class is a member of itself. In other words, the membership + relation is irreflexive on ordinal classes. Theorem 2.2(i) of + [BellMachover] p. 469, generalized to classes. We prove this without + invoking the Axiom of Regularity. (Contributed by NM, 2-Jan-1994.) $) ordirr $p |- ( Ord A -> -. A e. A ) $= ( word cep wfr wcel wn ordfr efrirr syl ) ABACDAAEFAGAHI $. $( $j usage 'ordirr' avoids 'ax-reg'; $) @@ -56890,9 +56913,10 @@ with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] ${ $d x y z $. - $( The ordinal class is well-founded. This lemma is needed for ~ ordon in - order to eliminate the need for the Axiom of Regularity. (Contributed - by NM, 17-May-1994.) $) + $( The ordinal class is well-founded. This proof does not require the + axiom of regularity. This lemma is used in ~ ordon (through ~ epweon ) + in order to eliminate the need for the axiom of regularity. + (Contributed by NM, 17-May-1994.) $) onfr $p |- _E Fr On $= ( vx vz vy con0 cep wfr cv wss c0 wne cin wceq wrex dfepfr wel wex eqeq1d wa wi wcel n0 ineq2 rspcev adantll inss1 word ssel2 eloni ordfr inss2 vex @@ -70297,8 +70321,8 @@ associative structure (such as a group). (Contributed by NM, IWJWKVRVSWIWJWKWAWB $. $} - $( A set well-founded by epsilon contains no 3-cycle loops. (Contributed by - NM, 19-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) $) + $( A well-founded class contains no 3-cycle loops. (Contributed by NM, + 19-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) $) epne3 $p |- ( ( _E Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B e. C /\ C e. D /\ D e. B ) ) $= ( cep wfr wcel w3a wa wbr fr3nr wb epelg 3ad2ant2 3ad2ant3 3anbi123d adantl @@ -70336,14 +70360,15 @@ associative structure (such as a group). (Contributed by NM, ${ $d x y $. - $( The membership relation well-orders the class of ordinal numbers. - Proposition 4.8(g) of [Mendelson] p. 244. (Contributed by NM, - 1-Nov-2003.) $) + $( The membership relation well-orders the class of ordinal numbers. This + proof does not require the axiom of regularity. Proposition 4.8(g) of + [Mendelson] p. 244. (Contributed by NM, 1-Nov-2003.) $) epweon $p |- _E We On $= ( vx vy con0 cep wwe wfr cv wbr weq w3o wral onfr wcel eloni wa ordtri3or word wel epel biid 3orbi123i sylibr syl2an rgen2a dfwe2 mpbir2an ) CDECDF AGZBGZDHZABIZUHUGDHZJZBCKACKLULABCUGCMUGQZUHQZULUHCMUGNUHNUMUNOABRZUJBARZ JULUGUHPUIUOUJUJUKUPBUGSUJTAUHSUAUBUCUDABCDUEUF $. + $( $j usage 'epweon' avoids 'ax-reg'; $) $} $( The class of all ordinal numbers is ordinal. Proposition 7.12 of @@ -70416,8 +70441,8 @@ be a set (so instead it is a proper class). Here we prove the denial of onss $p |- ( A e. On -> A C_ On ) $= ( con0 wcel word wss eloni ordsson syl ) ABCADABEAFAGH $. - $( For an ordinal, the predecessor under ` _E ` and ` On ` is an identity - relationship. (Contributed by Scott Fenton, 27-Mar-2011.) $) + $( The predecessor of an ordinal under ` _E ` and ` On ` is itself. + (Contributed by Scott Fenton, 27-Mar-2011.) $) predon $p |- ( A e. On -> Pred ( _E , On , A ) = A ) $= ( con0 wcel cep cpred cin predep wss wceq onss sseqin2 sylib eqtrd ) ABCZBD AEBAFZABBAGNABHOAIAJABKLM $. @@ -81756,9 +81781,10 @@ general ordinal versions of these theorems (in this case ~ oa0r ) so ${ $d y A $. ecid.1 $e |- A e. _V $. - $( A set is equal to its converse epsilon coset. (Note: converse epsilon - is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) - (Revised by Mario Carneiro, 9-Jul-2014.) $) + $( A set is equal to its coset under the converse membership relation. + (Note: the converse membership relation is not an equivalence relation.) + (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, + 9-Jul-2014.) $) ecid $p |- [ A ] `' _E = A $= ( vy cep ccnv cec cv wcel wbr vex elec brcnv epeli 3bitri eqriv ) CADEZFZ ACGZQHARPIRADIRAHRAPCJZBKARDBSLRABMNO $. @@ -81766,9 +81792,10 @@ general ordinal versions of these theorems (in this case ~ oa0r ) so ${ $d x y A $. - $( A set is equal to its quotient set mod converse epsilon. (Note: - converse epsilon is not an equivalence relation.) (Contributed by NM, - 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) $) + $( A set is equal to its quotient set modulo the converse membership + relation. (Note: the converse membership relation is not an equivalence + relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario + Carneiro, 9-Jul-2014.) $) qsid $p |- ( A /. `' _E ) = A $= ( vy vx cep ccnv cqs cv cec wceq wrex wcel vex eqeq2i equcom bitri rexbii ecid elqs risset 3bitr4i eqriv ) BADEZFZABGZCGZUBHZIZCAJUEUDIZCAJUDUCKUDA @@ -95654,8 +95681,8 @@ proves the equinumerosity relationship for this definition (compare differs from Hilbert's transfinite axiom described on that page in that it requires ` R We A ` as an antecedent. Class ` A ` collects the sets of the least rank for which ` ph ( x ) ` is true. Class ` B ` , which - emulates the epsilon, is the minimum element in a well-ordering ` R ` on - ` A ` . + emulates Hilbert's epsilon, is the minimum element in a well-ordering + ` R ` on ` A ` . If a well-ordering ` R ` on ` A ` can be expressed in a closed form, as might be the case if we are working with say natural numbers, we can @@ -115063,7 +115090,7 @@ B C_ ( A +P. C ) ) $= $( Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ` CC ` from those in ` R. ` . The trick involves - ~ qsid , which shows that the coset of the converse epsilon relation + ~ qsid , which shows that the coset of the converse membership relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that ` CC ` is a quotient set, even though it is not (compare ~ df-c ), and allows us to reuse some @@ -115085,7 +115112,7 @@ B C_ ( A +P. C ) ) $= $( Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ~ ecid , which shows that the coset of - the converse epsilon relation (which is not an equivalence relation) + the converse membership relation (which is not an equivalence relation) leaves a set unchanged. See also ~ dfcnqs . _Note: This is the last lemma (from which the axioms will be derived) in_ @@ -512716,15 +512743,15 @@ Real and complex numbers (cont.) $d A x $. $d B x $. $d R x $. coep.1 $e |- A e. _V $. coep.2 $e |- B e. _V $. - $( Composition with epsilon. (Contributed by Scott Fenton, + $( Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) $) coep $p |- ( A ( _E o. R ) B <-> E. x e. B A R x ) $= ( cv wbr cep wex wcel ccom wrex epeli anbi1ci exbii brco df-rex 3bitr4i wa ) BAGZDHZUACIHZTZAJUACKZUBTZAJBCIDLHUBACMUDUFAUCUEUBUACFNOPABCIDEFQUBA CRS $. - $( Composition with the converse of epsilon. (Contributed by Scott Fenton, - 18-Feb-2013.) $) + $( Composition with the converse membership relation. (Contributed by + Scott Fenton, 18-Feb-2013.) $) coepr $p |- ( A ( R o. `' _E ) B <-> E. x e. A x R B ) $= ( cv cep ccnv wbr wa wex wcel ccom wrex vex brcnv epeli bitri anbi1i brco exbii df-rex 3bitr4i ) BAGZHIZJZUECDJZKZALUEBMZUHKZALBCDUFNJUHABOUIUKAUGU @@ -513329,14 +513356,14 @@ Real and complex numbers (cont.) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - Epsilon induction + Set induction (or epsilon induction) =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= $) ${ $d ph y z $. $d x y z $. setinds.1 $e |- ( A. y e. x [. y / x ]. ph -> ph ) $. - $( Principle of ` _E ` induction (set induction). If a property passes + $( Principle of set induction (or ` _E ` -induction). If a property passes from all elements of ` x ` to ` x ` itself, then it holds for all ` x ` . (Contributed by Scott Fenton, 10-Mar-2011.) $) setinds $p |- ph $= @@ -513392,8 +513419,8 @@ Real and complex numbers (cont.) VQRUFAVNRUGVPWBVOCCECUHCVNRUIULUJQUMUNUO $. $} - $( Given ~ ax-reg , an ordinal is a transitive class totally ordered by - epsilon. (Contributed by Scott Fenton, 28-Jan-2011.) $) + $( Given ~ ax-reg , an ordinal is a transitive class totally ordered by the + membership relation. (Contributed by Scott Fenton, 28-Jan-2011.) $) dford5reg $p |- ( Ord A <-> ( Tr A /\ _E Or A ) ) $= ( word wtr cep wwe wa wor df-ord wfr zfregfr df-we mpbiran anbi2i bitri ) A BACZADEZFOADGZFAHPQOPADIQAJADKLMN $. @@ -513670,7 +513697,7 @@ Real and complex numbers (cont.) ${ $d x y $. - $( The domain of the epsilon relation is the universe. (Contributed by + $( The domain of the membership relation is the universe. (Contributed by Scott Fenton, 27-Oct-2010.) $) domep $p |- dom _E = _V $= ( vx vy weq cab cv cep wbr wex cvv cdm equid wel el exbii mpbir 2th abbii @@ -634538,10 +634565,10 @@ group element in (1,2), contradicting ~ pell14qrgapw . (Contributed by ${ $d x y A $. $d x y B $. - $( Epsilon induction for sets contained in a transitive set. If we are - allowed to assume Infinity, then all sets have a transitive closure and - this reduces to ~ setind ; however, this version is useful without - Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.) $) + $( Set induction for sets contained in a transitive set. If we are allowed + to assume Infinity, then all sets have a transitive closure and this + reduces to ~ setind ; however, this version is useful without Infinity. + (Contributed by Stefan O'Rear, 28-Oct-2014.) $) setindtr $p |- ( A. x ( x C_ A -> x e. A ) -> ( E. y ( Tr y /\ B e. y ) -> B e. A ) ) $= ( cv wtr wcel wa wex wss wi wal c0 wceq cin wn sylib adantlr ex cvv impel @@ -634561,7 +634588,7 @@ group element in (1,2), contradicting ~ pell14qrgapw . (Contributed by setindtrs.a $e |- ( A. y e. x ps -> ph ) $. setindtrs.b $e |- ( x = y -> ( ph <-> ps ) ) $. setindtrs.c $e |- ( x = B -> ( ph <-> ch ) ) $. - $( Epsilon induction scheme without Infinity. See comments at ~ setindtr . + $( Set induction scheme without Infinity. See comments at ~ setindtr . (Contributed by Stefan O'Rear, 28-Oct-2014.) $) setindtrs $p |- ( E. z ( Tr z /\ B e. z ) -> ch ) $= ( va cv wtr wcel wa wex wi wral nfsab1 cvv setindtr dfss3 nfcv nfral nfim @@ -655785,7 +655812,7 @@ Deduction Proof (not shown) was minimized. The minimized proof is ${ $d a x y $. - $( The epsilon relation is foundational on the class of ordinal numbers. + $( The membership relation is foundational on the class of ordinal numbers. ~ onfrALT is an alternate proof of ~ onfr . ~ onfrALTVD is the Virtual Deduction proof from which ~ onfrALT is derived. The Virtual Deduction proof mirrors the working proof of ~ onfr which is the main part of the @@ -687902,7 +687929,7 @@ used to represent the final q_n in the paper (the one with n large $( This lemma proves that there exists a function ` x ` as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: x_j is in the subalgebra, 0 <= x_j <= 1, x_j < ε / n on A_j (meaning A in the paper), x_j > 1 - - \epslon / n on B_j. Here ` D ` is used to represent A in the paper + \epsilon / n on B_j. Here ` D ` is used to represent A in the paper (because A is used for the subalgebra of functions), ` E ` is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) $) @@ -725807,7 +725834,7 @@ Negated membership (alternative) $) $( Declare new connectives. $) - $c e// $. $( Not an element of (epsilon with slash through it). $) + $c e// $. $( Not an element of (stylized epsilon with slash through it). $) $( Extend wff notation to include the 'not elemet of' relation. $) cnelbr $a class e// $. @@ -725815,7 +725842,7 @@ Negated membership (alternative) ${ $d x y $. $( Define negated membership as binary relation. Analogous to ~ df-eprel - (the epsilon relation). (Contributed by AV, 26-Dec-2021.) $) + (the membership relation). (Contributed by AV, 26-Dec-2021.) $) df-nelbr $a |- e// = { <. x , y >. | -. x e. y } $. $( Alternate definition of the negated membership as binary relation.