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

Metamath Proof Explorer

Theorem cotr3

Description: Two ways of saying a relation is transitive. (Contributed by RP, 22-Mar-2020)

		Ref	Expression
	Hypotheses	cotr3.a	$⊢ A = dom R$
		cotr3.b	$⊢ B = A \cap C$
		cotr3.c	$⊢ C = ran R$
	Assertion	cotr3	$⊢ R \circ R \subseteq R \leftrightarrow \forall x \in A \forall y \in B \forall z \in C ((x R y \land y R z) \to x R z)$

Proof

Step	Hyp	Ref	Expression
1		cotr3.a	$⊢ A = dom R$
2		cotr3.b	$⊢ B = A \cap C$
3		cotr3.c	$⊢ C = ran R$
4	1	eqimss2i	$⊢ dom R \subseteq A$
5	1 3	ineq12i	$⊢ A \cap C = dom R \cap ran R$
6	2 5	eqtri	$⊢ B = dom R \cap ran R$
7	6	eqimss2i	$⊢ dom R \cap ran R \subseteq B$
8	3	eqimss2i	$⊢ ran R \subseteq C$
9	4 7 8	cotr2	$⊢ R \circ R \subseteq R \leftrightarrow \forall x \in A \forall y \in B \forall z \in C ((x R y \land y R z) \to x R z)$