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 \to EqvRel ≀ R$

Proof

Step	Hyp	Ref	Expression
1		dfdisjALTV4	$⊢ Disj R \leftrightarrow (\forall y \exists^{*} u u R y \land Rel R)$
2	1	simplbi	$⊢ Disj R \to \forall y \exists^{*} u u R y$
3		trcoss	$⊢ \forall y \exists^{*} u u R y \to \forall x \forall y \forall z ((x ≀ R y \land y ≀ R z) \to x ≀ R z)$
4	2 3	syl	$⊢ Disj R \to \forall x \forall y \forall z ((x ≀ R y \land y ≀ R z) \to x ≀ R z)$
5		eqvrelcoss3	$⊢ EqvRel ≀ R \leftrightarrow \forall x \forall y \forall z ((x ≀ R y \land y ≀ R z) \to x ≀ R z)$
6	4 5	sylibr	$⊢ Disj R \to EqvRel ≀ R$

Metamath Proof Explorer

Theorem disjim

Proof