Theorem coss12dOLD

Description: Obsolete version of coss12d as of 8-Nov-2026. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		coss12dOLD.a	|- ( ph -> A C_ B )
2		coss12dOLD.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 ) )