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 ⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
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 ⊢ ( 𝜑 → ( 𝑆 ∘ 𝑇 ) ⊆ 𝑅 )