Theorem cotr2

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

	Ref	Expression
Hypotheses	cotr2.a	$$⊢\mathrm{dom}R\subseteq A$$
	cotr2.b	$$⊢\mathrm{dom}R\cap \mathrm{ran}R\subseteq B$$
	cotr2.c	$$⊢\mathrm{ran}R\subseteq C$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		cotr2.a	$$⊢\mathrm{dom}R\subseteq A$$
2		cotr2.b	$$⊢\mathrm{dom}R\cap \mathrm{ran}R\subseteq B$$
3		cotr2.c	$$⊢\mathrm{ran}R\subseteq C$$
4		incom	$$⊢\mathrm{dom}R\cap \mathrm{ran}R=\mathrm{ran}R\cap \mathrm{dom}R$$
5	4 2	eqsstrri	$$⊢\mathrm{ran}R\cap \mathrm{dom}R\subseteq B$$
6	1 5 3	cotr2g	$$⊢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)$$