This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ MembPart A ↔ CoMembEr A

Proof

Step Hyp Ref Expression
1 mpet3 ⊢ ElDisj A ∧ ¬ ∅ ∈ A ↔ CoElEqvRel A ∧ ⋃ A / ∼ A = A
2 dfmembpart2 ⊢ MembPart A ↔ ElDisj A ∧ ¬ ∅ ∈ A
3 dfcomember3 ⊢ CoMembEr A ↔ CoElEqvRel A ∧ ⋃ A / ∼ A = A
4 1 2 3 3bitr4i ⊢ MembPart A ↔ CoMembEr A