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	⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
	trrelssd.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝑅 )
	trrelssd.t	⊢ ( 𝜑 → 𝑇 ⊆ 𝑅 )
Assertion	trrelssd	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑇 ) ⊆ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		trrelssd.r	⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
2		trrelssd.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝑅 )
3		trrelssd.t	⊢ ( 𝜑 → 𝑇 ⊆ 𝑅 )
4	2 3	coss12d	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑇 ) ⊆ ( 𝑅 ∘ 𝑅 ) )
5	4 1	sstrd	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑇 ) ⊆ 𝑅 )