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

Metamath Proof Explorer

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 (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \cap (A \times A)$

Proof

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