Theorem xpintrreld

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

	Ref	Expression
Hypotheses	xpintrreld.r	|- ( ph -> ( R o. R ) C_ R )
	xpintrreld.s	|- ( ph -> S = ( R i^i ( A X. B ) ) )
Assertion	xpintrreld	|- ( ph -> ( S o. S ) C_ S )

Proof

Step	Hyp	Ref	Expression
1		xpintrreld.r	|- ( ph -> ( R o. R ) C_ R )
2		xpintrreld.s	|- ( ph -> S = ( R i^i ( A X. B ) ) )
3		xptrrel	|- ( ( A X. B ) o. ( A X. B ) ) C_ ( A X. B )
4	3	a1i	|- ( ph -> ( ( A X. B ) o. ( A X. B ) ) C_ ( A X. B ) )
5	1 4 2	trrelind	|- ( ph -> ( S o. S ) C_ S )