Metamath Proof Explorer

Theorem petlem

Description: If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 ), or converse function (cf. dfdisjALTV ), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 . (Contributed by Peter Mazsa, 18-Sep-2021)

Ref Expression
Hypothesis petlem.1 ⊢ EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A → Disj R
Assertion petlem ⊢ Disj R ∧ dom ⁡ R / R = A ↔ EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A

Proof

Step Hyp Ref Expression
1 petlem.1 ⊢ EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A → Disj R
2 partim2 ⊢ Disj R ∧ dom ⁡ R / R = A → EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A
3 simpr ⊢ EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A → dom ⁡ ≀ R / ≀ R = A
4 disjdmqseq ⊢ Disj R → dom ⁡ R / R = A ↔ dom ⁡ ≀ R / ≀ R = A
5 4 pm5.32i ⊢ Disj R ∧ dom ⁡ R / R = A ↔ Disj R ∧ dom ⁡ ≀ R / ≀ R = A
6 1 3 5 sylanbrc ⊢ EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A → Disj R ∧ dom ⁡ R / R = A
7 2 6 impbii ⊢ Disj R ∧ dom ⁡ R / R = A ↔ EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A