Theorem mpet

Description: 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)

	Ref	Expression
Assertion	mpet	Could not format assertion : No typesetting found for |- ( MembPart A <-> CoMembEr A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mpet3	$$⊢\left(ElDisjA\wedge \neg \varnothing \in A\right)\leftrightarrow \left(CoElEqvRelA\wedge \bigcup A/\sim A=A\right)$$
2		dfmembpart2	Could not format ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) : No typesetting found for |- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) with typecode |-
3		dfcomember3	Could not format ( CoMembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) : No typesetting found for |- ( CoMembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) with typecode |-
4	1 2 3	3bitr4i	Could not format ( MembPart A <-> CoMembEr A ) : No typesetting found for |- ( MembPart A <-> CoMembEr A ) with typecode |-