Theorem trinxp

Description: The relation induced by a transitive relation on a part of its field is transitive. (Taking the intersection of a relation with a Cartesian square is a way to restrict it to a subset of its field.) (Contributed by FL, 31-Jul-2009)

	Ref	Expression
Assertion	trinxp	$$⊢R\circ R\subseteq R\to \left(R\cap \left(A\times A\right)\right)\circ \left(R\cap \left(A\times A\right)\right)\subseteq R\cap \left(A\times A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpidtr	$$⊢\left(A\times A\right)\circ \left(A\times A\right)\subseteq A\times A$$
2		trin2	$$⊢\left(R\circ R\subseteq R\wedge \left(A\times A\right)\circ \left(A\times A\right)\subseteq A\times A\right)\to \left(R\cap \left(A\times A\right)\right)\circ \left(R\cap \left(A\times A\right)\right)\subseteq R\cap \left(A\times A\right)$$
3	1 2	mpan2	$$⊢R\circ R\subseteq R\to \left(R\cap \left(A\times A\right)\right)\circ \left(R\cap \left(A\times A\right)\right)\subseteq R\cap \left(A\times A\right)$$