Theorem restrreld

Description: The restriction of a transitive relation is a transitive relation. (Contributed by RP, 24-Dec-2019)

	Ref	Expression
Hypotheses	restrreld.r	⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
	restrreld.s	⊢ ( 𝜑 → 𝑆 = ( 𝑅 ↾ 𝐴 ) )
Assertion	restrreld	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		restrreld.r	⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
2		restrreld.s	⊢ ( 𝜑 → 𝑆 = ( 𝑅 ↾ 𝐴 ) )
3		df-res	⊢ ( 𝑅 ↾ 𝐴 ) = ( 𝑅 ∩ ( 𝐴 × V ) )
4	2 3	eqtrdi	⊢ ( 𝜑 → 𝑆 = ( 𝑅 ∩ ( 𝐴 × V ) ) )
5	1 4	xpintrreld	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 )