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