Metamath Proof Explorer

Theorem disjim

Description: The "Divide et Aequivalere" Theorem: every disjoint relation generates equivalent cosets by the relation: generalization of the former prter1 , cf. eldisjim . (Contributed by Peter Mazsa, 3-May-2019) (Revised by Peter Mazsa, 17-Sep-2021)

Ref Expression
Assertion disjim ⊢ Disj R → EqvRel ≀ R

Proof

Step Hyp Ref Expression
1 dfdisjALTV4 ⊢ Disj R ↔ ∀ y ∃* u u R y ∧ Rel ⁡ R
2 1 simplbi ⊢ Disj R → ∀ y ∃* u u R y
3 trcoss ⊢ ∀ y ∃* u u R y → ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z
4 2 3 syl ⊢ Disj R → ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z
5 eqvrelcoss3 ⊢ EqvRel ≀ R ↔ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z
6 4 5 sylibr ⊢ Disj R → EqvRel ≀ R