Metamath Proof Explorer

Theorem mpet3

Description: Member Partition-Equivalence Theorem. Together with mpet mpet2 , mostly in its conventional cpet and cpet2 form, this is what we used to think of 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)

Ref Expression
Assertion mpet3 ⊢ ElDisj A ∧ ¬ ∅ ∈ A ↔ CoElEqvRel A ∧ ⋃ A / ∼ A = A

Proof

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