This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → R ∘ R ⊆ R
trrelssd.s ⊢ φ → S ⊆ R
trrelssd.t ⊢ φ → T ⊆ R
Assertion trrelssd ⊢ φ → S ∘ T ⊆ R

Proof

Step Hyp Ref Expression
1 trrelssd.r ⊢ φ → R ∘ R ⊆ R
2 trrelssd.s ⊢ φ → S ⊆ R
3 trrelssd.t ⊢ φ → T ⊆ R
4 2 3 coss12d ⊢ φ → S ∘ T ⊆ R ∘ R
5 4 1 sstrd ⊢ φ → S ∘ T ⊆ R