Theorem trrelind

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

	Ref	Expression
Hypotheses	trrelind.r	|- ( ph -> ( R o. R ) C_ R )
	trrelind.s	|- ( ph -> ( S o. S ) C_ S )
	trrelind.t	|- ( ph -> T = ( R i^i S ) )
Assertion	trrelind	|- ( ph -> ( T o. T ) C_ T )

Proof

Step	Hyp	Ref	Expression
1		trrelind.r	|- ( ph -> ( R o. R ) C_ R )
2		trrelind.s	|- ( ph -> ( S o. S ) C_ S )
3		trrelind.t	|- ( ph -> T = ( R i^i S ) )
4		inss1	|- ( R i^i S ) C_ R
5	4	a1i	|- ( ph -> ( R i^i S ) C_ R )
6	1 5 5	trrelssd	|- ( ph -> ( ( R i^i S ) o. ( R i^i S ) ) C_ R )
7		inss2	|- ( R i^i S ) C_ S
8	7	a1i	|- ( ph -> ( R i^i S ) C_ S )
9	2 8 8	trrelssd	|- ( ph -> ( ( R i^i S ) o. ( R i^i S ) ) C_ S )
10	6 9	ssind	|- ( ph -> ( ( R i^i S ) o. ( R i^i S ) ) C_ ( R i^i S ) )
11	3 3	coeq12d	|- ( ph -> ( T o. T ) = ( ( R i^i S ) o. ( R i^i S ) ) )
12	10 11 3	3sstr4d	|- ( ph -> ( T o. T ) C_ T )