Skip to content

Commit

Permalink
CoElEqvRel
Browse files Browse the repository at this point in the history
  • Loading branch information
@mazsa
mazsa committed Nov 17, 2024
1 parent bc8cf00 commit 38978ff
Showing 1 changed file with 31 additions and 28 deletions.
59 changes: 31 additions & 28 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -560780,44 +560780,44 @@ Membership partition is the conventional meaning of partition (cf. the
(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 $.
mdisjim $p |- ( ElDisj A -> CoElEqvRel A ) $=
( ccnv cres wdisjALTV ccoss weqvrel weldisj wcoeleqvrel df-eldisj
cep disjim df-coeleqvrel 3imtr4i ) JBACZDNEFAGAHNKAIALM $.

${
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 $.
mdisjimi $p |- CoElEqvRel A $=
( weldisj wcoeleqvrel mdisjim ax-mp ) ACADBAEF $.
$}

${
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 $.
mdisjimd $p |- ( ph -> CoElEqvRel A ) $=
( weldisj wcoeleqvrel mdisjim syl ) ABDBECBFG $.
$}

${
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 $.
mdetlemi $p |- ( ElDisj A <-> CoElEqvRel A ) $=
( weldisj wcoeleqvrel mdisjim ax-mp 2th ) ACZADZBHIBAEFG $.
$}

${
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 $.
mdetlemd $p |- ( ph -> ( ElDisj A <-> CoElEqvRel A ) ) $=
( weldisj wcoeleqvrel mdisjim syl 2thd ) ABDZBEZCAIJCBFGH $.
$}

$( The null class is an equivalence relation. (Contributed by Peter Mazsa,
Expand Down Expand Up @@ -561249,21 +561249,22 @@ implies disjointness (e.g. ~ eqvrelqseqdisj5 ), or converse function
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 $.
( weqvrel cdm cqs wceq wa wcoeleqvrel cuni ccoels werALTV wmember
weldisj eqvrelqseqdisj2 mdisjim syl c0 wcel wn n0eldmqseq 3imtr4i
adantl wb eldisjn0el mpbid jca dferALTV2 dfmember3 ) BCZBDZBEAFZG
ZAHZAIAJEAFZGABKALULUMUNULAMZUMAUJBNZAOPULQARSZUNUKUQUIABTUBULUOU
QUNUCUPAUDPUEUFABUGAUHUA $.

$( 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 $.
( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) $=
( weldisj c0 wcel wn cep ccnv cres wdisjALTV cdm cqs wceq weqvrel
wa ccoss wcoeleqvrel cuni ccoels df-eldisj n0el3 eqvrelqseqdisj3
anbi12i petlem eqvreldmqs 3bitri ) ABZCADEZNFGAHZIZUHJUHKALZNUHOZ
MUKJZUKKALNAPAQARKALNUFUIUGUJASATUBAUHAULUKUAUCAUDUE $.

$( Membership Partition-Equivalence Theorem in its shortest possible form:
membership equivalence relation and membership partition are the same (or:
Expand All @@ -561272,15 +561273,16 @@ membership equivalence relation and membership partition are the same (or:
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 $.
( weldisj c0 wcel wn wa wcoeleqvrel cuni ccoels wmembpart wmember
cqs wceq mpet3 dfmembpart2 dfmember3 3bitr4i ) ABCADEFAGAHAILAMFA
JAKANAOAPQ $.

$( Membership Partition-Equivalence Theorem in a shorter form. Together with
~ mpet and ~ mpet3 , this is what is generally identified as the
partition-equivalence theorem (but cf. ~ pet with general ` R ` ).
(Contributed by Peter Mazsa, 24-Sep-2021.) $)
mpet2 $p |- ( ( `' _E |` A ) Part A <-> ,~ ( `' _E |` A ) ErALTV A ) $=
( wmembpart wmember cep ccnv cres wpart ccoss werALTV df-membpart dfmember2
( wmembpart wmember cep ccnv cres wpart ccoss werALTV df-membpart df-member
mpet 3bitr3i ) ABACADEAFZGANHIALAJAKM $.

$( Membership Partition-Equivalence Theorem with binary relations, cf.
Expand Down Expand Up @@ -561312,14 +561314,15 @@ membership equivalence relation and membership partition are the same (or:
$( 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 $.
mainer2 $p |- ( R ErALTV A -> ( CoElEqvRel A /\ -. (/) e. A ) ) $=
( werALTV weldisj c0 wn wa wcoeleqvrel fences2 mdisjim anim1i syl
wcel ) ABCADZEAMFZGAHZOGABINPOAJKL $.

$( 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 $.
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.) $)
Expand Down

0 comments on commit 38978ff

Please sign in to comment.