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

Metamath Proof Explorer

Theorem petlemi

Description: If you can prove disjointness (e.g. disjALTV0 , disjALTVid , disjALTVidres , disjALTVxrnidres , search for theorems containing the ' |- Disj ' string), or the same with converse function (cf. dfdisjALTV ), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. (Contributed by Peter Mazsa, 18-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 petlemi.1 ⊢ Disj R
2 1 a1i ⊢ EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A → Disj R
3 2 petlem ⊢ Disj R ∧ dom ⁡ R / R = A ↔ EqvRel ≀ R ∧ dom ⁡ ≀ R / ≀ R = A