Skip to content

Commit

Permalink
MembEr
Browse files Browse the repository at this point in the history
  • Loading branch information
@mazsa
mazsa committed Nov 21, 2024
1 parent 6b7ef88 commit df1dfb8
Showing 1 changed file with 37 additions and 39 deletions.
76 changes: 37 additions & 39 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}";
Expand Down Expand Up @@ -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 $)
Expand Down Expand Up @@ -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 $.
Expand Down Expand Up @@ -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 $.
Expand Down Expand Up @@ -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.) $)
Expand Down Expand Up @@ -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 $.

Expand Down Expand Up @@ -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 $.

Expand All @@ -561312,17 +561310,17 @@ 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
~ mpet 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.) $)
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.
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand Down

0 comments on commit df1dfb8

Please sign in to comment.