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	⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpidtr	⊢ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )
2		trin2	⊢ ( ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) ) → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )
3	1 2	mpan2	⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )