Theorem cotr3

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

	Ref	Expression
Hypotheses	cotr3.a	$$⊢A=\mathrm{dom}R$$
	cotr3.b	$$⊢B=A\cap C$$
	cotr3.c	$$⊢C=\mathrm{ran}R$$
Assertion	cotr3	$$⊢R\circ R\subseteq R\leftrightarrow \forall x\in A\forall y\in B\forall z\in C\left(\left(xRy\wedge yRz\right)\to xRz\right)$$

Proof

Step	Hyp	Ref	Expression
1		cotr3.a	$$⊢A=\mathrm{dom}R$$
2		cotr3.b	$$⊢B=A\cap C$$
3		cotr3.c	$$⊢C=\mathrm{ran}R$$
4	1	eqimss2i	$$⊢\mathrm{dom}R\subseteq A$$
5	1 3	ineq12i	$$⊢A\cap C=\mathrm{dom}R\cap \mathrm{ran}R$$
6	2 5	eqtri	$$⊢B=\mathrm{dom}R\cap \mathrm{ran}R$$
7	6	eqimss2i	$$⊢\mathrm{dom}R\cap \mathrm{ran}R\subseteq B$$
8	3	eqimss2i	$$⊢\mathrm{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\left(\left(xRy\wedge yRz\right)\to xRz\right)$$