From df1dfb8d62c79b1f4b32b5d43b9732aaf814efaa Mon Sep 17 00:00:00 2001 From: mazsa Date: Thu, 21 Nov 2024 15:46:42 +0100 Subject: [PATCH] MembEr --- set.mm | 76 ++++++++++++++++++++++++++++------------------------------ 1 file changed, 37 insertions(+), 39 deletions(-) diff --git a/set.mm b/set.mm index 8d735420ea..4280925d5b 100644 --- a/set.mm +++ b/set.mm @@ -437187,12 +437187,12 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the htmldef "ErALTV" as ' ErALTV '; althtmldef "ErALTV" as ' ErALTV '; latexdef "ErALTV" as "\mathrm{ErALTV}"; -htmldef "MembErs" as ' MembErs '; - althtmldef "MembErs" as ' MembErs '; - latexdef "MembErs" as "\mathrm{MembErs}"; -htmldef "MembEr" as ' MembEr '; - althtmldef "MembEr" as ' MembEr '; - latexdef "MembEr" as "\mathrm{MembEr}"; +htmldef "CoMembErs" as ' CoMembErs '; + althtmldef "CoMembErs" as ' CoMembErs '; + latexdef "CoMembErs" as "\mathrm{CoMembErs}"; +htmldef "CoMembEr" as ' CoMembEr '; + althtmldef "CoMembEr" as ' CoMembEr '; + latexdef "CoMembEr" as "\mathrm{CoMembEr}"; htmldef "Funss" as ' Funss '; althtmldef "Funss" as ' Funss '; latexdef "Funss" as "\mathrm{Funss}"; @@ -550171,8 +550171,8 @@ A collection of theorems for commuting equalities (or quotients $) $c ErALTV $. $( Equivalence relation on its domain quotient predicate $) - $c MembErs $. $( The class of membership equivalence relations $) - $c MembEr $. $( Membership equivalence relation predicate $) + $c CoMembErs $. $( The class of membership equivalence relations $) + $c CoMembEr $. $( Membership equivalence relation predicate $) $c Funss $. $( The class of all function sets (used only once) $) $c FunsALTV $. $( The class of functions, i.e., function relations $) @@ -550354,12 +550354,12 @@ A collection of theorems for commuting equalities (or $( Extend the definition of a class to include the membership equivalence relations class. $) - cmembers $a class MembErs $. + cmembers $a class CoMembErs $. $( Extend the definition of a wff to include the membership equivalence relation predicate. (Read: the membership equivalence relation on ` A ` , or, the restricted elementhood equivalence relation on its domain quotient ` A ` .) $) - wmember $a wff MembEr A $. + wcomember $a wff CoMembEr A $. $( Extend the definition of a class to include the function set class. $) cfunss $a class Funss $. @@ -553304,25 +553304,23 @@ relation with an intersection with the same Cartesian product (see also references in it; if you do not need them, use ~ moantrALT instead, since it does not rely on the concept of unique existence ( ~ df-eu ). (Contributed by Peter Mazsa, 2-Oct-2018.) (Revised by Peter Mazsa, - 19-Nov-2024.) (Proof modification is discouraged.) $) + 20-Nov-2024.) (Proof modification is discouraged.) $) moantr $p |- ( E* x ps -> ( ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) -> E. x ( ph /\ ch ) ) ) $= - ( wmo wa wex nfmo1 nfe1 mopickr ancrd anim1d df-3an 3simpb sylbir - nfan w3a syl6 eximd expimpd ) BDEZABFZDGZBCFZDGACFZDGUAUCFZUDUEDU - AUCDBDHUBDIPUFUDUBCFZUEUFBUBCUFBAABDJKLUGABCQUEABCMABCNORST $. + ( wmo wa wex nfmo1 nfe1 nfan mopickr anim1d eximd expimpd ) BDEZA + BFZDGZBCFZDGACFZDGOQFZRSDOQDBDHPDIJTBACABDKLMN $. $( Sufficient condition for transitivity of conjunctions inside existential quantifiers. This proof does not rely on the concept of unique existence ( ~ df-eu ). (Contributed by Peter Mazsa, 2-Oct-2018.) (Shortened by - Peter Mazsa, 19-Nov-2024.) $) + Peter Mazsa, 20-Nov-2024.) $) moantrALT $p |- ( E* x ps -> ( ( E. x ( ph /\ ps ) /\ E. x ( ps /\ ch ) ) -> E. x ( ph /\ ch ) ) ) $= - ( wmo wa wex nfmo1 nfe1 nfan exancom mopick sylan2br ancrd anim1d - wi w3a df-3an 3simpb sylbir syl6 eximd expimpd ) BDEZABFZDGZBCFZD - GACFZDGUDUFFZUGUHDUDUFDBDHUEDIJUIUGUECFZUHUIBUECUIBAUFUDBAFDGBAPB - ADKBADLMNOUJABCQUHABCRABCSTUAUBUC $. + ( wmo wa wex nfmo1 nfe1 nfan exancom mopick sylan2br anim1d eximd + wi expimpd ) BDEZABFZDGZBCFZDGACFZDGRTFZUAUBDRTDBDHSDIJUCBACTRBAF + DGBAPBADKBADLMNOQ $. ${ $d A a $. @@ -559535,18 +559533,18 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation. $( Define the class of membership equivalence relations on their domain quotients. (Contributed by Peter Mazsa, 28-Nov-2022.) (Revised by Peter Mazsa, 24-Jul-2023.) $) - df-members $a |- MembErs = { a | ,~ ( `' _E |` a ) Ers a } $. + df-comembers $a |- CoMembErs = { a | ,~ ( `' _E |` a ) Ers a } $. $( Define the membership equivalence relation on the class ` A ` (or, the restricted elementhood equivalence relation on its domain quotient - ` A ` .) Alternate definitions are ~ dfmember2 and ~ dfmember3 . + ` A ` .) Alternate definitions are ~ dfcomember2 and ~ dfcomember3 . Later on, in an application of set theory I make a distinction between the default elementhood concept and a special membership concept: membership equivalence relation will be an integral part of that membership concept. (Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa, 28-Nov-2022.) $) - df-member $a |- ( MembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) $. + df-comember $a |- ( CoMembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) $. $( Binary equivalence relation with natural domain, see the comment of ~ df-ers . (Contributed by Peter Mazsa, 23-Jul-2021.) $) @@ -559585,20 +559583,20 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation. $( Alternate definition of the membership equivalence relation. (Contributed by Peter Mazsa, 28-Nov-2022.) $) - dfmember $p |- ( MembEr A <-> ~ A ErALTV A ) $= - ( wmember cep ccnv cres werALTV ccoels df-member df-coels erALTVeq1i bitr4i + dfcomember $p |- ( CoMembEr A <-> ~ A ErALTV A ) $= + ( wcomember cep ccnv cres werALTV ccoels df-comember df-coels erALTVeq1i bitr4i ccoss ) ABACDAELZFAAGZFAHANMAIJK $. $( Alternate definition of the membership equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021.) $) - dfmember2 $p |- ( MembEr A <-> ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) ) $= - ( wmember ccoels werALTV weqvrel cdm cqs wceq wa dfmember dferALTV2 bitri ) + dfcomember2 $p |- ( CoMembEr A <-> ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) ) $= + ( wcomember ccoels werALTV weqvrel cdm cqs wceq wa dfcomember dferALTV2 bitri ) ABAACZDMEMFMGAHIAJAMKL $. $( Alternate definition of the membership equivalence relation. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, 17-Jul-2023.) $) - dfmember3 $p |- ( MembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) $= - ( wmember ccoels weqvrel cdm cqs wceq wa wcoeleqvrel dfmember2 dfcoeleqvrel + dfcomember3 $p |- ( CoMembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) $= + ( wcomember ccoels weqvrel cdm cqs wceq wa wcoeleqvrel dfcomember2 dfcoeleqvrel cuni bicomi dmqscoelseq anbi12i bitri ) ABACZDZQEQFAGZHAIZALQFAGZHAJRTSUATR AKMANOP $. @@ -561288,10 +561286,10 @@ implies disjointness (e.g. ~ eqvrelqseqdisj5 ), or converse function $( The Main Theorem of Equivalences: any equivalence relation implies equivalent membership as well. (Contributed by Peter Mazsa, 26-Sep-2021.) $) - mainer $p |- ( R ErALTV A -> MembEr A ) $= - ( weqvrel cdm cqs wceq wa wcoeleqvrel cuni ccoels werALTV wmember + mainer $p |- ( R ErALTV A -> CoMembEr A ) $= + ( weqvrel cdm cqs wceq wa wcoeleqvrel cuni ccoels werALTV wcomember weldisj eqvrelqseqdisj2 mdisjim syl c0 wcel wn n0eldmqseq 3imtr4i - adantl wb eldisjn0el mpbid jca dferALTV2 dfmember3 ) BCZBDZBEAFZG + adantl wb eldisjn0el mpbid jca dferALTV2 dfcomember3 ) BCZBDZBEAFZG ZAHZAIAJEAFZGABKALULUMUNULAMZUMAUJBNZAOPULQARSZUNUKUQUIABTUBULUOU QUNUCUPAUDPUEUFABUGAUHUA $. @@ -561312,9 +561310,9 @@ membership equivalence relation and membership partition are the same (or: membership partition). Together with ~ mpet2 and ~ mpet3 , this is what is generally identified as the partition-equivalence theorem (but cf. ~ pet with general ` R ` ). (Contributed by Peter Mazsa, 24-Sep-2021.) $) - mpet $p |- ( MembPart A <-> MembEr A ) $= - ( weldisj c0 wcel wn wa wcoeleqvrel cuni ccoels wmembpart wmember - cqs wceq mpet3 dfmembpart2 dfmember3 3bitr4i ) ABCADEFAGAHAILAMFA + mpet $p |- ( MembPart A <-> CoMembEr A ) $= + ( weldisj c0 wcel wn wa wcoeleqvrel cuni ccoels wmembpart wcomember + cqs wceq mpet3 dfmembpart2 dfcomember3 3bitr4i ) ABCADEFAGAHAILAMFA JAKANAOAPQ $. $( Membership Partition-Equivalence Theorem in a shorter form. Together with @@ -561322,7 +561320,7 @@ membership equivalence relation and membership partition are the same (or: partition-equivalence theorem (but cf. ~ pet with general ` R ` ). (Contributed by Peter Mazsa, 24-Sep-2021.) $) mpet2 $p |- ( ( `' _E |` A ) Part A <-> ,~ ( `' _E |` A ) ErALTV A ) $= - ( wmembpart wmember cep ccnv cres wpart ccoss werALTV df-membpart df-member + ( wmembpart wcomember cep ccnv cres wpart ccoss werALTV df-membpart df-comember mpet 3bitr3i ) ABACADEAFZGANHIALAJAKM $. $( Membership Partition-Equivalence Theorem with binary relations, cf. @@ -561339,7 +561337,7 @@ membership equivalence relation and membership partition are the same (or: ~ mpet ) generate partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.) $) fences $p |- ( R ErALTV A -> MembPart A ) $= - ( werALTV wmember wmembpart mainer mpet sylibr ) ABCADAEABFAGH $. + ( werALTV wcomember wmembpart mainer mpet sylibr ) ABCADAEABFAGH $. $( The Theorem of Fences by Equivalences: all kinds of equivalence relations imaginable (in addition to the membership equivalence relation cf. @@ -561421,14 +561419,14 @@ This theorem (together with ~ pets and ~ pet2 ) is the main result of my $( Some kinds of partition with general ` R ` (in addition to the membership partition cf. ~ mpet and ~ mpet2 ) imply equivalence of members. (Contributed by Peter Mazsa, 23-Sep-2021.) $) - partimmember $p |- ( ( R |X. ( `' _E |` A ) ) Part A -> MembEr A ) $= - ( cep ccnv cres cxrn wpart ccoss werALTV wmember pet mainer sylbi ) ABCDAEF + partimmember $p |- ( ( R |X. ( `' _E |` A ) ) Part A -> CoMembEr A ) $= + ( cep ccnv cres cxrn wpart ccoss werALTV wcomember pet mainer sylbi ) ABCDAEF ZGANHZIAJABKAOLM $. $( Some kinds of partition with general ` R ` imply membership partition as well. (Contributed by Peter Mazsa, 23-Sep-2021.) $) partimmembpart $p |- ( ( R |X. ( `' _E |` A ) ) Part A -> MembPart A ) $= - ( cep ccnv cres cxrn wpart wmember wmembpart partimmember mpet sylibr ) ABC + ( cep ccnv cres cxrn wpart wcomember wmembpart partimmember mpet sylibr ) ABC DAEFGAHAIABJAKL $. $( Partition-Equivalence Theorem with general ` R ` , with binary relations.