Theorem restrreld

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

	Ref	Expression
Hypotheses	restrreld.r	|- ( ph -> ( R o. R ) C_ R )
	restrreld.s	|- ( ph -> S = ( R |` A ) )
Assertion	restrreld	|- ( ph -> ( S o. S ) C_ S )

Proof

Step	Hyp	Ref	Expression
1		restrreld.r	|- ( ph -> ( R o. R ) C_ R )
2		restrreld.s	|- ( ph -> S = ( R |` A ) )
3		df-res	|- ( R |` A ) = ( R i^i ( A X. _V ) )
4	2 3	eqtrdi	|- ( ph -> S = ( R i^i ( A X. _V ) ) )
5	1 4	xpintrreld	|- ( ph -> ( S o. S ) C_ S )