trcoss

Description: Sufficient condition for the transitivity of cosets by R . (Contributed by Peter Mazsa, 26-Dec-2018)

		Ref	Expression
	Assertion	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)$

Step	Hyp	Ref	Expression
1		moantr	$⊢ \exists^{*} u u R y \to ((\exists u (u R x \land u R y) \land \exists u (u R y \land u R z)) \to \exists u (u R x \land u R z))$
2		brcoss	$⊢ (x \in V \land y \in V) \to (x ≀ R y \leftrightarrow \exists u (u R x \land u R y))$
3	2	el2v	$⊢ x ≀ R y \leftrightarrow \exists u (u R x \land u R y)$
4		brcoss	$⊢ (y \in V \land z \in V) \to (y ≀ R z \leftrightarrow \exists u (u R y \land u R z))$
5	4	el2v	$⊢ y ≀ R z \leftrightarrow \exists u (u R y \land u R z)$
6	3 5	anbi12i	$⊢ (x ≀ R y \land y ≀ R z) \leftrightarrow (\exists u (u R x \land u R y) \land \exists u (u R y \land u R z))$
7		brcoss	$⊢ (x \in V \land z \in V) \to (x ≀ R z \leftrightarrow \exists u (u R x \land u R z))$
8	7	el2v	$⊢ x ≀ R z \leftrightarrow \exists u (u R x \land u R z)$
9	1 6 8	3imtr4g	$⊢ \exists^{*} u u R y \to ((x ≀ R y \land y ≀ R z) \to x ≀ R z)$
10	9	alrimiv	$⊢ \exists^{*} u u R y \to \forall z ((x ≀ R y \land y ≀ R z) \to x ≀ R z)$
11	10	alimi	$⊢ \forall y \exists^{*} u u R y \to \forall y \forall z ((x ≀ R y \land y ≀ R z) \to x ≀ R z)$
12	11	alrimiv	$⊢ \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)$

Metamath Proof Explorer