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

Metamath Proof Explorer

Theorem trcoss2

Description: Equivalent expressions for the transitivity of cosets by R . (Contributed by Peter Mazsa, 4-Jul-2020) (Revised by Peter Mazsa, 16-Oct-2021)

		Ref	Expression
	Assertion	trcoss2	$⊢ \forall x \forall y \forall z ((x ≀ R y \land y ≀ R z) \to x ≀ R z) \leftrightarrow \forall x \forall z ([x] ≀ R \cap [z] ≀ R \neq \emptyset \to [x] R^{-1} \cap [z] R^{-1} \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		alcom	$⊢ \forall y \forall z ((x ≀ R y \land y ≀ R z) \to x ≀ R z) \leftrightarrow \forall z \forall y ((x ≀ R y \land y ≀ R z) \to x ≀ R z)$
2	1	albii	$⊢ \forall x \forall y \forall z ((x ≀ R y \land y ≀ R z) \to x ≀ R z) \leftrightarrow \forall x \forall z \forall y ((x ≀ R y \land y ≀ R z) \to x ≀ R z)$
3		19.23v	$⊢ \forall y (y \in ([x] ≀ R \cap [z] ≀ R) \to [x] R^{-1} \cap [z] R^{-1} \neq \emptyset) \leftrightarrow (\exists y y \in ([x] ≀ R \cap [z] ≀ R) \to [x] R^{-1} \cap [z] R^{-1} \neq \emptyset)$
4		eleccossin	$⊢ (y \in V \land z \in V) \to (y \in ([x] ≀ R \cap [z] ≀ R) \leftrightarrow (x ≀ R y \land y ≀ R z))$
5	4	el2v	$⊢ y \in ([x] ≀ R \cap [z] ≀ R) \leftrightarrow (x ≀ R y \land y ≀ R z)$
6	5	bicomi	$⊢ (x ≀ R y \land y ≀ R z) \leftrightarrow y \in ([x] ≀ R \cap [z] ≀ R)$
7		brcoss3	$⊢ (x \in V \land z \in V) \to (x ≀ R z \leftrightarrow [x] R^{-1} \cap [z] R^{-1} \neq \emptyset)$
8	7	el2v	$⊢ x ≀ R z \leftrightarrow [x] R^{-1} \cap [z] R^{-1} \neq \emptyset$
9	6 8	imbi12i	$⊢ ((x ≀ R y \land y ≀ R z) \to x ≀ R z) \leftrightarrow (y \in ([x] ≀ R \cap [z] ≀ R) \to [x] R^{-1} \cap [z] R^{-1} \neq \emptyset)$
10	9	albii	$⊢ \forall y ((x ≀ R y \land y ≀ R z) \to x ≀ R z) \leftrightarrow \forall y (y \in ([x] ≀ R \cap [z] ≀ R) \to [x] R^{-1} \cap [z] R^{-1} \neq \emptyset)$
11		n0	$⊢ [x] ≀ R \cap [z] ≀ R \neq \emptyset \leftrightarrow \exists y y \in ([x] ≀ R \cap [z] ≀ R)$
12	11	imbi1i	$⊢ ([x] ≀ R \cap [z] ≀ R \neq \emptyset \to [x] R^{-1} \cap [z] R^{-1} \neq \emptyset) \leftrightarrow (\exists y y \in ([x] ≀ R \cap [z] ≀ R) \to [x] R^{-1} \cap [z] R^{-1} \neq \emptyset)$
13	3 10 12	3bitr4i	$⊢ \forall y ((x ≀ R y \land y ≀ R z) \to x ≀ R z) \leftrightarrow ([x] ≀ R \cap [z] ≀ R \neq \emptyset \to [x] R^{-1} \cap [z] R^{-1} \neq \emptyset)$
14	13	2albii	$⊢ \forall x \forall z \forall y ((x ≀ R y \land y ≀ R z) \to x ≀ R z) \leftrightarrow \forall x \forall z ([x] ≀ R \cap [z] ≀ R \neq \emptyset \to [x] R^{-1} \cap [z] R^{-1} \neq \emptyset)$
15	2 14	bitri	$⊢ \forall x \forall y \forall z ((x ≀ R y \land y ≀ R z) \to x ≀ R z) \leftrightarrow \forall x \forall z ([x] ≀ R \cap [z] ≀ R \neq \emptyset \to [x] R^{-1} \cap [z] R^{-1} \neq \emptyset)$