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