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	$$⊢\phi \to R\circ R\subseteq R$$
	trrelssd.s	$$⊢\phi \to S\subseteq R$$
	trrelssd.t	$$⊢\phi \to T\subseteq R$$
Assertion	trrelssd	$$⊢\phi \to S\circ T\subseteq R$$

Proof

Step	Hyp	Ref	Expression
1		trrelssd.r	$$⊢\phi \to R\circ R\subseteq R$$
2		trrelssd.s	$$⊢\phi \to S\subseteq R$$
3		trrelssd.t	$$⊢\phi \to T\subseteq R$$
4	2 3	coss12d	$$⊢\phi \to S\circ T\subseteq R\circ R$$
5	4 1	sstrd	$$⊢\phi \to S\circ T\subseteq R$$