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
|- ( 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 )