Theorem xpintrreld

Description: The intersection of a transitive relation with a Cartesian product is a transitve relation. (Contributed by RP, 24-Dec-2019)

	Ref	Expression
Hypotheses	xpintrreld.r	⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
	xpintrreld.s	⊢ ( 𝜑 → 𝑆 = ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) )
Assertion	xpintrreld	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		xpintrreld.r	⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
2		xpintrreld.s	⊢ ( 𝜑 → 𝑆 = ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) )
3		xptrrel	⊢ ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 )
4	3	a1i	⊢ ( 𝜑 → ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 ) )
5	1 4 2	trrelind	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 )