Theorem xpss12 4831

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 3219	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2		ssel 3219	. . . 4 |- ( C C_ D -> ( y e. C -> y e. D ) )
3	1, 2	im2anan9 600	. . 3 |- ( ( A C_ B /\ C C_ D ) -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. D ) ) )
4	3	ssopab2dv 4371	. 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 4729	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6		df-xp 4729	. 2 |- ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7	4, 5, 6	3sstr4g 3268	1 |- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200   C_ wss 3198   {copab 4147   X. cxp 4721

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-in 3204  df-ss 3211  df-opab 4149  df-xp 4729

This theorem is referenced by:  xpss  4832  xpss1  4834  xpss2  4835  djussxp  4873  ssxpbm  5170  ssrnres  5177  cossxp  5257  cossxp2  5258  cocnvss  5260  relrelss  5261  fssxp  5499  oprabss  6102  pmss12g  6839  caserel  7277  casef  7278  dmaddpi  7535  dmmulpi  7536  rexpssxrxp  8214  ltrelxr  8230  dfz2  9542  phimullem  12787  znleval  14657  txuni2  14970  txbas  14972  neitx  14982  txcnp  14985  cnmpt2res  15011  psmetres2  15047  xmetres2  15093  metres2  15095  xmetresbl  15154  xmettx  15224  qtopbasss  15235  tgqioo  15269  resubmet  15270  limccnp2lem  15390  limccnp2cntop  15391  mpodvdsmulf1o  15704  fsumdvdsmul  15705