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

Metamath Proof Explorer

Theorem coss12d

Description: Subset deduction for composition of two classes. (Contributed by RP, 24-Dec-2019)

Ref Expression
Hypotheses coss12d.a 
|- ( ph -> A C_ B )
coss12d.c 
|- ( ph -> C C_ D )
Assertion coss12d 
|- ( ph -> ( A o. C ) C_ ( B o. D ) )

Proof

Step Hyp Ref Expression
1 coss12d.a 
 |-  ( ph -> A C_ B )
2 coss12d.c 
 |-  ( ph -> C C_ D )
3 2 ssbrd 
 |-  ( ph -> ( x C y -> x D y ) )
4 1 ssbrd 
 |-  ( ph -> ( y A z -> y B z ) )
5 3 4 anim12d 
 |-  ( ph -> ( ( x C y /\ y A z ) -> ( x D y /\ y B z ) ) )
6 5 eximdv 
 |-  ( ph -> ( E. y ( x C y /\ y A z ) -> E. y ( x D y /\ y B z ) ) )
7 6 ssopab2dv 
 |-  ( ph -> { <. x , z >. | E. y ( x C y /\ y A z ) } C_ { <. x , z >. | E. y ( x D y /\ y B z ) } )
8 df-co 
 |-  ( A o. C ) = { <. x , z >. | E. y ( x C y /\ y A z ) }
9 df-co 
 |-  ( B o. D ) = { <. x , z >. | E. y ( x D y /\ y B z ) }
10 7 8 9 3sstr4g 
 |-  ( ph -> ( A o. C ) C_ ( B o. D ) )