Theorem xpss12 4705

Description: Subset theorem for cross product. Generalization of Theorem 101 of [Suppes] p. 52. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
xpss12	|- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Proof of Theorem xpss12

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3131	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2		ssel 3131	. . . 4 |- ( C C_ D -> ( y e. C -> y e. D ) )
3	1, 2	im2anan9 588	. . 3 |- ( ( A C_ B /\ C C_ D ) -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. D ) ) )
4	3	ssopab2dv 4250	. 2 |- ( ( A C_ B /\ C C_ D ) -> { <. x , y >. | ( x e. A /\ y e. C ) } C_ { <. x , y >. | ( x e. B /\ y e. D ) } )
5		df-xp 4604	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6		df-xp 4604	. 2 |- ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7	4, 5, 6	3sstr4g 3180	1 |- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2135   C_ wss 3111   {copab 4036   X. cxp 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-in 3117  df-ss 3124  df-opab 4038  df-xp 4604

This theorem is referenced by:  xpss  4706  xpss1  4708  xpss2  4709  djussxp  4743  ssxpbm  5033  ssrnres  5040  cossxp  5120  cossxp2  5121  cocnvss  5123  relrelss  5124  fssxp  5349  oprabss  5919  pmss12g  6632  caserel  7043  casef  7044  dmaddpi  7257  dmmulpi  7258  rexpssxrxp  7934  ltrelxr  7950  dfz2  9254  phimullem  12134  txuni2  12797  txbas  12799  neitx  12809  txcnp  12812  cnmpt2res  12838  psmetres2  12874  xmetres2  12920  metres2  12922  xmetresbl  12981  xmettx  13051  qtopbasss  13062  tgqioo  13088  resubmet  13089  limccnp2lem  13186  limccnp2cntop  13187