Theorem xpss12 4727

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 3147	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2		ssel 3147	. . . 4 |- ( C C_ D -> ( y e. C -> y e. D ) )
3	1, 2	im2anan9 598	. . 3 |- ( ( A C_ B /\ C C_ D ) -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. D ) ) )
4	3	ssopab2dv 4272	. 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 4626	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6		df-xp 4626	. 2 |- ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7	4, 5, 6	3sstr4g 3196	1 |- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2146   C_ wss 3127   {copab 4058   X. cxp 4618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-in 3133  df-ss 3140  df-opab 4060  df-xp 4626

This theorem is referenced by:  xpss  4728  xpss1  4730  xpss2  4731  djussxp  4765  ssxpbm  5056  ssrnres  5063  cossxp  5143  cossxp2  5144  cocnvss  5146  relrelss  5147  fssxp  5375  oprabss  5951  pmss12g  6665  caserel  7076  casef  7077  dmaddpi  7299  dmmulpi  7300  rexpssxrxp  7976  ltrelxr  7992  dfz2  9296  phimullem  12190  txuni2  13307  txbas  13309  neitx  13319  txcnp  13322  cnmpt2res  13348  psmetres2  13384  xmetres2  13430  metres2  13432  xmetresbl  13491  xmettx  13561  qtopbasss  13572  tgqioo  13598  resubmet  13599  limccnp2lem  13696  limccnp2cntop  13697