Theorem trrelssd

Description: The composition of subclasses of a transitive relation is a subclass of that relation. (Contributed by RP, 24-Dec-2019)

	Ref	Expression
Hypotheses	trrelssd.r	|- ( ph -> ( R o. R ) C_ R )
	trrelssd.s	|- ( ph -> S C_ R )
	trrelssd.t	|- ( ph -> T C_ R )
Assertion	trrelssd	|- ( ph -> ( S o. T ) C_ R )

Proof

Step	Hyp	Ref	Expression
1		trrelssd.r	|- ( ph -> ( R o. R ) C_ R )
2		trrelssd.s	|- ( ph -> S C_ R )
3		trrelssd.t	|- ( ph -> T C_ R )
4	2 3	coss12d	|- ( ph -> ( S o. T ) C_ ( R o. R ) )
5	4 1	sstrd	|- ( ph -> ( S o. T ) C_ R )