Metamath Proof Explorer

Theorem cpet2

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

Ref Expression
Assertion cpet2 ⊢ElDisjA∧¬∅∈A↔EqvRel∼A∧⋃A/∼A=A

Proof

Step Hyp Ref Expression
1 eldisjn0elb ⊢ElDisjA∧¬∅∈A↔DisjE-1↾A∧dom⁡E-1↾A/E-1↾A=A
2 eqvrelqseqdisj3 ⊢EqvRel≀E-1↾A∧dom⁡≀E-1↾A/≀E-1↾A=A→DisjE-1↾A
3 2 petlem ⊢DisjE-1↾A∧dom⁡E-1↾A/E-1↾A=A↔EqvRel≀E-1↾A∧dom⁡≀E-1↾A/≀E-1↾A=A
4 eqvreldmqs2 ⊢EqvRel≀E-1↾A∧dom⁡≀E-1↾A/≀E-1↾A=A↔EqvRel∼A∧⋃A/∼A=A
5 1 3 4 3bitri ⊢ElDisjA∧¬∅∈A↔EqvRel∼A∧⋃A/∼A=A