diff --git a/discouraged b/discouraged index 0557785111..63f7947fdc 100644 --- a/discouraged +++ b/discouraged @@ -20899,6 +20899,7 @@ Proof modification of "mnringvscadOLD" is discouraged (30 steps). Proof modification of "mobidvALT" is discouraged (48 steps). Proof modification of "moelOLD" is discouraged (101 steps). Proof modification of "mof0ALT" is discouraged (67 steps). +Proof modification of "mopickr" is discouraged (77 steps). Proof modification of "mpjao3danOLD" is discouraged (29 steps). Proof modification of "mpofunOLD" is discouraged (95 steps). Proof modification of "mpteq12daOLD" is discouraged (41 steps). diff --git a/set.mm b/set.mm index cd69cba5e6..3014a9f69e 100644 --- a/set.mm +++ b/set.mm @@ -450807,12 +450807,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}"; @@ -450837,6 +450837,21 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the htmldef "ElDisj" as ' ElDisj '; althtmldef "ElDisj" as ' ElDisj '; latexdef "ElDisj" as "\mathrm{ElDisj}"; +htmldef "AntisymRel" as ' AntisymRel '; + althtmldef "AntisymRel" as ' AntisymRel '; + latexdef "AntisymRel" as "\mathrm{AntisymRel}"; +htmldef "Parts" as ' Parts '; + althtmldef "Parts" as ' Parts '; + latexdef "Parts" as "{\rm Parts}"; +htmldef "Part" as ' Part '; + althtmldef "Part" as ' Part '; + latexdef "Part" as "{\rm Part}"; +htmldef "MembParts" as ' MembParts '; + althtmldef "MembParts" as ' MembParts '; + latexdef "MembParts" as "{\rm MembParts}"; +htmldef "MembPart" as ' MembPart '; + althtmldef "MembPart" as ' MembPart '; + latexdef "MembPart" as "{\rm MembPart}"; /* End of Peter Mazsa's mathbox */ /* Mathbox of Rodolfo Medina */ @@ -580782,8 +580797,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 comember equivalence relations $) + $c CoMembEr $. $( Comember equivalence relation predicate $) $c Funss $. $( The class of all function sets (used only once) $) $c FunsALTV $. $( The class of functions, i.e., function relations $) @@ -580797,6 +580812,14 @@ A collection of theorems for commuting equalities (or relation $) $c ElDisj $. $( Disjoint elementhood predicate $) + $c AntisymRel $. $( Antisymmetric relation predicate $) + + $c Parts $. $( The class of all partitions, i.e., partition relations $) + $c Part $. $( Partition predicate $) + + $c MembParts $. $( The class of member partition relations $) + $c MembPart $. $( Member partition predicate $) + $( Extend the definition of a class to include the range Cartesian product class. $) cxrn $a class ( A |X. B ) $. @@ -580890,14 +580913,14 @@ A collection of theorems for commuting equalities (or domain quotient ` A ` .) $) werALTV $a wff R ErALTV A $. - $( Extend the definition of a class to include the membership equivalence + $( Extend the definition of a class to include the comember equivalence relations class. $) - cmembers $a class MembErs $. - $( 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 + ccomembers $a class CoMembErs $. + $( Extend the definition of a wff to include the comember equivalence + relation predicate. (Read: the comember equivalence relation on ` A ` , + or, the restricted coelement 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 $. @@ -580918,13 +580941,33 @@ A collection of theorems for commuting equalities (or wdisjALTV $a wff Disj R $. $( Extend the definition of a class to include the disjoint elements class, - i.e., the disjoint elementhood relations class. $) + i.e., the disjoint element relations class. $) celdisjs $a class ElDisjs $. - $( Extend the definition of a wff to include the disjoint elementhood - predicate, i.e., the disjoint elementhood relation predicate. (Read: the - elements of ` A ` are disjoint.) $) + $( Extend the definition of a wff to include the disjoint element predicate, + i.e., the disjoint element relation predicate. (Read: the elements of + ` A ` are disjoint.) $) weldisj $a wff ElDisj A $. + $( Extend the definition of a wff to include the antisymmetry relation + predicate. (Read: ` R ` is an antisymmetric relation.) $) + wantisymrel $a wff AntisymRel R $. + + $( Extend the definition of a class to include the partitions class, i.e., + the partition relations class. $) + cparts $a class Parts $. + $( Extend the definition of a wff to include the partition predicate, i.e., + the partition relation predicate. (Read: ` A ` is a partition by + ` R ` .) $) + wpart $a wff R Part A $. + + $( Extend the definition of a class to include the member partitions class, + i.e., the member partition relations class. $) + cmembparts $a class MembParts $. + $( Extend the definition of a wff to include the member partition predicate, + i.e., the member partition relation predicate. (Read: ` A ` is a member + partition.) $) + wmembpart $a wff MembPart A $. + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -581021,12 +581064,49 @@ A collection of theorems for commuting equalities (or ( wa w3a biantrur 3anass 3bitr4i ) BCFZAKFCABCGAKDHBCEHABCIJ $. $} - $( Substitution of equal classes into elementhood relation. (Contributed by + ${ + bianbi.1 $e |- ( ph <-> ( ps /\ ch ) ) $. + bianbi.2 $e |- ( ps <-> th ) $. + $( Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, + 31-Jul-2023.) $) + bianbi $p |- ( ph <-> ( th /\ ch ) ) $= + ( wa anbi1i bitri ) ABCGDCGEBDCFHI $. + $} + + ${ + bianim.1 $e |- ( ph <-> ( ps /\ ch ) ) $. + bianim.2 $e |- ( ch -> ( ps <-> th ) ) $. + $( Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, + 31-Jul-2023.) $) + bianim $p |- ( ph <-> ( th /\ ch ) ) $= + ( wa pm5.32ri bitri ) ABCGDCGECBDFHI $. + $} + + ${ + biorfd.1 $e |- ( ph -> -. ps ) $. + $( A wff is equivalent to its disjunction with falsehood, deduction form. + (Contributed by Peter Mazsa, 22-Aug-2023.) $) + biorfd $p |- ( ph -> ( ch <-> ( ps \/ ch ) ) ) $= + ( wn wo wb biorf syl ) ABECBCFGDBCHI $. + $} + + $( Substitution of equal classes in binary relation. (Contributed by Peter + Mazsa, 14-Jun-2024.) $) + eqbrtr $p |- ( ( A = B /\ B R C ) -> A R C ) $= + ( wceq wbr breq1 biimpar ) ABEACDFBCDFABCDGH $. + + $( Substitution of equal classes in a binary relation. (Contributed by Peter + Mazsa, 14-Jun-2024.) $) + eqbrb $p |- ( ( A = B /\ A R C ) <-> ( A = B /\ B R C ) ) $= + ( wceq wbr wa simpl eqbrtr jca eqcom anbi1i 3imtr3i impbii ) ABEZACDFZGZOBC + DFZGZBAEZPGZTRGQSUATRTPHBACDIJTOPBAKZLTORUBLMSOPORHABCDIJN $. + + $( Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 22-Jul-2017.) $) eqeltr $p |- ( ( A = B /\ B e. C ) -> A e. C ) $= ( wceq wcel eleq1 biimpar ) ABDACEBCEABCFG $. - $( Substitution of equal classes into elementhood relation. (Contributed by + $( Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 17-Jul-2019.) $) eqelb $p |- ( ( A = B /\ A e. C ) <-> ( A = B /\ B e. C ) ) $= ( wceq wcel wa simpl eqeltr jca eqcom anbi1i 3imtr3i impbii ) ABDZACEZFZNBC @@ -581040,6 +581120,76 @@ A collection of theorems for commuting equalities (or ( wceq wb eqeq12 sylan2 ) ABCGDEGBDGCEGHFBCDEIJ $. $} + $( One-to-one relationship between the successor operation and the singleton. + (Contributed by Peter Mazsa, 31-Dec-2024.) $) + suceqsneq $p |- ( A e. V -> ( suc A = suc B <-> { A } = { B } ) ) $= + ( wcel csuc wceq csn suc11reg sneqbg bitr4id ) ACDAEBEFABFAGBGFABHABCIJ $. + + $( A class is disjoint from its singleton. A consequence of regularity. + Shorter proof than ~ bnj521 and does not depend on ~ df-ne . (Temporary: + as soon as this Mathbox only PR is accepted, I'll open a PR to place this + to the main. PM) (Contributed by BJ, 4-Apr-2019.) $) + disjcsn $p |- ( A i^i { A } ) = (/) $= + ( csn cin c0 wceq wcel wn elirr disjsn mpbir ) AABCDEAAFGAHAAIJ $. + + $( An equality involving class union and class difference. (Temporary: as + soon as this Mathbox only PR is accepted, I'll open a PR to place this to + the main. PM) (Contributed by Thierry Arnoux, 26-Jun-2024.) $) + undif5TEMP $p |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A ) $= + ( cin c0 wceq cun cdif difun2 disjdif2 eqtrid ) ABCDEABFBGABGAABHABIJ $. + + $( Absorption of union with a singleton by difference. (Contributed by Peter + Mazsa, 24-Jul-2024.) $) + sucdifsn2 $p |- ( ( A u. { A } ) \ { A } ) = A $= + ( csn cin c0 wceq cun cdif disjcsn undif5TEMP ax-mp ) AABZCDEAKFKGAEAHAKIJ + $. + + $( The difference between the successor and the singleton of a class is the + class. (Contributed by Peter Mazsa, 20-Sep-2024.) $) + sucdifsn $p |- ( suc A \ { A } ) = A $= + ( csuc csn cdif cun df-suc difeq1i sucdifsn2 eqtri ) ABZACZDAKEZKDAJLKAFGAH + I $. + + $( The restriction to a disjoint is the empty class. (Contributed by Peter + Mazsa, 24-Jul-2024.) $) + disjresin $p |- ( ( A i^i B ) = (/) -> ( R |` ( A i^i B ) ) = (/) ) $= + ( cin c0 wceq cres reseq2 res0 eqtrdi ) ABDZEFCKGCEGEKECHCIJ $. + + $( The intersection of restrictions to disjoint is the empty class. + (Contributed by Peter Mazsa, 24-Jul-2024.) $) + disjresdisj $p |- ( ( A i^i B ) = (/) -> + ( ( R |` A ) i^i ( R |` B ) ) = (/) ) $= + ( cin c0 wceq cres resindi disjresin eqtr3id ) ABDZEFCAGCBGDCKGECABHABCIJ + $. + + $( The difference between restrictions to disjoint is the first restriction. + (Contributed by Peter Mazsa, 24-Jul-2024.) $) + disjresdif $p |- ( ( A i^i B ) = (/) -> + ( ( R |` A ) \ ( R |` B ) ) = ( R |` A ) ) $= + ( cin c0 wceq cres cdif disjresdisj disjdif2 syl ) ABDEFCAGZCBGZDEFLMHLFABC + ILMJK $. + + $( Lemma for ~ ressucdifsn2 . (Contributed by Peter Mazsa, 24-Jul-2024.) $) + disjresundif $p |- ( ( A i^i B ) = (/) -> + ( ( R |` ( A u. B ) ) \ ( R |` B ) ) = ( R |` A ) ) $= + ( cin c0 wceq cun cres cdif resundi difeq1i difun2 eqtri disjresdif eqtrid + ) ABDEFCABGHZCBHZIZCAHZQIZSRSQGZQITPUAQCABJKSQLMABCNO $. + + $( The difference between restrictions to the successor and the singleton of + a class is the restriction to the class, see ~ ressucdifsn . (Contributed + by Peter Mazsa, 24-Jul-2024.) $) + ressucdifsn2 $p |- ( ( R |` ( A u. { A } ) ) \ ( R |` { A } ) ) = + ( R |` A ) $= + ( csn cin c0 wceq cun cres cdif disjcsn disjresundif ax-mp ) AACZDEFBAMGHBM + HIBAHFAJAMBKL $. + + $( The difference between restrictions to the successor and the singleton of + a class is the restriction to the class. (Contributed by Peter Mazsa, + 20-Sep-2024.) $) + ressucdifsn $p |- ( ( R |` suc A ) \ ( R |` { A } ) ) = ( R |` A ) $= + ( csuc cres csn cdif cun df-suc reseq2i difeq1i ressucdifsn2 eqtri ) BACZDZ + BAEZDZFBAOGZDZPFBADNRPMQBAHIJABKL $. + $( Two ways of expressing the restriction of an intersection. (Contributed by Peter Mazsa, 5-Jun-2021.) $) inres2 $p |- ( ( R |` A ) i^i S ) = ( ( R i^i S ) |` A ) $= @@ -581056,6 +581206,23 @@ A collection of theorems for commuting equalities (or nexmo1 $p |- ( -. E. x ph -> E* x ph ) $= ( wex wn weu wi wmo pm2.21 moeu sylibr ) ABCZDKABEZFABGKLHABIJ $. + $( Restricted universal quantification over intersection. (Contributed by + Peter Mazsa, 8-Sep-2023.) $) + ralin $p |- ( A. x e. ( A i^i B ) ph <-> + A. x e. A ( x e. B -> ph ) ) $= + ( cv wcel wi cin wa elin imbi1i impexp bitri ralbii2 ) ABEZDFZAGZBCDHZCORFZ + AGOCFZPIZAGTQGSUAAOCDJKTPALMN $. + + ${ + $d A y $. $d x y $. + $( Double restricted universal quantification, special case. (Contributed + by Peter Mazsa, 17-Jun-2020.) $) + r2alan $p |- ( A. x A. y ( ( ( x e. A /\ y e. B ) /\ ph ) -> ps ) <-> + A. x e. A A. y e. B ( ph -> ps ) ) $= + ( cv wcel wa wi wal wral impexp 2albii r2al bitr4i ) CGEHDGFHIZAIBJZDKCKQ + ABJZJZDKCKSDFLCELRTCDQABMNSCDEFOP $. + $} + ${ 3ralbii.1 $e |- ( ph <-> ps ) $. $( Inference adding three restricted universal quantifiers to both sides of @@ -581139,6 +581306,13 @@ A collection of theorems for commuting equalities (or UIMLZUQUKURULUTUPUJCUNUOUHUIUFZUGUTUPUJDVAUGUAUBUC $. $} + $( Binary relation on the converse of an intersection with a Cartesian + product. (Contributed by Peter Mazsa, 27-Jul-2019.) $) + br1cnvinxp $p |- ( C `' ( R i^i ( A X. B ) ) D <-> + ( ( C e. B /\ D e. A ) /\ D R C ) ) $= + ( cxp cin ccnv wbr wcel wa relinxp relbrcnv brinxp2 ancom anbi1i 3bitri ) C + DEABFGZHIDCRIDAJZCBJZKZDCEIZKTSKZUBKCDRABELMABDCENUAUCUBSTOPQ $. + $( Elementhood in a converse ` R ` -coset when ` R ` is a relation. (Contributed by Peter Mazsa, 9-Dec-2018.) $) releleccnv $p |- ( Rel R -> ( A e. [ B ] `' R <-> A R B ) ) $= @@ -581231,6 +581405,14 @@ A collection of theorems for commuting equalities (or AUDJKHZUEUFUIABCDUDRLUFUEBCUCDAMNOUKUGUEIUHIUGUEUHPUJAUDBCDQUGUEUHSUGUEUHTU AUB $. + $( Binary relation on the converse of a restriction. (Contributed by Peter + Mazsa, 27-Jul-2019.) $) + br1cnvres $p |- ( B e. V -> + ( B `' ( R |` A ) C <-> ( C e. A /\ C R B ) ) ) $= + ( cres ccnv wbr cvv cxp cin wcel wa df-res cnveqi breqi wb br1cnvinxp anass + elex bitri baib syl bitrid ) BCDAFZGZHBCDAIJKZGZHZBELZCALZCBDHZMZBCUFUHUEUG + DANOPUJBILZUIUMQBETUIUNUMUIUNUKMULMUNUMMAIBCDRUNUKULSUAUBUCUD $. + ${ $d A y $. $d B y $. $d R y $. $( Elementhood in the domain of a restriction. (Contributed by Peter @@ -581242,6 +581424,37 @@ A collection of theorems for commuting equalities (or BCUCDOPQRUFUGASTUA $. $} + ${ + $d A x $. $d B x $. $d R x $. $d V x $. + $( Element of the range of a restriction. (Contributed by Peter Mazsa, + 26-Dec-2018.) $) + elrnres $p |- ( B e. V -> ( B e. ran ( R |` A ) <-> E. x e. A x R B ) ) $= + ( wcel cres crn cv wbr wex wrex elrng brres exbidv bitrd df-rex bitr4di + wa ) CEFZCDBGZHFZAIZBFUCCDJZSZAKZUDABLTUBUCCUAJZAKUFACUAEMTUGUEABUCCDENOP + UDABQR $. + $} + + ${ + $d A y $. $d B y $. $d R y $. + $( Element of the domain of a restriction to a singleton. (Contributed by + Peter Mazsa, 12-Jun-2024.) $) + eldmressnALTV $p |- ( B e. V -> + ( B e. dom ( R |` { A } ) <-> ( B = A /\ A e. dom R ) ) ) $= + ( vy wcel csn cres cdm wceq wa wbr wex eldmres elsng eldmg bicomd anbi12d + cv bitrd eqelb bitrdi ) BDFZBCAGZHIFZBAJZBCIZFZKZUFAUGFKUCUEBUDFZBESCLEMZ + KUIEUDBCDNUCUJUFUKUHBADOUCUHUKEBCDPQRTBAUGUAUB $. + $} + + ${ + $d A x $. $d B x $. $d R x $. $d W x $. + $( Element of the range of a restriction to a singleton. (Contributed by + Peter Mazsa, 12-Jun-2024.) $) + elrnressn $p |- ( ( A e. V /\ B e. W ) -> + ( B e. ran ( R |` { A } ) <-> A R B ) ) $= + ( vx wcel csn cres crn cv wbr wrex elrnres breq1 rexsng sylan9bbr ) BEGBC + AHZIJGFKZBCLZFRMADGABCLZFRBCENTUAFADSABCOPQ $. + $} + ${ $d A y $. $d R y $. $d V y $. $( Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018.) $) @@ -581325,6 +581538,13 @@ A collection of theorems for commuting equalities (or ( [ A ] `' _E = [ B ] `' _E <-> A = B ) ) $= ( wcel cep ccnv cec eccnvep eqeqan12d ) ACEBDEAFGZHABKHBACIBDIJ $. + $( Property of the epsilon relation. (Contributed by Peter Mazsa, + 27-Apr-2020.) $) + disjeccnvep $p |- ( ( A e. V /\ B e. W ) -> + ( ( [ A ] `' _E i^i [ B ] `' _E ) = (/) <-> ( A i^i B ) = (/) ) ) $= + ( wcel wa cep ccnv cec cin c0 eccnvep ineqan12d eqeq1d ) ACEZBDEZFAGHZIZBQI + ZJABJKOPRASBACLBDLMN $. + $( The restricted converse epsilon coset of an element of the restriction is the element itself. (Contributed by Peter Mazsa, 16-Jul-2019.) $) eccnvepres2 $p |- ( B e. A -> [ B ] ( `' _E |` A ) = B ) $= @@ -581594,6 +581814,40 @@ equivalence of domain elementhood (equivalence is not necessary as HUFUEUHPBUCUDQRSTUBUA $. $} + ${ + $d A x $. $d B x $. $d ps x $. + ceqsrexv2TEMP.1 $e |- ( x = A -> ( ph <-> ps ) ) $. + $( Alternate elimitation of a restricted existential quantifier, using + implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.) $) + ceqsrexv2TEMP $p |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) $= + ( ceqsrexbv ) ABCDEFG $. + $} + + ${ + $d x A $. $d x B $. $d ps x $. + ceqsralv2TEMP.1 $e |- ( x = A -> ( ph <-> ps ) ) $. + $( Alternate elimination of a restricted universal quantifier, using + implicit substitution. (Temporary: as soon as this Mathbox only PR is + accepted, I'll open a PR to place this to the main. PM) (Contributed by + Scott Fenton, 7-Dec-2020.) $) + ceqsralv2TEMP $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $= + ( cv wceq wi wral wcel wrex notbid ceqsrexv2TEMP rexanali 3bitr3i con4bii + wn wa annim ) CGDHZAICEJZDEKZBIZUAARZSCELUCBRZSUBRUDRUEUFCDEUAABFMNUAACEO + UCBTPQ $. + $} + + ${ + $d A x y $. $d B x y $. $d R x y $. + $( Two ways to say that an intersection of the identity relation with a + Cartesian product is a subclass. (Contributed by Peter Mazsa, + 12-Dec-2023.) $) + ref5 $p |- ( ( _I i^i ( A X. B ) ) C_ R <-> A. x e. ( A i^i B ) x R x ) $= + ( vy cv wceq wbr wi wral wcel cid cxp cin wss equcom imbi1i ceqsralv2TEMP + ralbii breq2 bitr3i idinxpss ralin 3bitr4i ) AFZEFZGZUEUFDHZIZECJZABJUECK + UEUEDHZIZABJLBCMNDOUKABCNJUJULABUJUFUEGZUHIZECJULUNUIECUMUGUHEAPQSUHUKEUE + CUFUEUEDTRUASAEBCDUBUKABCUCUD $. + $} + ${ $d x y $. $d A y $. $( Two ways to say that an intersection with a Cartesian product is a @@ -581851,7 +582105,7 @@ relation with an intersection with the same Cartesian product (see also ${ eqres.1 $e |- R = ( S |` C ) $. $( Converting a class constant definition by restriction (like ~ df-ers or - ~~? df-parts ) into a binary relation. (Contributed by Peter Mazsa, + ~ df-parts ) into a binary relation. (Contributed by Peter Mazsa, 1-Oct-2018.) $) eqres $p |- ( B e. V -> ( A R B <-> ( A e. C /\ A S B ) ) ) $= ( wbr cres wcel wa breqi brres bitrid ) ABDHABECIZHBFJACJABEHKABDOGLCABEF @@ -581939,6 +582193,33 @@ relation with an intersection with the same Cartesian product (see also ( ccnv crn cres cdm df-rn reseq2i wrel wceq relcnv dfrel5 mpbi eqtri ) ABZA CZDNNEZDZNOPNAFGNHQNIAJNKLM $. + $( Subset of restriction, special case. (Contributed by Peter Mazsa, + 10-Apr-2023.) $) + relssinxpdmrn $p |- ( Rel R -> + ( R C_ ( S i^i ( dom R X. ran R ) ) <-> R C_ S ) ) $= + ( wrel wss cdm crn cxp wa cin relssdmrn biantrud ssin bitr2di ) ACZABDZOAAE + AFGZDZHABPIDNQOAJKABPLM $. + + $( Two ways to say that a relation is a subclass. (Contributed by Peter + Mazsa, 11-Apr-2023.) $) + cnvref4 $p |- ( Rel R -> + ( ( R i^i ( dom R X. ran R ) ) C_ ( S i^i ( dom R X. ran R ) ) <-> + R C_ S ) ) $= + ( wrel cdm crn cxp cin wceq dfrel6 biimpi dmeqd rneqd xpeq12d ineq2d sseq2d + wss wb relxp relin2 relssinxpdmrn mp2b sseq1d bitrid bitr3d ) ACZAADZAEZFZG + ZBUIDZUIEZFZGZPZUIBUHGZPABPZUEUMUOUIUEULUHBUEUJUFUKUGUEUIAUEUIAHAIJZKUEUIAU + QLMNOUNUIBPZUEUPUHCUICUNURQUFUGRAUHSUIBTUAUEUIABUQUBUCUD $. + + ${ + $d R x y $. + $( Two ways to say that a relation is a subclass of the identity relation. + (Contributed by Peter Mazsa, 26-Jun-2019.) $) + cnvref5 $p |- ( Rel R -> ( R C_ _I <-> A. x A. y ( x R y -> x = y ) ) ) $= + ( wrel cid wss cv wbr wi wal ssrel3 wb cvv ideqg elv imbi2i 2albii bitrdi + wceq ) CDCEFAGZBGZCHZTUAEHZIZBJAJUBTUASZIZBJAJABCEKUDUFABUCUEUBUCUELBTUAM + NOPQR $. + $} + ${ $d A x $. $d B x $. $d R x $. $d V x $. $d W x $. $( Two ways of saying that the coset of ` A ` and the coset of ` B ` have @@ -582070,6 +582351,24 @@ relation with an intersection with the same Cartesian product (see also APZUFTABCUEDRUFUHUIACDSUAUB $. $} + $( Uniqueness is equivalent to non-existence or unique existence. Alternate + definition of the at-most-one quantifier, in terms of the existential + quantifier and the unique existential quantifier. (Contributed by Peter + Mazsa, 19-Nov-2024.) $) + moeu2 $p |- ( E* x ph <-> ( -. E. x ph \/ E! x ph ) ) $= + ( wmo wex weu wi wn wo moeu imor bitri ) ABCABDZABEZFLGMHABILMJK $. + + $( "At most one" picks a variable value, eliminating an existential + quantifier. The proof begins with references *2.21 ( ~ pm2.21 ) and + *14.26 ( ~ eupickbi ) from [WhiteheadRussell] p. 104 and p. 183. + (Contributed by Peter Mazsa, 18-Nov-2024.) + (Proof modification is discouraged.) $) + mopickr $p |- ( ( E* x ps /\ E. x ( ph /\ ps ) ) -> ( ps -> ph ) ) $= + ( wmo wa wex wi exancom wn weu wo moeu2 19.8a con3i pm2.21 syl a1d eupickbi + wal sp syl6bi jaoi sylbi syl5bi imp ) BCDZABECFZBAGZUGBAECFZUFUHABCHUFBCFZI + ZBCJZKUIUHGZBCLUKUMULUKUHUIUKBIUHBUJBCMNBAOPQULUIUHCSUHBACRUHCTUAUBUCUDUE + $. + $( Sufficient condition for transitivity of conjunctions inside existential quantifiers. (Contributed by Peter Mazsa, 2-Oct-2018.) $) moantr $p |- ( E* x ps -> @@ -582138,6 +582437,12 @@ relation with an intersection with the same Cartesian product (see also ZBJDCBDAKPBOCLMN $. $} + $( Intersection with a converse, binary relation. (Contributed by Peter + Mazsa, 24-Mar-2024.) $) + brcnvin $p |- ( ( A e. V /\ B e. W ) -> + ( A ( R i^i `' S ) B <-> ( A R B /\ B S A ) ) ) $= + ( ccnv cin wbr wa wcel brin brcnvg anbi2d bitrid ) ABCDGZHIABCIZABPIZJAEKBF + KJZQBADIZJABCPLSRTQABEFDMNO $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -582319,6 +582624,76 @@ relation with an intersection with the same Cartesian product (see also DUE $. $} + ${ + $d A u v $. $d R u v $. $d V u $. + $( Double restricted quantification over the union of a set and its + singleton. (Contributed by Peter Mazsa, 22-Aug-2023.) $) + disjressuc2 $p |- ( A e. V -> + ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) + ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) <-> + ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ + A. u e. A ( [ u ] R i^i [ A ] R ) = (/) ) ) ) $= + ( wcel cv wceq cec c0 wo wral wa eqeq1 eceq1 ineq1d eqeq1d orbi12d anbi2i + cin csn cun eqeq2 ineq2d 2ralunsn eqid biantru bitr4di eqcom bitrdi incom + orci w3a eqtrdi cbvralvw biimpi pm4.71i 3anass df-3an elneq neneqd biorfd + 3bitr2ri ralbiia ) CEFZBGZAGZHZVFDIZVGDIZTZJHZKZACCUAUBZLBVNLZVMACLBCLZVF + CHZVICDIZTZJHZKZBCLZMZVPVTBCLZMVEVOWCCVGHZVRVJTZJHZKZACLZMZWCVEVOWCWICCHZ + VRVRTZJHZKZMZMWJVMWAWHWNBACCEVQVHWEVLWGVFCVGNVQVKWFJVQVIVRVJVFCDOZPQRVGCH + ZVHVQVLVTVGCVFUCWQVKVSJWQVJVRVIVGCDOUDQRVQVQWKVTWMVFCCNVQVSWLJVQVIVRVRWPP + QRUEWIWOWCWNWIWKWMCUFULUGSUHWCVPWBWIMZMVPWBWIUMWJWBWRVPWBWIWBWIWAWHBACVHV + QWEVTWGVHVQWQWEVFVGCNVGCUIUJVHVSWFJVHVSVJVRTWFVHVIVJVRVFVGDOPVJVRUKUNQRUO + UPUQSVPWBWIURVPWBWIUSVCUJWDWBVPVTWABCVFCFZVQVTWSVFCVFCUTVAVBVDSUH $. + $} + + ${ + $d A y z $. $d B y z $. $d R y z $. $d S y z $. $d V y z $. + $d W y z $. + $( Two ways of saying that ` ( R |X. S ) ` -cosets are disjoint. + (Contributed by Peter Mazsa, 19-Jun-2020.) (Revised by Peter Mazsa, + 21-Aug-2023.) $) + disjecxrn $p |- ( ( A e. V /\ B e. W ) -> + ( ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) = (/) <-> + ( ( [ A ] R i^i [ B ] R ) = (/) \/ + ( [ A ] S i^i [ B ] S ) = (/) ) ) ) $= + ( vy vz wcel wa cec cin c0 wceq wne cv wbr wex copab bitrdi wo cxrn ecxrn + ineqan12d inopab eqtrdi an4 opabbii neeq1d opabn0 exdistrv ecinn0 anbi12d + wn bitr4d neanior necon4abid ) AEIZBFIZJZACKBCKLZMNADKBDKLZMNUAZACDUBZKZB + VDKZLZMUTVGMOZVAMOZVBMOZJZVCUNUTVHAGPZCQZBVLCQZJZGRZAHPZDQZBVQDQZJZHRZJZV + KUTVHVOVTJZHRGRZWBUTVHWCGHSZMOWDUTVGWEMUTVGVMVRJZVNVSJZJZGHSZWEUTVGWFGHSZ + WGGHSZLWIURUSVEWJVFWKGHACDEUCGHBCDFUCUDWFWGGHUEUFWHWCGHVMVRVNVSUGUHUFUIWC + GHUJTVOVTGHUKTUTVIVPVJWAGABCEFULHABDEFULUMUOVAMVBMUPTUQ $. + $} + + $( Two ways of saying that cosets are disjoint, special case of ~ disjecxrn . + (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, + 25-Aug-2023.) $) + disjecxrncnvep $p |- ( ( A e. V /\ B e. W ) -> + ( ( [ A ] ( R |X. `' _E ) i^i [ B ] ( R |X. `' _E ) ) = (/) <-> + ( ( A i^i B ) = (/) \/ ( [ A ] R i^i [ B ] R ) = (/) ) ) ) $= + ( wcel wa cep ccnv cxrn cec cin c0 wceq disjecxrn bitrdi disjeccnvep orbi1d + wo orcom bitrd ) ADFBEFGZACHIZJZKBUDKLMNZAUCKBUCKLMNZACKBCKLMNZSZABLMNZUGSU + BUEUGUFSUHABCUCDEOUGUFTPUBUFUIUGABDEQRUA $. + + ${ + $d A u v $. $d R u v $. $d V u $. + $( Double restricted quantification over the union of a set and its + singleton. (Contributed by Peter Mazsa, 22-Aug-2023.) $) + disjsuc2 $p |- ( A e. V -> + ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) + ( u = v \/ + ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) <-> + ( A. u e. A A. v e. A + ( u = v \/ + ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ + A. u e. A + ( ( u i^i A ) = (/) \/ + ( [ u ] R i^i [ A ] R ) = (/) ) ) ) ) $= + ( wcel cv wceq cep ccnv cxrn cec cin c0 wo csn cun wral wa disjressuc2 wb + cvv disjecxrncnvep el2v1 ralbidv anbi2d bitrd ) CEFZBGZAGZHUIDIJKZLZUJUKL + MNHOZACCPQZRBUNRUMACRBCRZULCUKLMNHZBCRZSUOUICMNHUIDLCDLMNHOZBCRZSABCUKETU + HUQUSUOUHUPURBCUHUPURUABUICDUBEUCUDUEUFUG $. + $} + ${ $d A u x y z $. $d B u x y z $. $d C u x y z $. $d R u x y z $. $d S u x y z $. @@ -582530,7 +582905,7 @@ relation with an intersection with the same Cartesian product (see also This concept simplifies theorems relating partition and equivalence: the left side of these theorems relate to ` R ` , the right side relate to - ` ,~ R ` (see e.g. ~~? pet ). Without the definition of ` ,~ R ` we + ` ,~ R ` (see e.g. ~ pet ). Without the definition of ` ,~ R ` we should have to relate the right side of these theorems to a composition of a converse (cf. ~ dfcoss3 ) or to the range of a range Cartesian product of classes (cf. ~ dfcoss4 ), which would make the theorems @@ -582583,6 +582958,43 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these ZCFAGPDFAGHBICDJAAKLCDBAMCDBAANO $. $} + ${ + $d R u x y $. + $( Class of cosets by the converse of ` R ` (Contributed by Peter Mazsa, + 17-Jun-2020.) $) + cosscnv $p |- ,~ `' R = { <. x , y >. | E. u ( x R u /\ y R u ) } $= + ( ccnv ccoss cv wbr wa wex copab df-coss wb cvv brcnvg el2v anbi12i exbii + opabbii eqtri ) DEZFCGZAGZUAHZUBBGZUAHZIZCJZABKUCUBDHZUEUBDHZIZCJZABKABCU + ALUHULABUGUKCUDUIUFUJUDUIMCAUBUCNNDOPUFUJMCBUBUENNDOPQRST $. + $} + + ${ + $d A u v x $. $d R u v x $. + $( Class of cosets by the converse of a restriction. (Contributed by Peter + Mazsa, 8-Jun-2020.) $) + coss1cnvres $p |- ,~ `' ( R |` A ) = + { <. u , v >. | + ( ( u e. A /\ v e. A ) /\ E. x ( u R x /\ v R x ) ) } $= + ( cres ccnv ccoss cv wbr wex copab wcel df-coss cvv br1cnvres elv anbi12i + wa wb an4 bitr4i exbii 19.42v bitri opabbii eqtri ) EDFGZHAIZCIZUHJZUIBIZ + UHJZSZAKZCBLUJDMZULDMZSZUJUIEJZULUIEJZSZAKSZCBLCBAUHNUOVBCBUOURVASZAKVBUN + VCAUNUPUSSZUQUTSZSVCUKVDUMVEUKVDTADUIUJEOPQUMVETADUIULEOPQRUPUQUSUTUAUBUC + URVAAUDUEUFUG $. + $} + + ${ + $d A u v x $. + $( Special case of ~ coss1cnvres . (Contributed by Peter Mazsa, + 8-Jun-2020.) $) + coss2cnvepres $p |- ,~ `' ( `' _E |` A ) = + { <. u , v >. | + ( ( u e. A /\ v e. A ) /\ E. x ( x e. u /\ x e. v ) ) } $= + ( cep ccnv cres ccoss cv wcel wa wbr wex copab coss1cnvres wb cvv brcnvep + elv anbi12i exbii anbi2i opabbii eqtri ) EFZDGFHCIZDJBIZDJKZUFAIZUELZUGUI + UELZKZAMZKZCBNUHUIUFJZUIUGJZKZAMZKZCBNABCDUEOUNUSCBUMURUHULUQAUJUOUKUPUJU + OPCUFUIQRSUKUPPBUGUIQRSTUAUBUCUD $. + $} + $( If ` A ` is a set then the class of cosets by ` A ` is a set. (Contributed by Peter Mazsa, 4-Jan-2019.) $) cossex $p |- ( A e. V -> ,~ A e. _V ) $= @@ -582791,6 +583203,64 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these CDEBJKLAMZCELSDELIABNCSEOZHDTHIABNABCDEFGPABCDEEFGQR $. $} + $( Binary relation on a restriction to a singleton. (Contributed by Peter + Mazsa, 11-Jun-2024.) $) + brressn $p |- ( ( B e. V /\ C e. W ) -> + ( B ( R |` { A } ) C <-> ( B = A /\ B R C ) ) ) $= + ( wcel wa csn cres wbr wceq wb brres adantl elsng adantr anbi1d bitrd ) BEG + ZCFGZHZBCDAIZJKZBUCGZBCDKZHZBALZUFHUAUDUGMTUCBCDFNOUBUEUHUFTUEUHMUABAEPQRS + $. + + ${ + $d A a u $. $d R a u $. + $( A class ' R ' restricted to the singleton of the class ' A ' is the + ordered pair class abstraction of the class ' A ' and the sets in + relation ' R ' to ' A ' (and not in relation to the singleton ' { A + } ' ). (Contributed by Peter Mazsa, 16-Jun-2024.) $) + ressn2 $p |- ( R |` { A } ) = { <. a , u >. | ( a = A /\ A R u ) } $= + ( csn cres cv wcel wbr copab wceq dfres2 velsn anbi1i eqbrb bitri opabbii + wa eqtri ) CBEZFDGZTHZUAAGZCIZRZDAJUABKZBUCCIRZDAJDATCLUEUGDAUEUFUDRUGUBU + FUDDBMNUABUCCOPQS $. + $} + + ${ + $d A x $. $d V x $. + $( Any class ' R ' restricted to the singleton of the set ' A ' (see + ~ ressn2 ) is reflexive, see also ~ refrelressn . (Contributed by Peter + Mazsa, 12-Jun-2024.) $) + refressn $p |- ( A e. V -> + A. x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) + x ( R |` { A } ) x ) $= + ( wcel cv csn cres wbr cdm crn cin wceq wa wi elin wb cvv adantr sylbi + eldmressnALTV elv simplbi a1i elrnressn elvd biimpd adantld syl5bi eqcomd + breq1d mpbidi jcad brressn el2v syl6ibr ralrimiv ) BDEZAFZUSCBGHZIZAUTJZU + TKZLZURUSVDEZUSBMZUSUSCIZNZVAURVEVFVGVEVFOURVEUSVBEZUSVCEZNZVFUSVBVCPZVIV + FVJVIVFBCJEZVIVFVMNQABUSCRUAUBUCZSTUDVEBUSCIZVGURVEVKURVOVLURVJVOVIURVJVO + URVJVOQABUSCDRUEUFUGUHUIVEVKVOVGQZVLVIVPVJVIBUSUSCVIUSBVNUJUKSTULUMVAVHQA + ABUSUSCRRUNUOUPUQ $. + $} + + $( Every class ' R ' restricted to the singleton of the class ' A ' (see + ~ ressn2 ) is antisymmetric. (Contributed by Peter Mazsa, + 11-Jun-2024.) $) + antisymressn $p |- + A. x A. y ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) x ) -> x = y ) $= + ( cv csn cres wbr wa wceq wi wb cvv brressn el2v simplbi eqtr3 syl2an gen2 + ) AEZBEZDCFGZHZUATUBHZITUAJZKABUCTCJZUACJZUEUDUCUFTUADHZUCUFUHILABCTUADMMNO + PUDUGUATDHZUDUGUIILBACUATDMMNOPTUACQRS $. + + $( Any class ' R ' restricted to the singleton of the class ' A ' (see + ~ ressn2 ) is transitive, see also ~ trrelressn . (Contributed by Peter + Mazsa, 16-Jun-2024.) $) + trressn $p |- + A. x A. y A. z ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) z ) -> + x ( R |` { A } ) z ) $= + ( cv csn cres wbr wa wi wal wceq eqbrb anbi12i 3imtr4i wb cvv brressn el2v + an3 gen2 ax-gen ) AFZBFZEDGHZIZUECFZUFIZJZUDUHUFIZKZCLBLAULBCUDDMZUDUEEIJZU + EDMZUEUHEIJZJZUMUDUHEIJZUJUKUMDUEEIZJZUODUHEIZJZJUMVAJUQURUMUSUOVAUAUNUTUPV + BUDDUEENUEDUHENOUDDUHENPUGUNUIUPUGUNQABDUDUEERRSTUIUPQBCDUEUHERRSTOUKURQACD + UDUHERRSTPUBUC $. + ${ $d A x $. $d B x $. $d R x $. $d V x $. $d W x $. $( ` A ` and ` B ` are cosets by relation ` R ` : a binary relation. @@ -582821,9 +583291,9 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these ${ $d A u $. $d B u $. $d C u $. $d D u $. $d E u $. $d R u $. $d S u $. $d V u $. $d W u $. $d X u $. $d Y u $. - $( ` <. B , C >. ` and ` <. D , E >. ` are cosets by an intersection with a - restriction: a binary relation. (Contributed by Peter Mazsa, - 8-Jun-2021.) $) + $( ` <. B , C >. ` and ` <. D , E >. ` are cosets by an range Cartesian + product with a restriction: a binary relation. (Contributed by Peter + Mazsa, 8-Jun-2021.) $) br1cossxrnres $p |- ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) -> ( <. B , C >. ,~ ( R |X. ( S |` A ) ) <. D , E >. <-> @@ -583593,6 +584063,16 @@ when we switch from (general) sets to relations in ~ dfrefrels2 , UCCQTUA $. $} + ${ + $d R x $. + $( Alternate definition of the reflexive relation predicate. (Contributed + by Peter Mazsa, 12-Dec-2023.) $) + dfrefrel5 $p |- ( RefRel R <-> + ( A. x e. ( dom R i^i ran R ) x R x /\ Rel R ) ) $= + ( wrefrel cid cdm crn cxp cin wss wrel cv wbr wral dfrefrel2 ref5 bianbi + ) BCDBEZBFZGHBIBJAKZSBLAQRHMBNAQRBOP $. + $} + ${ $d R r $. $( Element of the class of reflexive relations. (Contributed by Peter @@ -583642,6 +584122,15 @@ when we switch from (general) sets to relations in ~ dfrefrels2 , ( ccoss wrefrel cid cdm crn cxp cin wss wrel wa refrelcoss2 dfrefrel2 mpbir ) ABZCDOEOFGHOIOJKALOMN $. + ${ + $d A x $. $d R x $. $d V x $. + $( Any class ' R ' restricted to the singleton of the set ' A ' (see + ~ ressn2 ) is reflexive. (Contributed by Peter Mazsa, 12-Jun-2024.) $) + refrelressn $p |- ( A e. V -> RefRel ( R |` { A } ) ) $= + ( vx wcel cv csn cres wbr cdm crn cin wral wrel refressn relres dfrefrel5 + wrefrel sylanblrc ) ACEDFZTBAGZHZIDUBJUBKLMUBNUBRDABCOBUAPDUBQS $. + $} + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -583725,6 +584214,22 @@ and disjoints ( ~ df-disjs , ~ df-disjALTV ). FLCQUEUGUFABUBUCCSTUA $. $} + $( Alternate definition of the converse reflexive relation predicate. + (Contributed by Peter Mazsa, 25-May-2024.) $) + dfcnvrefrel4 $p |- ( CnvRefRel R <-> ( R C_ _I /\ Rel R ) ) $= + ( wcnvrefrel cdm crn cxp cin cid wss wrel df-cnvrefrel cnvref4 bianim ) ABA + ACADEZFGMFHAIAGHAJAGKL $. + + ${ + $d R x y $. + $( Alternate definition of the converse reflexive relation predicate. + (Contributed by Peter Mazsa, 25-May-2024.) $) + dfcnvrefrel5 $p |- ( CnvRefRel R <-> + ( A. x A. y ( x R y -> x = y ) /\ Rel R ) ) $= + ( wcnvrefrel cid wss wrel cv wbr wceq wi wal dfcnvrefrel4 cnvref5 bianim + ) CDCEFCGAHZBHZCIPQJKBLALCMABCNO $. + $} + ${ $d R r $. $( Element of the class of converse reflexive relations. (Contributed by @@ -584241,6 +584746,14 @@ class of symmetric relations as well (like the elements of the class of ( wceq ccom wrel wa wtrrel coideq id sseq12d releq anbi12d dftrrel2 3bitr4g wss ) ABCZAADZAOZAEZFBBDZBOZBEZFAGBGPRUASUBPQTABABHPIJABKLAMBMN $. + ${ + $d A x y z $. $d R x y z $. + $( Any class ' R ' restricted to the singleton of the class ' A ' (see + ~ ressn2 ) is transitive. (Contributed by Peter Mazsa, 17-Jun-2024.) $) + trrelressn $p |- TrRel ( R |` { A } ) $= + ( vx vy vz csn cres wtrrel cv wbr wa wi wal wrel relres dftrrel3 mpbir2an + trressn ) BAFZGZHCIZDIZTJUBEIZTJKUAUCTJLEMDMCMTNCDEABRBSOCDETPQ $. + $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -584906,13 +585419,19 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation. n0eldmqseq $p |- ( ( dom R /. R ) = A -> -. (/) e. A ) $= ( cdm cqs wceq c0 wcel n0eldmqs eleq2 mtbii ) BCBDZAEFKGFAGBHKAFIJ $. + $( Implication of that the empty set is not an element of a class. + (Contributed by Peter Mazsa, 30-Dec-2024.) $) + n0elim $p |- ( -. (/) e. A -> + ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) $= + ( c0 wcel cep ccnv cres cdm cqs wceq n0el2 biimpi qseq1d qsresid qsid eqtri + wn eqtrdi ) BACPZDEZAFZGZTHATHZARUAATRUAAIAJKLUBASHAASMANOQ $. + $( Two ways of expressing that the empty set is not an element of a class. (Contributed by Peter Mazsa, 27-May-2021.) $) n0el3 $p |- ( -. (/) e. A <-> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) $= - ( c0 wcel cep ccnv cres cdm cqs wceq n0el2 biimpi qseq1d qsresid qsid eqtri - wn eqtrdi n0eldmqseq impbii ) BACPZDEZAFZGZUBHZAITUDAUBHZATUCAUBTUCAIAJKLUE - AUAHAAUAMANOQAUBRS $. + ( c0 wcel wn cep ccnv cres cdm cqs wceq n0elim n0eldmqseq impbii ) BACDEFAG + ZHNIAJAKANLM $. $( The domain quotient binary relation of the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the @@ -584955,7 +585474,7 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation. ( wcel wrel cdm cqs wceq crn cuni wi wa unieq wb unidmqseq imp syl5ib ex ) BCDZBEZBFBGZAHZBIAJZHZKUBUAJUCHZSTLUDUAAMSTUEUDNUCBCOPQR $. - $( Lemma for ~ erim2 . (Contributed by Peter Mazsa, 29-Dec-2021.) $) + $( Lemma for ~ erimeq2 . (Contributed by Peter Mazsa, 29-Dec-2021.) $) dmqseqim2 $p |- ( R e. V -> ( Rel R -> ( ( dom R /. R ) = A -> ( B e. ran R <-> B e. U. A ) ) ) ) $= ( wcel wrel cdm cqs wceq crn cuni wb dmqseqim eleq2 syl8 ) CDECFCGCHAICJZAK @@ -585037,14 +585556,13 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation. component ( ` dom R = A ` ) of the present ~ df-er . While we acknowledge the need of a domain component, the present ~ df-er definition does not utilize the results revealed by the new theorems in the - Partition-Equivalence Theorem part below (like ~~? pets and ~~? pet ). - From those theorems follows that the natural domain of equivalence - relations is + Partition-Equivalence Theorem part below (like ~ pets and ~ pet ). From + those theorems follows that the natural domain of equivalence relations is not ` R Domain A ` (i.e. ` dom R = A ` see ~ brdomaing ), but ` R DomainQss A ` (i.e. ` ( dom R /. R ) = A ` , see ~ brdmqss ), see - ~ erim vs. ~ prter3 . + ~ erimeq vs. ~ prter3 . While I'm sure we need both equivalence relation ~ df-eqvrels and equivalence relation on domain quotient ~ df-ers , I'm not sure whether we @@ -585063,21 +585581,21 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation. ~ brerser . (Contributed by Peter Mazsa, 12-Aug-2021.) $) df-erALTV $a |- ( R ErALTV A <-> ( EqvRel R /\ R DomainQs A ) ) $. - $( Define the class of membership equivalence relations on their domain + $( Define the class of comember 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 . + $( Define the comember equivalence relation on the class ` A ` (or, the + restricted coelement equivalence relation on its domain quotient ` 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.) $) @@ -585114,28 +585632,30 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation. ( wceq werALTV wb erALTVeq1 syl ) ACDFBCGBDGHEBCDIJ $. $} - $( Alternate definition of the membership equivalence relation. (Contributed + $( Alternate definition of the comember 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 - ccoss ) ABACDAELZFAAGZFAHANMAIJK $. + dfcomember $p |- ( CoMembEr A <-> ~ A ErALTV A ) $= + ( wcomember ccnv cres werALTV ccoels df-comember df-coels erALTVeq1i bitr4i + cep ccoss ) ABAKCADLZEAAFZEAGANMAHIJ $. - $( Alternate definition of the membership equivalence relation. (Contributed + $( Alternate definition of the comember 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 ) - ABAACZDMEMFMGAHIAJAMKL $. + dfcomember2 $p |- ( CoMembEr A <-> + ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) ) $= + ( wcomember ccoels werALTV weqvrel cdm cqs wceq dfcomember dferALTV2 bitri + wa ) ABAACZDMEMFMGAHLAIAMJK $. - $( Alternate definition of the membership equivalence relation. (Contributed + $( Alternate definition of the comember 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 - cuni bicomi dmqscoelseq anbi12i bitri ) ABACZDZQEQFAGZHAIZALQFAGZHAJRTSUATR - AKMANOP $. - - $( Two ways to express membership equivalence relation on its domain - quotient. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter - Mazsa, 17-Jul-2023.) $) + dfcomember3 $p |- ( CoMembEr A <-> + ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) $= + ( wcomember ccoels weqvrel cdm wceq wa wcoeleqvrel dfcomember2 dfcoeleqvrel + cqs cuni bicomi dmqscoelseq anbi12i bitri ) ABACZDZQEQKAFZGAHZALQKAFZGAIRTS + UATRAJMANOP $. + + $( Two ways to express comember equivalence relation on its domain quotient. + (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, + 17-Jul-2023.) $) eqvreldmqs $p |- ( ( EqvRel ,~ ( `' _E |` A ) /\ ( dom ,~ ( `' _E |` A ) /. ,~ ( `' _E |` A ) ) = A ) <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) $= @@ -585143,6 +585663,14 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation. cuni bicomi dmqs1cosscnvepreseq anbi12i ) BCADEZFZAGZQHQIAJAMAKIAJSRALNAOP $. + $( Two ways to express comember equivalence relation on its domain quotient. + (Contributed by Peter Mazsa, 30-Dec-2024.) $) + eqvreldmqs2 $p |- ( ( EqvRel ,~ ( `' _E |` A ) /\ + ( dom ,~ ( `' _E |` A ) /. ,~ ( `' _E |` A ) ) = A ) <-> + ( EqvRel ~ A /\ ( U. A /. ~ A ) = A ) ) $= + ( cep ccnv cres ccoss weqvrel ccoels cdm cqs wceq df-coels eqvreleqi bicomi + cuni dmqs1cosscnvepreseq anbi12i ) BCADEZFZAGZFZQHQIAJANSIAJTRSQAKLMAOP $. + $( Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when ` A ` and ` R ` are sets. (Contributed by Peter Mazsa, 25-Aug-2021.) $) @@ -585156,10 +585684,10 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation. $d A u x y $. $d R u x y $. $d V x y $. $( Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is ~ prter3 in a - more convenient form , see also ~ erim ). (Contributed by Rodolfo + more convenient form , see also ~ erimeq ). (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 29-Dec-2021.) $) - erim2 $p |- ( R e. V -> + erimeq2 $p |- ( R e. V -> ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ~ A = R ) ) $= ( vx vy vu wcel wceq wa wrel ad2antrl cv wbr wrex wb simpll eleq2d bitrdi cvv el2v weqvrel cdm cqs ccoels relcoels a1i eqvrelrel brcoels cec simprl @@ -585178,12 +585706,11 @@ coelements on the domain is equal to the relation (this is ~ prter3 in a $( Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is the most - convenient form of ~ prter3 and ~ erim2 ). (Contributed by Peter Mazsa, + convenient form of ~ prter3 and ~ erimeq2 ). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.) $) - erim $p |- ( R e. V -> ( R ErALTV A -> ~ A = R ) ) $= - ( werALTV weqvrel cdm cqs wceq wa wcel ccoels dferALTV2 erim2 syl5bi ) ABDB - EBFBGAHIBCJAKBHABLABCMN $. - + erimeq $p |- ( R e. V -> ( R ErALTV A -> ~ A = R ) ) $= + ( werALTV weqvrel cdm cqs wceq wa wcel ccoels dferALTV2 erimeq2 syl5bi ) AB + DBEBFBGAHIBCJAKBHABLABCMN $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -585440,22 +585967,22 @@ instead of simply using converse functions (cf. ~ dfdisjALTV ). ~ dfdisjALTV5 . (Contributed by Peter Mazsa, 17-Jul-2021.) $) df-disjALTV $a |- ( Disj R <-> ( CnvRefRel ,~ `' R /\ Rel R ) ) $. - $( Define the disjoint elementhood relations class, i.e., the disjoint - elements class. The element of the disjoint elements class and the - disjoint elementhood predicate are the same, that is + $( Define the disjoint element relations class, i.e., the disjoint elements + class. The element of the disjoint elements class and the disjoint + elementhood predicate are the same, that is ` ( A e. ElDisjs <-> ElDisj A ) ` when ` A ` is a set, see ~ eleldisjseldisj . (Contributed by Peter Mazsa, 28-Nov-2022.) $) df-eldisjs $a |- ElDisjs = { a | ( `' _E |` a ) e. Disjs } $. - $( Define the disjoint elementhood relation predicate, i.e., the disjoint + $( Define the disjoint element relation predicate, i.e., the disjoint elementhood predicate. Read: the elements of ` A ` are disjoint. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is ` ( A e. ElDisjs <-> ElDisj A ) ` when ` A ` is a set, see ~ eleldisjseldisj . As of now, disjoint elementhood is defined as "partition" in set.mm : - compare ~ df-prt with ~ dfeldisj5 . See also the comments of ~~? - dfmembpart2 and of ~~? df-parts . (Contributed by Peter Mazsa, + compare ~ df-prt with ~ dfeldisj5 . See also the comments of + ~ dfmembpart2 and of ~ df-parts . (Contributed by Peter Mazsa, 17-Jul-2021.) $) df-eldisj $a |- ( ElDisj A <-> Disj ( `' _E |` A ) ) $. @@ -585723,8 +586250,8 @@ instead of simply using converse functions (cf. ~ dfdisjALTV ). ( wceq wdisjALTV wb disjeq syl ) ABCEBFCFGDBCHI $. $} - $( Lemma for the equality theorem for partition ~~? parteq1 . (Contributed - by Peter Mazsa, 5-Oct-2021.) $) + $( Lemma for the equality theorem for partition ~ parteq1 . (Contributed by + Peter Mazsa, 5-Oct-2021.) $) disjdmqseqeq1 $p |- ( R = S -> ( ( Disj R /\ ( dom R /. R ) = A ) <-> ( Disj S /\ ( dom S /. S ) = A ) ) ) $= @@ -585775,6 +586302,27 @@ instead of simply using converse functions (cf. ~ dfdisjALTV ). ( wceq weldisj wb eldisjeq syl ) ABCEBFCFGDBCHI $. $} + ${ + $d A u v x $. $d R u v x $. + $( Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023.) $) + disjres $p |- ( Rel R -> + ( Disj ( R |` A ) <-> + A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) ) ) $= + ( vx wrel cres wdisjALTV cv wbr wrmo wal wceq cec cin c0 wral wmo relres + wo dfdisjALTV4 mpbiran2 wcel wa wb cvv brres elv mobii df-rmo albii bitri + bitr4i id inecmo bitr4id ) DFDCGZHZBIZEIZDJZBCKZELZUSAIZMZUSDNVDDNOPMTACQ + BCQURUSUTUQJZBRZELZVCURVHUQFDCSEBUQUAUBVGVBEVGUSCUCVAUDZBRVBVFVIBVFVIUEEC + USUTDUFUGUHUIVABCUJUMUKULBAECUSVDDVEUNUOUP $. + $} + + $( Two forms of disjoint elements when the empty set is not an element of the + class. (Contributed by Peter Mazsa, 31-Dec-2024.) $) + eldisjn0elb $p |- ( ( ElDisj A /\ -. (/) e. A ) <-> + ( Disj ( `' _E |` A ) /\ + ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) ) $= + ( weldisj cep ccnv cres wdisjALTV c0 wcel wn cdm cqs wceq df-eldisj anbi12i + n0el3 ) ABCDAEZFGAHIPJPKALAMAON $. + $( Two ways of saying that a range Cartesian product is disjoint. (Contributed by Peter Mazsa, 17-Jun-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) $) @@ -585782,6 +586330,19 @@ instead of simply using converse functions (cf. ~ dfdisjALTV ). ( cxrn wdisjALTV ccnv ccoss cid wss cin wrel xrnrel dfdisjALTV2 1cosscnvxrn mpbiran2 sseq1i bitri ) ABCZDZQEFZGHZAEFBEFIZGHRTQJABKQLNSUAGABMOP $. + ${ + $d A u v $. $d R u v $. $d S u v $. + $( Disjoint range Cartesian product. (Contributed by Peter Mazsa, + 25-Aug-2023.) $) + disjxrnres5 $p |- ( Disj ( R |X. ( S |` A ) ) <-> + A. u e. A A. v e. A + ( u = v \/ ( [ u ] ( R |X. S ) i^i [ v ] ( R |X. S ) ) = (/) ) ) $= + ( cres cxrn wdisjALTV cv wceq cec cin c0 wral xrnres2 disjeqi wrel xrnrel + wo wb disjres ax-mp bitr3i ) DECFGZHDEGZCFZHZBIZAIZJUHUEKUIUEKLMJSACNBCNZ + UFUDCDEOPUEQUGUJTDERABCUEUAUBUC $. + $} + + $( Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) $) disjorimxrn $p |- ( ( Disj R \/ Disj S ) -> Disj ( R |X. S ) ) $= @@ -585846,6 +586407,883 @@ instead of simply using converse functions (cf. ~ dfdisjALTV ). disjALTVxrnidres $p |- Disj ( R |X. ( _I |` A ) ) $= ( cid wdisjALTV cres cxrn disjALTVid disjimxrnres ax-mp ) CDBCAEFDGABCHI $. + ${ + $d A u v $. $d R u v $. $d V u $. + $( Disjoint range Cartesian product, special case. (Contributed by Peter + Mazsa, 25-Aug-2023.) $) + disjsuc $p |- ( A e. V -> + ( Disj ( R |X. ( `' _E |` suc A ) ) <-> + ( Disj ( R |X. ( `' _E |` A ) ) /\ + A. u e. A + ( ( u i^i A ) = (/) \/ + ( [ u ] R i^i [ A ] R ) = (/) ) ) ) ) $= + ( vv wcel cv wceq cep ccnv cxrn cec c0 wo wral cres wdisjALTV disjxrnres5 + cin wa csn cun csuc disjsuc2 df-suc reseq2i xrneq2i disjeqi bitri 3bitr4g + anbi1i ) BDFAGZEGZHULCIJZKZLUMUOLSMHNZEBBUAUBZOAUQOZUPEBOABOZULBSMHULCLBC + LSMHNABOZTCUNBUCZPZKZQZCUNBPKQZUTTEABCDUDVDCUNUQPZKZQURVCVGVBVFCVAUQUNBUE + UFUGUHEAUQCUNRUIVEUSUTEABCUNRUKUJ $. + $} + +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Antisymmetry +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + $( Define the antisymmetric relation predicate. (Read: ` R ` is an + antisymmetric relation.) (Contributed by Peter Mazsa, 24-Jun-2024.) $) + df-antisymrel $a |- ( AntisymRel R <-> + ( CnvRefRel ( R i^i `' R ) /\ Rel R ) ) $. + + $( Alternate definition of the antisymmetric relation predicate. + (Contributed by Peter Mazsa, 24-Jun-2024.) $) + dfantisymrel4 $p |- ( AntisymRel R <-> + ( ( R i^i `' R ) C_ _I /\ Rel R ) ) $= + ( wantisymrel ccnv cin wcnvrefrel cid wss df-antisymrel relcnv relin2 ax-mp + wrel dfcnvrefrel4 mpbiran2 bianbi ) ABAACZDZEZALQFGZAHRSQLZPLTAIAPJKQMNO $. + + ${ + $d R x y $. + $( Alternate definition of the antisymmetric relation predicate. + (Contributed by Peter Mazsa, 24-Jun-2024.) $) + dfantisymrel5 $p |- ( AntisymRel R <-> + ( A. x A. y ( ( x R y /\ y R x ) -> x = y ) /\ Rel R ) ) $= + ( wantisymrel ccnv cin wcnvrefrel wrel cv wa wceq wi df-antisymrel relcnv + wbr wal relin2 ax-mp dfcnvrefrel5 cvv mpbiran2 brcnvin el2v imbi1i 2albii + wb bitri bianbi ) CDCCEZFZGZCHAIZBIZCOUMULCOJZULUMKZLZBPAPZCMUKULUMUJOZUO + LZBPAPZUQUKUTUJHZUIHVACNCUIQRABUJSUAUSUPABURUNUOURUNUFABULUMCCTTUBUCUDUEU + GUH $. + $} + + ${ + $d A x y $. $d R x y $. + $( (Contributed by Peter Mazsa, 25-Jun-2024.) $) + antisymrelres $p |- ( AntisymRel ( R |` A ) <-> + A. x e. A A. y e. A ( ( x R y /\ y R x ) -> x = y ) ) $= + ( cres wantisymrel cv wbr wa wceq wi wal wcel wral wrel relres wb cvv elv + brres dfantisymrel5 mpbiran2 anbi12i bitri imbi1i 2albii r2alan 3bitri + an4 ) DCEZFZAGZBGZUJHZUMULUJHZIZULUMJZKZBLALZULCMZUMCMZIULUMDHZUMULDHZIZI + ZUQKZBLALVDUQKBCNACNUKUSUJODCPABUJUAUBURVFABUPVEUQUPUTVBIZVAVCIZIVEUNVGUO + VHUNVGQBCULUMDRTSUOVHQACUMULDRTSUCUTVBVAVCUIUDUEUFVDUQABCCUGUH $. + $} + + ${ + $d A x y $. $d R x y $. + $( (Contributed by Peter Mazsa, 29-Jun-2024.) $) + antisymrelressn $p |- AntisymRel ( R |` { A } ) $= + ( vx vy csn cres wantisymrel cv wbr wa wceq wi antisymressn dfantisymrel5 + wal wrel relres mpbir2an ) BAEZFZGCHZDHZTIUBUATIJUAUBKLDOCOTPCDABMBSQCDTN + R $. + $} + +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Partitions: disjoints on domain quotients +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + $( Define the class of all partitions, cf. the comment of ~ df-disjs . + Partitions are disjoints on domain quotients (or: domain quotients + restricted to disjoints). + + This is a more general meaning of partition than we we are familiar with: + the conventional meaning of partition (e.g. partition ` A ` of ` X ` , + [Halmos] p. 28: "A partition of ` X ` is a disjoint collection ` A ` of + non-empty subsets of ` X ` whose union is ` X ` ", or Definition 35, + [Suppes] p. 83., cf. https://oeis.org/A000110 ) is what we call membership + partition here, cf. ~ dfmembpart2 . + + The binary partitions relation and the partition predicate are the same, + that is, ` ( R Parts A <-> R Part A ) ` if ` A ` and ` R ` are sets, cf. + ~ brpartspart . (Contributed by Peter Mazsa, 26-Jun-2021.) $) + df-parts $a |- Parts = ( DomainQss |` Disjs ) $. + + $( Define the partition predicate (read: ` A ` is a partition by ` R ` ). + Alternative definition is ~ dfpart2 . The binary partition and the + partition predicate are the same if ` A ` and ` R ` are sets, cf. + ~ brpartspart . (Contributed by Peter Mazsa, 12-Aug-2021.) $) + df-part $a |- ( R Part A <-> ( Disj R /\ R DomainQs A ) ) $. + + $( Define the class of member partition relations on their domain quotients. + (Contributed by Peter Mazsa, 26-Jun-2021.) $) + df-membparts $a |- MembParts = { a | ( `' _E |` a ) Parts a } $. + + $( Define the member partition predicate, or the disjoint restricted element + relation on its domain quotient predicate. (Read: ` A ` is a member + partition.) A alternative definition is ~ dfmembpart2 . + + Member partition is the conventional meaning of partition (see the notes + of ~ df-parts and ~ dfmembpart2 ), we generalize the concept in ~ df-parts + and ~ df-part . + + Member partition and comember equivalence are the same by ~ mpet . + (Contributed by Peter Mazsa, 26-Jun-2021.) $) + df-membpart $a |- ( MembPart A <-> ( `' _E |` A ) Part A ) $. + + $( Alternate definition of the partition predicate. (Contributed by Peter + Mazsa, 5-Sep-2021.) $) + dfpart2 $p |- ( R Part A <-> ( Disj R /\ ( dom R /. R ) = A ) ) $= + ( wpart wdisjALTV wdmqs wa cdm cqs wceq df-part df-dmqs anbi2i bitri ) ABCB + DZABEZFNBGBHAIZFABJOPNABKLM $. + + $( Alternate definition of the conventional membership case of partition. + Partition ` A ` of ` X ` , [Halmos] p. 28: "A partition of ` X ` is a + disjoint collection ` A ` of non-empty subsets of ` X ` whose union is + ` X ` ", or Definition 35, [Suppes] p. 83., cf. https://oeis.org/A000110 . + (Contributed by Peter Mazsa, 14-Aug-2021.) $) + dfmembpart2 $p |- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) $= + ( wmembpart cep ccnv cres wpart wdisjALTV wdmqs wa weldisj wcel df-membpart + c0 wn df-part df-eldisj bicomi cnvepresdmqs anbi12i 3bitri ) ABACDAEZFUAGZA + UAHZIAJZMAKNZIALAUAOUBUDUCUEUDUBAPQARST $. + + $( Binary partitions relation. (Contributed by Peter Mazsa, 23-Jul-2021.) $) + brparts $p |- ( A e. V -> + ( R Parts A <-> ( R e. Disjs /\ R DomainQss A ) ) ) $= + ( cdisjs cparts cdmqss df-parts eqres ) BADEFCGH $. + + $( Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021.) $) + brparts2 $p |- ( ( A e. V /\ R e. W ) -> + ( R Parts A <-> ( R e. Disjs /\ ( dom R /. R ) = A ) ) ) $= + ( wcel wa cparts wbr cdisjs cdmqss cdm cqs wb brparts adantr brdmqss anbi2d + wceq bitrd ) ACEZBDEZFZBAGHZBIEZBAJHZFZUDBKBLARZFTUCUFMUAABCNOUBUEUGUDABCDP + QS $. + + $( Binary partition and the partition predicate are the same if ` A ` and + ` R ` are sets. (Contributed by Peter Mazsa, 5-Sep-2021.) $) + brpartspart $p |- ( ( A e. V /\ R e. W ) -> ( R Parts A <-> R Part A ) ) $= + ( wcel wa cdisjs cdmqss wbr wdisjALTV wdmqs cparts wpart eldisjsdisj adantl + wb brdmqssqs anbi12d brparts adantr df-part a1i 3bitr4d ) ACEZBDEZFZBGEZBAH + IZFZBJZABKZFZBALIZABMZUFUGUJUHUKUEUGUJPUDBDNOABCDQRUDUMUIPUEABCSTUNULPUFABU + AUBUC $. + + $( Equality theorem for partition. (Contributed by Peter Mazsa, + 5-Oct-2021.) $) + parteq1 $p |- ( R = S -> ( R Part A <-> S Part A ) ) $= + ( wceq wdisjALTV cdm cqs wa wpart disjdmqseqeq1 dfpart2 3bitr4g ) BCDBEBFBG + ADHCECFCGADHABIACIABCJABKACKL $. + + $( Equality theorem for partition. (Contributed by Peter Mazsa, + 25-Jul-2024.) $) + parteq2 $p |- ( A = B -> ( R Part A <-> R Part B ) ) $= + ( wceq wdisjALTV cdm cqs wa wpart eqeq2 anbi2d dfpart2 3bitr4g ) ABDZCEZCFC + GZADZHOPBDZHACIBCINQROABPJKACLBCLM $. + + $( Equality theorem for partition. (Contributed by Peter Mazsa, + 25-Jul-2024.) $) + parteq12 $p |- ( ( R = S /\ A = B ) -> ( R Part A <-> S Part B ) ) $= + ( wceq wpart parteq1 parteq2 sylan9bb ) CDEACFADFABEBDFACDGABDHI $. + + ${ + parteq1i.1 $e |- R = S $. + $( Equality theorem for partition, inference version. (Contributed by + Peter Mazsa, 5-Oct-2021.) $) + parteq1i $p |- ( R Part A <-> S Part A ) $= + ( wceq wpart wb parteq1 ax-mp ) BCEABFACFGDABCHI $. + $} + + ${ + parteq1d.1 $e |- ( ph -> R = S ) $. + $( Equality theorem for partition, deduction version. (Contributed by + Peter Mazsa, 5-Oct-2021.) $) + parteq1d $p |- ( ph -> ( R Part A <-> S Part A ) ) $= + ( wceq wpart wb parteq1 syl ) ACDFBCGBDGHEBCDIJ $. + $} + + $( Property of the partition. (Contributed by Peter Mazsa, 24-Jul-2024.) $) + partsuc2 $p |- ( ( ( R |` ( A u. { A } ) ) \ ( R |` { A } ) ) Part + ( ( A u. { A } ) \ { A } ) <-> + ( R |` A ) Part A ) $= + ( csn cun cres cdif wceq wpart wb ressucdifsn2 sucdifsn2 parteq12 mp2an ) B + AACZDZEBNEFZBAEZGONFZAGRPHAQHIABJAKRAPQLM $. + + $( Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024.) $) + partsuc $p |- + ( ( ( R |` suc A ) \ ( R |` { A } ) ) Part ( suc A \ { A } ) <-> + ( R |` A ) Part A ) $= + ( csuc cres csn cdif wceq wpart wb ressucdifsn sucdifsn parteq12 mp2an ) BA + CZDBAEZDFZBADZGNOFZAGRPHAQHIABJAKRAPQLM $. + +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Partition-Equivalence Theorems +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + ${ + $d R u x y z $. + $( The "Divide et Aequivalere" Theorem: every disjoint relation generates + equivalent cosets by the relation: generalization of the former + ~ prter1 , cf. ~ eldisjim . (Contributed by Peter Mazsa, 3-May-2019.) + (Revised by Peter Mazsa, 17-Sep-2021.) $) + disjim $p |- ( Disj R -> EqvRel ,~ R ) $= + ( vx vy vz vu wdisjALTV cv ccoss wbr wal weqvrel wrel dfdisjALTV4 simplbi + wa wi wmo trcoss syl eqvrelcoss3 sylibr ) AFZBGZCGZAHZIUDDGZUEIOUCUFUEIPD + JCJBJZUEKUBEGUDAIEQCJZUGUBUHALCEAMNBCDEARSBCDATUA $. + $} + + ${ + disjimi.1 $e |- Disj R $. + $( Every disjoint relation generates equivalent cosets by the relation, + inference version. (Contributed by Peter Mazsa, 30-Sep-2021.) $) + disjimi $p |- EqvRel ,~ R $= + ( wdisjALTV ccoss weqvrel disjim ax-mp ) ACADEBAFG $. + $} + + ${ + detlem.1 $e |- Disj R $. + $( If a relation is disjoint, then it is equivalent to the equivalent + cosets of the relation, inference version. (Contributed by Peter Mazsa, + 30-Sep-2021.) $) + detlem $p |- ( Disj R <-> EqvRel ,~ R ) $= + ( wdisjALTV ccoss weqvrel disjim a1i impbii ) ACZADEZAFIJBGH $. + $} + + $( If the elements of ` A ` are disjoint, then it has equivalent coelements + (former ~ prter1 ). Special case of ~ disjim . (Contributed by Rodolfo + Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015) (Revised + by Peter Mazsa, 8-Feb-2018.) ( Revised by Peter Mazsa, 23-Sep-2021.) $) + eldisjim $p |- ( ElDisj A -> CoElEqvRel A ) $= + ( cep ccnv wdisjALTV ccoss weqvrel weldisj wcoeleqvrel disjim df-coeleqvrel + cres df-eldisj 3imtr4i ) BCAKZDNEFAGAHNIALAJM $. + + $( Alternate form of ~ eldisjim . (Contributed by Peter Mazsa, + 30-Dec-2024.) $) + eldisjim2 $p |- ( ElDisj A -> EqvRel ~ A ) $= + ( cep ccnv wdisjALTV ccoss weqvrel weldisj ccoels disjim df-eldisj df-coels + cres eqvreleqi 3imtr4i ) BCALZDOEZFAGAHZFOIAJQPAKMN $. + + $( The null class is an equivalence relation. (Contributed by Peter Mazsa, + 31-Dec-2021.) $) + eqvrel0 $p |- EqvRel (/) $= + ( c0 ccoss weqvrel disjALTV0 disjimi coss0 eqvreleqi mpbi ) ABZCACADEIAFGH + $. + + $( The cosets by the null class are in equivalence relation if and only if + the null class is disjoint (which it is, see ~ disjALTV0 ). (Contributed + by Peter Mazsa, 31-Dec-2021.) $) + det0 $p |- ( Disj (/) <-> EqvRel ,~ (/) ) $= + ( c0 disjALTV0 detlem ) ABC $. + + $( The cosets by the null class are in equivalence relation. (Contributed by + Peter Mazsa, 31-Dec-2024.) $) + eqvrelcoss0 $p |- EqvRel ,~ (/) $= + ( c0 disjALTV0 disjimi ) ABC $. + + $( The identity relation is an equivalence relation. (Contributed by Peter + Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 31-Dec-2021.) $) + eqvrelid $p |- EqvRel _I $= + ( cid ccoss weqvrel disjALTVid disjimi cossid eqvreleqi mpbi ) ABZCACADEIAF + GH $. + + $( The cosets by a restricted identity relation is an equivalence relation. + (Contributed by Peter Mazsa, 31-Dec-2021.) $) + eqvrel1cossidres $p |- EqvRel ,~ ( _I |` A ) $= + ( cid cres disjALTVidres disjimi ) BACADE $. + + $( The cosets by an intersection with a restricted identity relation are in + equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021.) $) + eqvrel1cossinidres $p |- EqvRel ,~ ( R i^i ( _I |` A ) ) $= + ( cid cres cin disjALTVinidres disjimi ) BCADEABFG $. + + $( The cosets by a tail Cartesian product with a restricted identity relation + are in equivalence relation. (Contributed by Peter Mazsa, + 31-Dec-2021.) $) + eqvrel1cossxrnidres $p |- EqvRel ,~ ( R |X. ( _I |` A ) ) $= + ( cid cres cxrn disjALTVxrnidres disjimi ) BCADEABFG $. + + $( The cosets by the identity relation are in equivalence relation if and + only if the identity relation is disjoint. (Contributed by Peter Mazsa, + 31-Dec-2021.) $) + detid $p |- ( Disj _I <-> EqvRel ,~ _I ) $= + ( cid disjALTVid detlem ) ABC $. + + $( The cosets by the identity class are in equivalence relation. + (Contributed by Peter Mazsa, 31-Dec-2024.) $) + eqvrelcossid $p |- EqvRel ,~ _I $= + ( cid disjALTVid disjimi ) ABC $. + + $( The cosets by the restricted identity relation are in equivalence relation + if and only if the restricted identity relation is disjoint. (Contributed + by Peter Mazsa, 31-Dec-2021.) $) + detidres $p |- ( Disj ( _I |` A ) <-> EqvRel ,~ ( _I |` A ) ) $= + ( cid cres disjALTVidres detlem ) BACADE $. + + $( The cosets by the intersection with the restricted identity relation are + in equivalence relation if and only if the intersection with the + restricted identity relation is disjoint. (Contributed by Peter Mazsa, + 31-Dec-2021.) $) + detinidres $p |- ( Disj ( R i^i ( _I |` A ) ) <-> + EqvRel ,~ ( R i^i ( _I |` A ) ) ) $= + ( cid cres cin disjALTVinidres detlem ) BCADEABFG $. + + $( The cosets by the tail Cartesian product with the restricted identity + relation are in equivalence relation if and only if the tail Cartesian + product with the restricted identity relation is disjoint. (Contributed + by Peter Mazsa, 31-Dec-2021.) $) + detxrnidres $p |- ( Disj ( R |X. ( _I |` A ) ) <-> + EqvRel ,~ ( R |X. ( _I |` A ) ) ) $= + ( cid cres cxrn disjALTVxrnidres detlem ) BCADEABFG $. + + ${ + $d R x y $. + $( Lemma for ~ disjdmqseq , ~ partim2 and ~ petlem via ~ disjlem17 , + (general version of the former ~ prtlem14 ). (Contributed by Peter + Mazsa, 10-Sep-2021.) $) + disjlem14 $p |- ( Disj R -> + ( ( x e. dom R /\ y e. dom R ) -> + ( ( A e. [ x ] R /\ A e. [ y ] R ) -> + [ x ] R = [ y ] R ) ) ) $= + ( wdisjALTV cv cdm wcel wa wceq cec cin c0 wo wi wral dfdisjALTV5 simplbi + wrel rsp2 syl eceq1 a1d elin nel02 pm2.21d syl5bir jaoi syl6 ) DEZAFZDGZH + BFZULHIZUKUMJZUKDKZUMDKZLZMJZNZCUPHCUQHIZUPUQJZOZUJUTBULPAULPZUNUTOUJVDDS + BADQRUTABULULTUAUOVCUSUOVBVAUKUMDUBUCVACURHZUSVBCUPUQUDUSVEVBURCUEUFUGUHU + I $. + $} + + ${ + $d A y $. $d B y $. $d R x y $. + $( Lemma for ~ disjdmqseq , ~ partim2 and ~ petlem via ~ disjlem18 , + (general version of the former ~ prtlem17 ). (Contributed by Peter + Mazsa, 10-Sep-2021.) $) + disjlem17 $p |- ( Disj R -> + ( ( x e. dom R /\ A e. [ x ] R ) -> + ( E. y e. dom R ( A e. [ y ] R /\ B e. [ y ] R ) -> + B e. [ x ] R ) ) ) $= + ( wdisjALTV cv cdm wcel cec wa wrex wi df-rex an32 wceq disjlem14 biimprd + wex eleq2 syl8 exp4a impd syl5bir expd imp5a imp4b exlimdv syl5bi ex ) EF + ZAGZEHZIZCULEJZIZKZCBGZEJZIZDUSIZKZBUMLZDUOIZMVCURUMIZVBKZBSUKUQKZVDVBBUM + NVGVFVDBUKUQVEVBVDUKUQVEUTVAVDUKUQVEUTVAVDMZMZUQVEKUNVEKZUPKUKVIUNVEUPOUK + VJUPVIUKVJUPUTVHUKVJUPUTKUOUSPZVHABCEQVKVDVAUOUSDTRUAUBUCUDUEUFUGUHUIUJ + $. + $} + + ${ + $d A x y $. $d B x y $. $d R x y $. $d V x y $. $d W x y $. + $( Lemma for ~ disjdmqseq , ~ partim2 and ~ petlem via ~ disjlem19 , + (general version of the former ~ prtlem18 ). (Contributed by Peter + Mazsa, 16-Sep-2021.) $) + disjlem18 $p |- ( ( A e. V /\ B e. W ) -> + ( Disj R -> + ( ( x e. dom R /\ A e. [ x ] R ) -> + ( B e. [ x ] R <-> A ,~ R B ) ) ) ) $= + ( vy wcel wa wdisjALTV cv cec wb wi wrex adantl relbrcoss impel sylibrd + ex cdm ccoss wbr rspe expr wrel disjrel adantr disjlem17 imbi1d impbidd ) + BEHCFHIZDJZAKZDUAZHZBUNDLZHZIZCUQHZBCDUBUCZMNULUMIZUSUTVAVBUSUTVANVBUSIUT + URUTIZAUOOZVAUSUTVDNVBUPURUTVDVCAUOUDUEPVBVAVDMZUSULDUFZVEUMABCDEFQDUGZRU + HSTVBUSBGKDLZHCVHHIGUOOZUTNZVAUTNUMUSVJNULAGBCDUIPVBVAVIUTULVFVAVIMUMGBCD + EFQVGRUJSUKT $. + $} + + ${ + $d A x z $. $d R x z $. $d V x z $. + $( Lemma for ~ disjdmqseq , ~ partim2 and ~ petlem via ~ disjdmqs , + (general version of the former ~ prtlem19 ). (Contributed by Peter + Mazsa, 16-Sep-2021.) $) + disjlem19 $p |- ( A e. V -> + ( Disj R -> + ( ( x e. dom R /\ A e. [ x ] R ) -> + [ x ] R = [ A ] ,~ R ) ) ) $= + ( vz wcel wdisjALTV cv cdm cec wa ccoss wceq wbr wb wi cvv disjlem18 elvd + imp31 elecALTV ad2antrr bitr4d eqrdv exp31 ) BDFZCGZAHZCIFBUHCJZFKZUIBCLZ + JZMUFUGKUJKZEUIULUMEHZUIFZBUNUKNZUNULFZUFUGUJUOUPOZUFUGUJURPPEABUNCDQRSTU + FUQUPOZUGUJUFUSEBUNUKDQUASUBUCUDUE $. + $} + + ${ + $d R u v x $. + $( Lemma for ~ disjdmqseq via ~ disjdmqs . (Contributed by Peter Mazsa, + 16-Sep-2021.) $) + disjdmqsss $p |- ( Disj R -> ( dom R /. R ) C_ ( dom ,~ R /. ,~ R ) ) $= + ( vv vx vu wdisjALTV cdm cqs cv wcel cec wceq wrex wa wb cvv elv syl wral + wi reximi ccoss wrel disjrel releldmqs disjlem19 ralrimivv 2r19.29 sylbid + ex eqtr ancoms syl6 releldmqscoss sylibrd ssrdv ) AEZBAFZAGZAUAZFUSGZUPBH + ZURIZVACHZUSJZKZCDHZAJZLZDUQLZVAUTIZUPVBVGVDKZVAVGKZMZCVGLZDUQLZVIUPVBVLC + VGLDUQLZVOUPAUBZVBVPNZAUCZVQVRSBCDVAAOUDPQUPVKCVGRDUQRZVPVOSUPVKDCUQVGUPV + FUQIVCVGIMVKSSCDVCAOUEPUFVTVPVOVKVLDCUQVGUGUIQUHVNVHDUQVMVECVGVLVKVEVAVGV + DUJUKTTULUPVQVJVINZVSVQWASBCDVAAOUMPQUNUO $. + $} + + ${ + $d R u v x $. + $( Lemma for ~ disjdmqseq via ~ disjdmqs . (Contributed by Peter Mazsa, + 16-Sep-2021.) $) + disjdmqscossss $p |- ( Disj R -> + ( dom ,~ R /. ,~ R ) C_ ( dom R /. R ) ) $= + ( vv vu vx cv cdm cqs wcel cab cec wceq wrex cvv elv syl wral reximi syl6 + wa wi wdisjALTV wrel wb disjrel releldmqscoss disjlem19 ralrimivv 2r19.29 + ccoss ex sylbid eqtr3 wex df-rex 19.41v bitri simprbi eqcom rexbii syl6ib + ss2abdv abid1 df-qs 3sstr4g ) AUAZBEZAUIZFVGGZHZBIVFCEZAJZKZCAFZLZBIVHVMA + GVEVIVNBVEVIVKVFKZCVMLZVNVEVIVODVKLZCVMLZVPVEVIVKDEZVGJZKZVFVTKZSZDVKLZCV + MLZVRVEVIWBDVKLCVMLZWEVEAUBZVIWFUCZAUDWGWHTBDCVFAMUENOVEWADVKPCVMPZWFWETV + EWACDVMVKVEVJVMHVSVKHZSWATTDCVSAMUFNUGWIWFWEWAWBCDVMVKUHUJOUKWDVQCVMWCVOD + VKVKVFVTULQQRVQVOCVMVQWJDUMZVOVQWJVOSDUMWKVOSVODVKUNWJVODUOUPUQQRVOVLCVMV + KVFURUSUTVABVHVBCBVMAVCVD $. + $} + + $( If a relation is disjoint, its domain quotient is equal to the domain + quotient of the cosets by it. Lemma for ~ partim2 and ~ petlem via + ~ disjdmqseq . (Contributed by Peter Mazsa, 16-Sep-2021.) $) + disjdmqs $p |- ( Disj R -> ( dom R /. R ) = ( dom ,~ R /. ,~ R ) ) $= + ( wdisjALTV cdm cqs ccoss disjdmqsss disjdmqscossss eqssd ) ABACADAEZCIDAFA + GH $. + + $( If a relation is disjoint, its domain quotient is equal to a class if and + only if the domain quotient of the cosets by it is equal to the class. + General version of ~ eldisjn0el (which is the closest theorem to the + former ~ prter2 ). Lemma for ~ partim2 and ~ petlem . (Contributed by + Peter Mazsa, 16-Sep-2021.) $) + disjdmqseq $p |- ( Disj R -> + ( ( dom R /. R ) = A <-> ( dom ,~ R /. ,~ R ) = A ) ) $= + ( wdisjALTV cdm cqs ccoss disjdmqs eqeq1d ) BCBDBEBFZDIEABGH $. + + $( Special case of ~ disjdmqseq (perhaps this is the closest theorem to the + former ~ prter2 ). (Contributed by Peter Mazsa, 26-Sep-2021.) $) + eldisjn0el $p |- ( ElDisj A -> + ( -. (/) e. A <-> ( U. A /. ~ A ) = A ) ) $= + ( cep ccnv cres wdisjALTV cdm cqs wceq ccoss wb weldisj c0 wcel cuni ccoels + wn disjdmqseq df-eldisj n0el3 dmqs1cosscnvepreseq bicomi bibi12i 3imtr4i ) + BCADZEUDFUDGAHZUDIZFUFGAHZJAKLAMPZANAOGAHZJAUDQARUHUEUIUGASUGUIATUAUBUC $. + + $( Disjoint relation on its natural domain implies an equivalence relation on + the cosets of the relation, on its natural domain, cf. ~ partim . Lemma + for ~ petlem . (Contributed by Peter Mazsa, 17-Sep-2021.) $) + partim2 $p |- ( ( Disj R /\ ( dom R /. R ) = A ) -> + ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) ) $= + ( wdisjALTV cdm cqs wceq ccoss weqvrel disjim adantr disjdmqseq biimpa jca + wa ) BCZBDBEAFZNBGZHZQDQEAFZORPBIJOPSABKLM $. + + $( Partition implies equivalence relation by the cosets of the relation on + its natural domain, cf. ~ partim2 . (Contributed by Peter Mazsa, + 17-Sep-2021.) $) + partim $p |- ( R Part A -> ,~ R ErALTV A ) $= + ( wdisjALTV cdm cqs wceq wa ccoss weqvrel werALTV partim2 dfpart2 dferALTV2 + wpart 3imtr4i ) BCBDBEAFGBHZIPDPEAFGABNAPJABKABLAPMO $. + + $( Partition implies that the class of coelements on the natural domain is + equal to the class of cosets of the relation, cf. ~ erimeq . (Contributed + by Peter Mazsa, 25-Dec-2024.) $) + partimeq $p |- ( R e. V -> ( R Part A -> ~ A = ,~ R ) ) $= + ( wcel ccoss cvv wpart werALTV ccoels wceq cossex partim erimeq syl2im ) BC + DBEZFDABGAOHAIOJBCKABLAOFMN $. + + ${ + $d A u $. $d B u $. $d V u $. + $( Special case of ~ disjlem19 (together with ~ membpartlem19 , this is + former ~ prtlem19 ). (Contributed by Peter Mazsa, 21-Oct-2021.) $) + eldisjlem19 $p |- ( B e. V -> + ( ElDisj A -> + ( ( u e. dom ( `' _E |` A ) /\ B e. u ) -> + u = [ B ] ~ A ) ) ) $= + ( wcel weldisj cv cep ccnv cres cdm wa ccoels cec wceq wi ccoss wdisjALTV + df-eldisj disjlem19 syl5bi imp expdimp wb eccnvepres3 eleq2d eqeq1d mpbid + imbi12d adantl df-coels eceq2i eqeq2i syl6ibr expimpd ex ) CDEZBFZAGZHIBJ + ZKEZCUSEZLUSCBMZNZOZPUQURLZVAVBVEVFVALZVBUSCUTQZNZOZVEVGCUSUTNZEZVKVIOZPZ + VBVJPZVFVAVLVMUQURVAVLLVMPZURUTRUQVPBSACUTDTUAUBUCVAVNVOUDVFVAVLVBVMVJVAV + KUSCBUSUEZUFVAVKUSVIVQUGUIUJUHVDVIUSVCVHCBUKULUMUNUOUP $. + $} + + ${ + $d A u $. $d B u $. $d V u $. + $( Together with ~ disjlem19 , this is former ~ prtlem19 . (Contributed by + Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) + (Revised by Peter Mazsa, 21-Oct-2021.) $) + membpartlem19 $p |- ( B e. V -> + ( MembPart A -> + ( ( u e. A /\ B e. u ) -> + u = [ B ] ~ A ) ) ) $= + ( wcel wmembpart cv wa ccoels cec wceq wi weldisj c0 dfmembpart2 cep ccnv + wn cres cdm n0el2 biimpi ad2antll eleq2d eldisjlem19 adantrd expd sylbird + imp sylan2b impd ex ) CDEZBFZAGZBEZCUOEZHUOCBIJKZLUMUNHUPUQURUNUMBMZNBERZ + HZUPUQURLZLBOUMVAHZUPUOPQBSTZEZVBVCVDBUOUTVDBKZUMUSUTVFBUAUBUCUDVCVEUQURU + MVAVEUQHURLZUMUSVGUTABCDUEUFUIUGUHUJUKUL $. + $} + + ${ + petlem.1 $e |- ( ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) -> + Disj R ) $. + $( If you can prove that the equivalence of cosets on their natural domain + implies disjointness (e.g. ~ eqvrelqseqdisj5 ), or converse function + (cf. ~ dfdisjALTV ), then disjointness, and equivalence of cosets, both + on their natural domain, are equivalent. Lemma for the Partition + Equivalence Theorem ~ pet2 . (Contributed by Peter Mazsa, + 18-Sep-2021.) $) + petlem $p |- ( ( Disj R /\ ( dom R /. R ) = A ) <-> + ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) ) $= + ( wdisjALTV cdm wceq wa ccoss weqvrel partim2 disjdmqseq pm5.32i sylanbrc + cqs simpr impbii ) BDZBEBNAFZGZBHZIZTETNAFZGZABJUCQUBSCUAUBOQRUBABKLMP $. + $} + + ${ + petlemi.1 $e |- Disj R $. + $( If you can prove disjointness (e.g. ~ disjALTV0 , ~ disjALTVid , + ~ disjALTVidres , ~ disjALTVxrnidres , search for theorems containing + the ' |- Disj ' string), or the same with converse function (cf. + ~ dfdisjALTV ), then disjointness, and equivalence of cosets, both on + their natural domain, are equivalent. (Contributed by Peter Mazsa, + 18-Sep-2021.) $) + petlemi $p |- ( ( Disj R /\ ( dom R /. R ) = A ) <-> + ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) ) $= + ( wdisjALTV ccoss weqvrel cdm cqs wceq wa a1i petlem ) ABBDBEZFMGMHAIJCKL + $. + $} + + $( Class ` A ` is a partition by the null class if and only if the cosets by + the null class are in equivalence relation on it. (Contributed by Peter + Mazsa, 31-Dec-2021.) $) + pet02 $p |- ( ( Disj (/) /\ ( dom (/) /. (/) ) = A ) <-> + ( EqvRel ,~ (/) /\ ( dom ,~ (/) /. ,~ (/) ) = A ) ) $= + ( c0 disjALTV0 petlemi ) ABCD $. + + $( Class ` A ` is a partition by the null class if and only if the cosets by + the null class are in equivalence relation on it. (Contributed by Peter + Mazsa, 31-Dec-2021.) $) + pet0 $p |- ( (/) Part A <-> ,~ (/) ErALTV A ) $= + ( c0 wdisjALTV cdm wceq ccoss weqvrel wpart werALTV pet02 dfpart2 dferALTV2 + cqs wa 3bitr4i ) BCBDBMAENBFZGPDPMAENABHAPIAJABKAPLO $. + + $( Class ` A ` is a partition by the identity class if and only if the cosets + by the identity class are in equivalence relation on it. (Contributed by + Peter Mazsa, 31-Dec-2021.) $) + petid2 $p |- ( ( Disj _I /\ ( dom _I /. _I ) = A ) <-> + ( EqvRel ,~ _I /\ ( dom ,~ _I /. ,~ _I ) = A ) ) $= + ( cid disjALTVid petlemi ) ABCD $. + + $( A class is a partition by the identity class if and only if the cosets by + the identity class are in equivalence relation on it. (Contributed by + Peter Mazsa, 31-Dec-2021.) $) + petid $p |- ( _I Part A <-> ,~ _I ErALTV A ) $= + ( cid wdisjALTV cdm cqs wceq ccoss weqvrel werALTV petid2 dfpart2 dferALTV2 + wa wpart 3bitr4i ) BCBDBEAFMBGZHPDPEAFMABNAPIAJABKAPLO $. + + $( Class ` A ` is a partition by the identity class restricted to it if and + only if the cosets by the restricted identity class are in equivalence + relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.) $) + petidres2 $p |- ( ( Disj ( _I |` A ) /\ + ( dom ( _I |` A ) /. ( _I |` A ) ) = A ) <-> + ( EqvRel ,~ ( _I |` A ) /\ + ( dom ,~ ( _I |` A ) /. ,~ ( _I |` A ) ) = A ) ) $= + ( cid cres disjALTVidres petlemi ) ABACADE $. + + $( A class is a partition by identity class restricted to it if and only if + the cosets by the restricted identity class are in equivalence relation on + it, cf. ~ eqvrel1cossidres . (Contributed by Peter Mazsa, + 31-Dec-2021.) $) + petidres $p |- ( ( _I |` A ) Part A <-> ,~ ( _I |` A ) ErALTV A ) $= + ( cid cres wdisjALTV cdm wceq ccoss weqvrel wpart werALTV petidres2 dfpart2 + cqs wa dferALTV2 3bitr4i ) BACZDQEQMAFNQGZHRERMAFNAQIARJAKAQLAROP $. + + $( Class ` A ` is a partition by an intersection with the identity class + restricted to it if and only if the cosets by the intersection are in + equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.) $) + petinidres2 $p |- ( ( Disj ( R i^i ( _I |` A ) ) /\ + ( dom ( R i^i ( _I |` A ) ) /. + ( R i^i ( _I |` A ) ) ) = A ) <-> + ( EqvRel ,~ ( R i^i ( _I |` A ) ) /\ + ( dom ,~ ( R i^i ( _I |` A ) ) /. + ,~ ( R i^i ( _I |` A ) ) ) = A ) ) $= + ( cid cres cin disjALTVinidres petlemi ) ABCADEABFG $. + + $( A class is a partition by an intersection with the identity class + restricted to it if and only if the cosets by the intersection are in + equivalence relation on it. Cf. ~ br1cossinidres , ~ disjALTVinidres and + ~ eqvrel1cossinidres . (Contributed by Peter Mazsa, 31-Dec-2021.) $) + petinidres $p |- ( ( R i^i ( _I |` A ) ) Part A <-> + ,~ ( R i^i ( _I |` A ) ) ErALTV A ) $= + ( cid cres cin wdisjALTV cdm cqs wa ccoss weqvrel wpart werALTV petinidres2 + wceq dfpart2 dferALTV2 3bitr4i ) BCADEZFSGSHAOISJZKTGTHAOIASLATMABNASPATQR + $. + + $( Class ` A ` is a partition by a tail Cartesian product with the identity + class restricted to it if and only if the cosets by the tail Cartesian + product are in equivalence relation on it. (Contributed by Peter Mazsa, + 31-Dec-2021.) $) + petxrnidres2 $p |- ( ( Disj ( R |X. ( _I |` A ) ) /\ + ( dom ( R |X. ( _I |` A ) ) /. + ( R |X. ( _I |` A ) ) ) = A ) <-> + ( EqvRel ,~ ( R |X. ( _I |` A ) ) /\ + ( dom ,~ ( R |X. ( _I |` A ) ) /. + ,~ ( R |X. ( _I |` A ) ) ) = A ) ) $= + ( cid cres cxrn disjALTVxrnidres petlemi ) ABCADEABFG $. + + $( A class is a partition by a tail Cartesian product with the identity class + restricted to it if and only if the cosets by the tail Cartesian product + are in equivalence relation on it. Cf. ~ br1cossxrnidres , + ~ disjALTVxrnidres and ~ eqvrel1cossxrnidres . (Contributed by Peter + Mazsa, 31-Dec-2021.) $) + petxrnidres $p |- ( ( R |X. ( _I |` A ) ) Part A <-> + ,~ ( R |X. ( _I |` A ) ) ErALTV A ) $= + ( cid cres cxrn wdisjALTV cdm wceq ccoss weqvrel wpart werALTV petxrnidres2 + cqs wa dfpart2 dferALTV2 3bitr4i ) BCADEZFSGSNAHOSIZJTGTNAHOASKATLABMASPATQ + R $. + + ${ + $d A y $. $d R x y $. + $( The elements of the quotient set of an equivalence relation are disjoint + (cf. ~ eqvreldisj2 , ~ eqvreldisj3 ). (Contributed by Mario Carneiro, + 10-Dec-2016.) (Revised by Peter Mazsa, 3-Dec-2024.) $) + eqvreldisj1 $p |- ( EqvRel R -> + A. x e. ( A /. R ) A. y e. ( A /. R ) + ( x = y \/ ( x i^i y ) = (/) ) ) $= + ( weqvrel cv wceq cin c0 wo cqs simpl simprl simprr qsdisjALTV ralrimivva + wcel wa ) DEZAFZBFZGTUAHIGJABCDKZUBSTUBQZUAUBQZRZRCTUADSUELSUCUDMSUCUDNOP + $. + $} + + ${ + $d A x y $. $d R x y $. + $( The elements of the quotient set of an equivalence relation are disjoint + (cf. ~ eqvreldisj3 ). (Contributed by Mario Carneiro, 10-Dec-2016.) + (Revised by Peter Mazsa, 19-Sep-2021.) $) + eqvreldisj2 $p |- ( EqvRel R -> ElDisj ( A /. R ) ) $= + ( vx vy weqvrel cv wceq cin cqs wral weldisj eqvreldisj1 dfeldisj5 sylibr + c0 wo ) BECFZDFZGQRHOGPDABIZJCSJSKCDABLDCSMN $. + $} + + $( The elements of the quotient set of an equivalence relation are disjoint + (cf. ~ qsdisj2 ). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised + by Peter Mazsa, 20-Jun-2019.) (Revised by Peter Mazsa, 19-Sep-2021.) $) + eqvreldisj3 $p |- ( EqvRel R -> Disj ( `' _E |` ( A /. R ) ) ) $= + ( weqvrel cqs weldisj cep ccnv cres wdisjALTV eqvreldisj2 df-eldisj sylib ) + BCABDZEFGMHIABJMKL $. + + $( Intersection with the converse epsilon relation restricted to the quotient + set of an equivalence relation is disjoint. (Contributed by Peter Mazsa, + 30-May-2020.) (Revised by Peter Mazsa, 31-Dec-2021.) $) + eqvreldisj4 $p |- ( EqvRel R -> Disj ( S i^i ( `' _E |` ( B /. R ) ) ) ) $= + ( weqvrel cep ccnv cqs cres wdisjALTV cin eqvreldisj3 disjimin syl ) BDEFAB + GHZICNJIABKCNLM $. + + $( Tail Cartesian product with converse epsilon relation restricted to the + quotient set of an equivalence relation is disjoint. (Contributed by + Peter Mazsa, 30-May-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) $) + eqvreldisj5 $p |- ( EqvRel R -> Disj ( S |X. ( `' _E |` ( B /. R ) ) ) ) $= + ( weqvrel cep ccnv cqs cres wdisjALTV cxrn eqvreldisj3 disjimxrn syl ) BDEF + ABGHZICNJIABKCNLM $. + + $( Implication of ~ eqvreldisj2 , lemma for The Main Theorem of Equivalences + ~ mainer . (Contributed by Peter Mazsa, 23-Sep-2021.) $) + eqvrelqseqdisj2 $p |- ( ( EqvRel R /\ ( B /. R ) = A ) -> ElDisj A ) $= + ( weqvrel cqs wceq wa weldisj eqvreldisj2 adantr wb eldisjeq adantl mpbid ) + CDZBCEZAFZGPHZAHZORQBCIJQRSKOPALMN $. + + $( Implication of ~ eqvrelqseqdisj2 and ~ n0eldmqseq , see comment of + ~ fences . (Contributed by Peter Mazsa, 30-Dec-2024.) $) + fences3 $p |- ( ( EqvRel R /\ ( dom R /. R ) = A ) -> + ( ElDisj A /\ -. (/) e. A ) ) $= + ( weqvrel cdm cqs wceq wa weldisj c0 wcel eqvrelqseqdisj2 n0eldmqseq adantl + wn jca ) BCZBDZBEAFZGAHIAJNZAQBKRSPABLMO $. + + $( Implication of ~ eqvreldisj3 , lemma for the Member Partition Equivalence + Theorem ~ mpet3 . (Contributed by Peter Mazsa, 27-Oct-2020.) (Revised by + Peter Mazsa, 24-Sep-2021.) $) + eqvrelqseqdisj3 $p |- ( ( EqvRel R /\ ( B /. R ) = A ) -> + Disj ( `' _E |` A ) ) $= + ( weqvrel cqs wceq wa cep ccnv cres wdisjALTV eqvreldisj3 adantr wb disjeqd + reseq2 adantl mpbid ) CDZBCEZAFZGHIZTJZKZUBAJZKZSUDUABCLMUAUDUFNSUAUCUETAUB + POQR $. + + $( Lemma for ~ petincnvepres2 . (Contributed by Peter Mazsa, + 31-Dec-2021.) $) + eqvrelqseqdisj4 $p |- ( ( EqvRel R /\ ( B /. R ) = A ) -> + Disj ( S i^i ( `' _E |` A ) ) ) $= + ( weqvrel cqs wceq cep ccnv cres wdisjALTV cin eqvrelqseqdisj3 disjimin syl + wa ) CEBCFAGPHIAJZKDQLKABCMDQNO $. + + $( Lemma for the Partition-Equivalence Theorem ~ pet2 . (Contributed by + Peter Mazsa, 15-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) $) + eqvrelqseqdisj5 $p |- ( ( EqvRel R /\ ( B /. R ) = A ) -> + Disj ( S |X. ( `' _E |` A ) ) ) $= + ( weqvrel cqs wceq wa cep ccnv cres wdisjALTV eqvrelqseqdisj3 disjimxrn syl + cxrn ) CEBCFAGHIJAKZLDQPLABCMDQNO $. + + $( The Main Theorem of Equivalences: every equivalence relation implies + equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021.) $) + mainer $p |- ( R ErALTV A -> CoMembEr A ) $= + ( weqvrel cdm cqs wceq wa wcoeleqvrel cuni ccoels werALTV wcomember weldisj + eqvrelqseqdisj2 eldisjim syl c0 wcel wn n0eldmqseq adantl wb eldisjn0el jca + mpbid dferALTV2 dfcomember3 3imtr4i ) BCZBDZBEAFZGZAHZAIAJEAFZGABKALULUMUNU + LAMZUMAUJBNZAOPULQARSZUNUKUQUIABTUAULUOUQUNUBUPAUCPUEUDABUFAUGUH $. + + $( Partition with general ` R ` (in addition to the member partition cf. + ~ mpet and ~ mpet2 ) implies equivalent comembers. (Contributed by Peter + Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.) $) + partimcomember $p |- ( R Part A -> CoMembEr A ) $= + ( wpart ccoss werALTV wcomember partim mainer syl ) ABCABDZEAFABGAJHI $. + + $( Member Partition-Equivalence Theorem. Together with ~ mpet ~ mpet2 , + mostly in its conventional ~ cpet and ~ cpet2 form, this is what we used + to think of as the partition equivalence theorem (but cf. ~ pet2 with + general ` R ` ). (Contributed by Peter Mazsa, 4-May-2018.) (Revised by + Peter Mazsa, 26-Sep-2021.) $) + mpet3 $p |- ( ( ElDisj A /\ -. (/) e. A ) <-> + ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) $= + ( weldisj c0 wcel wn cep ccnv cres wdisjALTV cdm cqs wceq ccoss wcoeleqvrel + wa weqvrel cuni ccoels eldisjn0elb eqvrelqseqdisj3 petlem eqvreldmqs 3bitri + ) ABCADEOFGAHZIUDJUDKALOUDMZPUEJZUEKALOANAQARKALOASAUDAUFUETUAAUBUC $. + + $( The conventional form of the Member Partition-Equivalence Theorem. In the + conventional case there is no (general) disjoint and no (general) + partition concept: mathematicians have called disjoint or partition what + we call element disjoint or member partition, see also ~ cpet . Together + with ~ cpet , ~ mpet ~ mpet2 , this is what we used to think of as the + partition equivalence theorem (but cf. ~ pet2 with general ` R ` ). + (Contributed by Peter Mazsa, 30-Dec-2024.) $) + cpet2 $p |- ( ( ElDisj A /\ -. (/) e. A ) <-> + ( EqvRel ~ A /\ ( U. A /. ~ A ) = A ) ) $= + ( weldisj c0 wcel wn wa cep ccnv cres wdisjALTV cdm cqs wceq weqvrel ccoels + ccoss cuni eldisjn0elb eqvrelqseqdisj3 petlem eqvreldmqs2 3bitri ) ABCADEFG + HAIZJUCKUCLAMFUCPZNUDKZUDLAMFAOZNAQUFLAMFARAUCAUEUDSTAUAUB $. + + $( The conventional form of Member Partition-Equivalence Theorem. In the + conventional case there is no (general) disjoint and no (general) + partition concept: mathematicians have been calling disjoint or partition + what we call element disjoint or member partition, see also ~ cpet2 . Cf. + ~ mpet , ~ mpet2 and ~ mpet3 for unconventional forms of Member + Partition-Equivalence Theorem. Cf. ~ pet and ~ pet2 for + Partition-Equivalence Theorem with general ` R ` . (Contributed by Peter + Mazsa, 31-Dec-2024.) $) + cpet $p |- ( MembPart A <-> + ( EqvRel ~ A /\ ( U. A /. ~ A ) = A ) ) $= + ( wmembpart weldisj c0 wcel wn wa ccoels weqvrel cuni cqs dfmembpart2 cpet2 + wceq bitri ) ABACDAEFGAHZIAJPKANGALAMO $. + + $( Member Partition-Equivalence Theorem in almost its shortest possible form, + cf. the 0-ary version ~ mpets . Member partition and comember equivalence + relation are the same (or: each element of ` A ` have equivalent comembers + if and only if ` A ` is a member partition). Together with ~ mpet2 , + ~ mpet3 , and with the conventional ~ cpet and ~ cpet2 , this is what we + used to think of as the partition equivalence theorem (but cf. ~ pet2 with + general ` R ` ). (Contributed by Peter Mazsa, 24-Sep-2021.) $) + mpet $p |- ( MembPart A <-> CoMembEr A ) $= + ( weldisj c0 wcel wn wcoeleqvrel cuni ccoels wceq wmembpart wcomember mpet3 + wa cqs dfmembpart2 dfcomember3 3bitr4i ) ABCADEMAFAGAHNAIMAJAKALAOAPQ $. + + $( Member Partition-Equivalence Theorem in a shorter form. Together with + ~ mpet ~ mpet3 , mostly in its conventional ~ cpet and ~ cpet2 form, this + is what we used to think of as the partition equivalence theorem (but cf. + ~ pet2 with general ` R ` ). (Contributed by Peter Mazsa, + 24-Sep-2021.) $) + mpet2 $p |- ( ( `' _E |` A ) Part A <-> ,~ ( `' _E |` A ) ErALTV A ) $= + ( wmembpart wcomember ccnv cres wpart ccoss werALTV df-membpart df-comember + cep mpet 3bitr3i ) ABACAKDAEZFANGHALAIAJM $. + + $( Member Partition-Equivalence Theorem with binary relations, cf. ~ mpet2 . + (Contributed by Peter Mazsa, 24-Sep-2021.) $) + mpets2 $p |- ( A e. V -> + ( ( `' _E |` A ) Parts A <-> ,~ ( `' _E |` A ) Ers A ) ) $= + ( wcel cep ccnv cres cparts wbr ccoss wb wpart werALTV mpet2 cvv cnvepresex + cers brpartspart mpdan 1cosscnvepresex brerser bibi12d mpbiri ) ABCZDEAFZAG + HZUDIZAPHZJAUDKZAUFLZJAMUCUEUHUGUIUCUDNCUEUHJABOAUDBNQRUCUFNCUGUIJABSAUFBNT + RUAUB $. + + $( Member Partition-Equivalence Theorem in its shortest possible form: it + shows that member partitions and comember equivalence relations are + literally the same. Cf. ~ pet , the general Partition-Equivalence + Theorem, with general ` R ` . (Contributed by Peter Mazsa, + 31-Dec-2024.) $) + mpets $p |- MembParts = CoMembErs $= + ( va cep ccnv cv cres cparts wbr ccoss cers cmembparts ccomembers wb mpets2 + cab cvv elv abbii df-membparts df-comembers 3eqtr4i ) BCADZEZUAFGZANUBHUAIG + ZANJKUCUDAUCUDLAUAOMPQARAST $. + + $( Partition with general ` R ` also imply member partition. (Contributed by + Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.) $) + mainpart $p |- ( R Part A -> MembPart A ) $= + ( wpart wcomember wmembpart partimcomember mpet sylibr ) ABCADAEABFAGH $. + + $( The Theorem of Fences by Equivalences: all conceivable equivalence + relations (besides the comember equivalence relation cf. ~ mpet ) generate + a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.) $) + fences $p |- ( R ErALTV A -> MembPart A ) $= + ( werALTV wcomember wmembpart mainer mpet sylibr ) ABCADAEABFAGH $. + + $( The Theorem of Fences by Equivalences: all conceivable equivalence + relations (besides the comember equivalence relation cf. ~ mpet3 ) + generate a partition of the members, it alo means that + ` ( R ErALTV A -> ElDisj A ) ` and that + ` ( R ErALTV A -> -. (/) e. A ) ` . (Contributed by Peter Mazsa, + 15-Oct-2021.) $) + fences2 $p |- ( R ErALTV A -> ( ElDisj A /\ -. (/) e. A ) ) $= + ( werALTV wmembpart weldisj c0 wcel wn wa fences dfmembpart2 sylib ) ABCADA + EFAGHIABJAKL $. + + $( The Main Theorem of Equivalences: every equivalence relation implies + equivalent comembers. (Contributed by Peter Mazsa, 15-Oct-2021.) $) + mainer2 $p |- ( R ErALTV A -> ( CoElEqvRel A /\ -. (/) e. A ) ) $= + ( werALTV weldisj c0 wcel wn wa wcoeleqvrel fences2 eldisjim anim1i syl ) A + BCADZEAFGZHAIZOHABJNPOAKLM $. + + $( Every equivalence relation implies equivalent coelements. (Contributed by + Peter Mazsa, 20-Oct-2021.) $) + mainerim $p |- ( R ErALTV A -> CoElEqvRel A ) $= + ( werALTV wcoeleqvrel c0 wcel wn mainer2 simpld ) ABCADEAFGABHI $. + + $( A partition-equivalence theorem with intersection and general ` R ` . + (Contributed by Peter Mazsa, 31-Dec-2021.) $) + petincnvepres2 $p |- ( ( Disj ( R i^i ( `' _E |` A ) ) /\ + ( dom ( R i^i ( `' _E |` A ) ) /. + ( R i^i ( `' _E |` A ) ) ) = A ) <-> + ( EqvRel ,~ ( R i^i ( `' _E |` A ) ) /\ + ( dom ,~ ( R i^i ( `' _E |` A ) ) /. + ,~ ( R i^i ( `' _E |` A ) ) ) = A ) ) $= + ( cep ccnv cres cin ccoss cdm eqvrelqseqdisj4 petlem ) ABCDAEFZAKGZHLBIJ $. + + $( The shortest form of a partition-equivalence theorem with intersection and + general ` R ` . Cf. ~ br1cossincnvepres . Cf. ~ pet . (Contributed by + Peter Mazsa, 23-Sep-2021.) $) + petincnvepres $p |- ( ( R i^i ( `' _E |` A ) ) Part A <-> + ,~ ( R i^i ( `' _E |` A ) ) ErALTV A ) $= + ( cep ccnv cres cin wdisjALTV cdm cqs wa ccoss weqvrel wpart petincnvepres2 + wceq werALTV dfpart2 dferALTV2 3bitr4i ) BCDAEFZGTHTIAOJTKZLUAHUAIAOJATMAUA + PABNATQAUARS $. + + $( Partition-Equivalence Theorem, with general ` R ` . This theorem + (together with ~ pet and ~ pets ) is the main result of my investigation + into set theory, see the comment of ~ pet . (Contributed by Peter Mazsa, + 24-May-2021.) (Revised by Peter Mazsa, 23-Sep-2021.) $) + pet2 $p |- ( ( Disj ( R |X. ( `' _E |` A ) ) /\ + ( dom ( R |X. ( `' _E |` A ) ) /. + ( R |X. ( `' _E |` A ) ) ) = A ) <-> + ( EqvRel ,~ ( R |X. ( `' _E |` A ) ) /\ + ( dom ,~ ( R |X. ( `' _E |` A ) ) /. + ,~ ( R |X. ( `' _E |` A ) ) ) = A ) ) $= + ( cep ccnv cres cxrn ccoss cdm eqvrelqseqdisj5 petlem ) ABCDAEFZAKGZHLBIJ + $. + + $( Partition-Equivalence Theorem with general ` R ` while preserving the + restricted converse epsilon relation of ~ mpet2 (as opposed to + ~ petincnvepres ). A class is a partition by a tail Cartesian product + with general ` R ` and the restricted converse element class if and only + if the cosets by the tail Cartesian product are in an equivalence relation + on it. Cf. ~ br1cossxrncnvepres . + + This theorem (together with ~ pets and ~ pet2 ) is the main result of my + investigation into set theory. It is no more general than the + conventional Member Partition-Equivalence Theorem ~ mpet , ~ mpet2 and + ~ mpet3 (because you cannot set ` R ` in this theorem in such a way that + you get ~ mpet2 ), i.e., it is not the hypothetical General + Partition-Equivalence Theorem gpet ` |- ( R Part A <-> ,~ R ErALTV A ) ` , + but this one has a general part that ~ mpet2 lacks: ` R ` , which is + sufficient for my future application of set theory, for my purpose outside + of set theory. (Contributed by Peter Mazsa, 23-Sep-2021.) $) + pet $p |- ( ( R |X. ( `' _E |` A ) ) Part A <-> + ,~ ( R |X. ( `' _E |` A ) ) ErALTV A ) $= + ( cep ccnv cres cxrn wdisjALTV cdm wceq wa ccoss weqvrel wpart werALTV pet2 + cqs dfpart2 dferALTV2 3bitr4i ) BCDAEFZGTHTPAIJTKZLUAHUAPAIJATMAUANABOATQAU + ARS $. + + $( Partition-Equivalence Theorem with general ` R ` , with binary relations. + This theorem (together with ~ pet and ~ pet2 ) is the main result of my + investigation into set theory, cf. the comment of ~ pet . (Contributed by + Peter Mazsa, 23-Sep-2021.) $) + pets $p |- ( ( A e. V /\ R e. W ) -> + ( ( R |X. ( `' _E |` A ) ) Parts A <-> + ,~ ( R |X. ( `' _E |` A ) ) Ers A ) ) $= + ( wcel wa cep ccnv cres cxrn cparts wbr ccoss cers wb wpart werALTV pet cvv + syldan xrncnvepresex brpartspart 1cossxrncnvepresex brerser bibi12d mpbiri + ) ACEZBDEZFZBGHAIJZAKLZUJMZANLZOAUJPZAULQZOABRUIUKUNUMUOUGUHUJSEUKUNOABCDUA + AUJCSUBTUGUHULSEUMUOOABCDUCAULCSUDTUEUF $. + $( (End of Peter Mazsa's mathbox.) $) $( End $[ set-mbox-pm.mm $] $)