From bc8cf0046e8533599c3dff9573e8791061aaebd8 Mon Sep 17 00:00:00 2001 From: mazsa Date: Sun, 17 Nov 2024 14:41:37 +0100 Subject: [PATCH] PETs Partition-Equivalence Theorems --- set.mm | 675 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 675 insertions(+) diff --git a/set.mm b/set.mm index ad347a0dbd..667c1b9f9a 100644 --- a/set.mm +++ b/set.mm @@ -560724,6 +560724,681 @@ Membership partition is the conventional meaning of partition (cf. the ( wceq wpart wb parteq1 syl ) ACDFBCGBDGHEBCDIJ $. $} +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Partition-Equivalence Theorems +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + ${ + $d R u x y z $. + $( The Teorem of "Divide et Aequivalere": every disjoint relation generates + equivalent cosets by the relation: generalization of the former + ~ prter1 , cf. ~ mdisjim . (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 $. + $} + + ${ + disjimd.1 $e |- ( ph -> Disj R ) $. + $( Every disjoint relation generates equivalent cosets by the relation, + deduction version. (Contributed by Peter Mazsa, 30-Sep-2021.) $) + disjimd $p |- ( ph -> EqvRel ,~ R ) $= + ( wdisjALTV ccoss weqvrel disjim syl ) ABDBEFCBGH $. + $} + + ${ + detlem.1 $e |- Disj R $. + $( If a relation is disjoint, then it is equivalent to the equivalent + cosets by the relation, inference version. (Contributed by Peter Mazsa, + 30-Sep-2021.) $) + detlem $p |- ( Disj R <-> EqvRel ,~ R ) $= + ( wdisjALTV ccoss weqvrel disjim a1i impbii ) ACZADEZAFIJBGH $. + $} + + ${ + detlemd.1 $e |- ( ph -> Disj R ) $. + $( If a relation is disjoint, then it is equivalent to the equivalent + cosets by the relation, deduction version. (Contributed by Peter Mazsa, + 30-Sep-2021.) $) + detlemd $p |- ( ph -> ( Disj R <-> EqvRel ,~ R ) ) $= + ( wdisjALTV ccoss weqvrel disjim a1d impbid2 ) ABDZBEFZBGAJKCHI $. + $} + + $( 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.) $) + mdisjim $p |- ( ElDisj A -> EqvRel ~ A ) $= + ( cep ccnv wdisjALTV ccoss weqvrel weldisj ccoels disjim df-eldisj df-coels + cres eqvreleqi 3imtr4i ) BCALZDOEZFAGAHZFOIAJQPAKMN $. + + ${ + mdisjimi.1 $e |- ElDisj A $. + $( If the elements of ` A ` are disjoint, then it has equivalent + coelements, inference version. (Contributed by Peter Mazsa, + 30-Sep-2021.) $) + mdisjimi $p |- EqvRel ~ A $= + ( weldisj ccoels weqvrel mdisjim ax-mp ) ACADEBAFG $. + $} + + ${ + mdisjimd.1 $e |- ( ph -> ElDisj A ) $. + $( If the elements of ` A ` are disjoint, then it has equivalent + coelements, deduction version. (Contributed by Peter Mazsa, + 30-Sep-2021.) $) + mdisjimd $p |- ( ph -> EqvRel ~ A ) $= + ( weldisj ccoels weqvrel mdisjim syl ) ABDBEFCBGH $. + $} + + ${ + mdetlemi.1 $e |- ElDisj A $. + $( If the elements of ` A ` are disjoint, then it is equivalent to the + equivalent coelements of it, inference version. (Contributed by Peter + Mazsa, 30-Sep-2021.) $) + mdetlemi $p |- ( ElDisj A <-> EqvRel ~ A ) $= + ( weldisj ccoels weqvrel mdisjim a1i impbii ) ACZADEZAFIJBGH $. + $} + + ${ + mdetlemd.1 $e |- ( ph -> ElDisj A ) $. + $( If the elements of ` A ` are disjoint, then it is equivalent to the + equivalent coelements of it, deduction version. (Contributed by Peter + Mazsa, 30-Sep-2021.) $) + mdetlemd $p |- ( ph -> ( ElDisj A <-> EqvRel ~ A ) ) $= + ( weldisj ccoels weqvrel mdisjim a1d impbid2 ) ABDZBEFZBGAJKCHI $. + $} + + $( 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 is an equivalence relation if and only if the + null class is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.) $) + det0 $p |- ( Disj (/) <-> EqvRel ,~ (/) ) $= + ( c0 disjALTV0 detlem ) ABC $. + + $( 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 is an + 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 + is an 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 is an 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 restricted identity relation is an 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 is an + 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 is an 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 y $. $d A x z $. $d R x y $. $d R x z $. $d V x y $. + $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 disjlem18 elvd imp31 + wi cvv elecALTV ad2antrr bitr4d eqrdv exp31 ) BDFZCGZAHZCIFBUHCJZFKZUIBCL + ZJZMUFUGKUJKZEUIULUMEHZUIFZBUNUKNZUNULFZUFUGUJUOUPOZUFUGUJURSSEABUNCDTPQR + UFUQUPOZUGUJUFUSEBUNUKDTUAQUBUCUDUE $. + $} + + ${ + $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 ancom eqtr sylbi syl6 releldmqscoss sylibrd ssrdv ) AEZBAFZAGZAUAZFUTG + ZUQBHZUSIZVBCHZUTJZKZCDHZAJZLZDURLZVBVAIZUQVCVHVEKZVBVHKZMZCVHLZDURLZVJUQ + VCVMCVHLDURLZVPUQAUBZVCVQNZAUCZVRVSSBCDVBAOUDPQUQVLCVHRDURRZVQVPSUQVLDCUR + VHUQVGURIVDVHIMVLSSCDVDAOUEPUFWAVQVPVLVMDCURVHUGUIQUHVOVIDURVNVFCVHVNVMVL + MVFVLVMUJVBVHVEUKULTTUMUQVRVKVJNZVTVRWBSBCDVBAOUNPQUOUP $. + $} + + ${ + $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 abid2 eqcomi df-qs 3sstr4g ) AUAZBEZAUIZFVHGZHZBIZVGCEZAJZKZCAFZL + ZBIVIVOAGVFVJVPBVFVJVMVGKZCVOLZVPVFVJVQDVMLZCVOLZVRVFVJVMDEZVHJZKZVGWBKZS + ZDVMLZCVOLZVTVFVJWDDVMLCVOLZWGVFAUBZVJWHUCZAUDWIWJTBDCVGAMUENOVFWCDVMPCVO + PZWHWGTVFWCCDVOVMVFVLVOHWAVMHZSWCTTDCWAAMUFNUGWKWHWGWCWDCDVOVMUHUJOUKWFVS + CVOWEVQDVMVMVGWBULQQRVSVQCVOVSWLDUMZVQVSWLVQSDUMWMVQSVQDVMUNWLVQDUOUPUQQR + VQVNCVOVMVGURUSUTVAVKVIBVIVBVCCBVOAVDVE $. + $} + + $( 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 the relation 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 equivalence relation by + 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 wa ccoss weqvrel wpart werALTV partim2 dfpart2 dferALTV2 + wceq 3imtr4i ) BCBDBEANFBGZHPDPEANFABIAPJABKABLAPMO $. + + ${ + $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 cqs wa ccoss weqvrel partim2 simpr jca disjdmqseq pm5.32i + wceq sylibr impbii ) BDZBEBFAOZGZBHZIZUAEUAFAOZGZABJUDRUCGTUDRUCCUBUCKLRS + UCABMNPQ $. + $} + + ${ + 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. Inference version. (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 + $. + $} + + ${ + petlemd.1 $e |- ( ph -> Disj R ) $. + $( If you can prove disjointness (or converse function, cf. ~ dfdisjALTV ), + then disjointness, and equivalence of cosets, both on their natural + domain, are equivalent. Deduction version. (Contributed by Peter + Mazsa, 18-Sep-2021.) $) + petlemd $p |- ( ph -> + ( ( Disj R /\ ( dom R /. R ) = A ) <-> + ( EqvRel ,~ R /\ ( dom ,~ R /. ,~ R ) = A ) ) ) $= + ( wdisjALTV cdm cqs wa ccoss weqvrel partim2 a1d simpr disjdmqseq pm5.32i + wceq jca2 syl6ibr impbid2 ) ACEZCFCGBPZHZCIZJZUCFUCGBPZHZBCKAUFTUEHUBAUFT + UEATUFDLUDUEMQTUAUEBCNORS $. + $} + + $( Class ` A ` is a partition by the null class if and only if the cosets by + the null class is an equivalence relation on it. (Contributed by Peter + Mazsa, 31-Dec-2021.) $) + pet02 $p |- ( ( Disj (/) /\ ( dom (/) /. (/) ) = A ) <-> + ( EqvRel ,~ (/) /\ ( dom ,~ (/) /. ,~ (/) ) = A ) ) $= + ( c0 disjALTV0 petlemi ) ABCD $. + + $( A class is a partition by the null class if and only if the cosets by the + null class is an equivalence relation on it. (Contributed by Peter Mazsa, + 31-Dec-2021.) $) + pet0 $p |- ( (/) Part A <-> ,~ (/) ErALTV A ) $= + ( c0 wdisjALTV cdm cqs wceq wa ccoss weqvrel wpart werALTV dfpart2 dferALTV2 + pet02 3bitr4i ) BCBDBEAFGBHZIPDPEAFGABJAPKANABLAPMO $. + + $( Class ` A ` is a partition by the class of the identity relations if and + only if the cosets by the identity class is an 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 class of the identity relations if and only + if the cosets by the identity class is an equivalence relation on it. + (Contributed by Peter Mazsa, 31-Dec-2021.) $) + petid $p |- ( _I Part A <-> ,~ _I ErALTV A ) $= + ( cid wdisjALTV cdm cqs wceq wa ccoss weqvrel wpart werALTV petid2 dferALTV2 + dfpart2 3bitr4i ) BCBDBEAFGBHZIPDPEAFGABJAPKALABNAPMO $. + + $( Class ` A ` is a partition by the class of the identity relations + restricted to it if and only if the cosets by the restricted identity + class is an 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 the class of the identity relations restricted + to it if and only if the cosets by the restricted identity class is an + 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 class of the + identity relations restricted to it if and only if the cosets by the + intersection is an 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 class of the identity + relations restricted to it if and only if the cosets by the intersection + is an 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 class of + the identity relations restricted to it if and only if the cosets by the + tail Cartesian product is an 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 class of the + identity relations restricted to it if and only if the cosets by the tail + Cartesian product is an 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 ) BCADEZFSGSNAHOSIZJTGTNAHOASKATLABMASPATQR + $. + + ${ + $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 c0 wo cqs wral weldisj wa simpl simprl simprr + wcel qsdisjALTV ralrimivva dfeldisj5 sylibr ) BEZCFZDFZGUDUEHIGJZDABKZLCU + GLUGMUCUFCDUGUGUCUDUGRZUEUGRZNZNAUDUEBUCUJOUCUHUIPUCUHUIQSTDCUGUAUB $. + $} + + $( 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 elements of 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 the elements of 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 ~ eqvreldisj3 , lemma for the Membership 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: 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 wa ccoels werALTV wmember weldisj eqvrelqseqdisj2 mdisjim + wceq cuni syl c0 wcel wn n0eldmqseq adantl wb eldisjn0el mpbid jca dferALTV2 + dfmember3 3imtr4i ) BCZBDZBEAMZFZAGZCZANULEAMZFABHAIUKUMUNUKAJZUMAUIBKZALOU + KPAQRZUNUJUQUHABSTUKUOUQUNUAUPAUBOUCUDABUEAUFUG $. + + $( Membership Partition-Equivalence Theorem. Together with ~ mpet and + ~ mpet2 , this is what is generally identified 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 ) <-> + ( EqvRel ~ A /\ ( U. A /. ~ A ) = A ) ) $= + ( weldisj c0 wcel wn wa cep ccnv cres wdisjALTV cdm cqs wceq weqvrel ccoels + ccoss cuni df-eldisj n0el3 anbi12i eqvrelqseqdisj3 petlem eqvreldmqs + 3bitri ) ABZCADEZFGHAIZJZUGKUGLAMZFUGPZNUJKZUJLAMFAOZNAQULLAMFUEUHUFUIARAST + AUGAUKUJUAUBAUCUD $. + + $( Membership Partition-Equivalence Theorem in its shortest possible form: + membership equivalence relation and membership partition are the same (or: + each element of ` A ` has equivalent members if and only if ` A ` is a + 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 ccoels weqvrel cuni wceq wmembpart wmember dfmembpart2 + wa cqs mpet3 dfmember3 3bitr4i ) ABCADEMAFZGAHRNAIMAJAKAOALAPQ $. + + $( 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 dfmember2 + mpet 3bitr3i ) ABACADEAFZGANHIALAJAKM $. + + $( Membership Partition-Equivalence Theorem with binary relations, cf. + ~ mpet2 . (Contributed by Peter Mazsa, 24-Sep-2021.) $) + mpets $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 ) ABCZDEA + FZAGHZUDIZAPHZJAUDKZAUFLZJAMUCUEUHUGUIUCUDNCUEUHJABOAUDBNQRUCUFNCUGUIJABSAU + FBNTRUAUB $. + + $( The Theorem of Fences by Equivalences: all kinds of equivalence relations + imaginable (in addition to the membership equivalence relation cf. + ~ 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 $. + + $( The Theorem of Fences by Equivalences: all kinds of equivalence relations + imaginable (in addition to the membership equivalence relation cf. + ~ mpet3 ) imply the partition of the members, moreover it implies 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: any equivalence relation implies + equivalent membership as well. (Contributed by Peter Mazsa, + 15-Oct-2021.) $) + mainer2 $p |- ( R ErALTV A -> ( EqvRel ~ A /\ -. (/) e. A ) ) $= + ( werALTV weldisj c0 wcel wn wa ccoels weqvrel fences2 mdisjim anim1i syl ) + ABCADZEAFGZHAIJZPHABKOQPALMN $. + + $( Any equivalence relation implies equivalent coelements as well. + (Contributed by Peter Mazsa, 20-Oct-2021.) $) + mainerim $p |- ( R ErALTV A -> EqvRel ~ A ) $= + ( werALTV ccoels weqvrel c0 wcel wn mainer2 simpld ) ABCADEFAGHABIJ $. + + $( 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 . (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 ) BCDAEFZGTHTIAOJTKZLUAHUAIAOJATMAUAP + ABNATQAUARS $. + + $( Partition-Equivalence Theorem, with general ` R ` . This theorem + (together with ~ pet and ~ pets ) is the main result of my inquiry into + set theory, cf. 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 keeping the + restricted converse epsilon relation of ~ mpet2 (as opposed to + ~ petincnvepres ). + + Cf. ~ br1cossxrncnvepres . + + This theorem (together with ~ pets and ~ pet2 ) is the main result of my + inquiry into set theory. Not more general than the conventional + Membership Partition-Equivalence Theorem ~ mpet , ~ mpet2 and ~ mpet3 + (because you cannot set ` R ` in this theorem in a way that you would get + ~ mpet2 ), i.e., this is not the hypothetical General Partition + Equivalence Theorem gpet ` |- ( R Part A <-> ,~ R ErALTV A ) ` , but this + has a general part that ~ mpet2 lacks: ` R ` , which is enough for my + future application of set theory, for my purpose outside of set theory. + Motto: "Le meglio è l'inimico del bene." (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 ) BCDAEFZGTHTPAIJTKZLUAHUAPAIJATMAUANABOATQAUA + RS $. + + $( 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 + 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 + DAEFGAHAIABJAKL $. + + $( Partition-Equivalence Theorem with general ` R ` , with binary relations. + This theorem (together with ~ pet and ~ pet2 ) is the main result of my + inquiry 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 + syl2anc simpl xrncnvepresex brpartspart 1cossxrncnvepresex bibi12d mpbiri + brerser ) ACEZBDEZFZBGHAIJZAKLZUKMZANLZOAUKPZAUMQZOABRUJULUOUNUPUJUHUKS + EULUOOUHUIUAZABCDUBAUKCSUCTUJUHUMSEUNUPOUQABCDUDAUMCSUGTUEUF $. $( (End of Peter Mazsa's mathbox.) $)