Theorem xpss12 4859

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 3234	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2		ssel 3234	. . . 4 |- ( C C_ D -> ( y e. C -> y e. D ) )
3	1, 2	im2anan9 602	. . 3 |- ( ( A C_ B /\ C C_ D ) -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. D ) ) )
4	3	ssopab2dv 4399	. 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 4757	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6		df-xp 4757	. 2 |- ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7	4, 5, 6	3sstr4g 3283	1 |- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2205   C_ wss 3213   {copab 4172   X. cxp 4749

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-in 3219  df-ss 3226  df-opab 4174  df-xp 4757

This theorem is referenced by:  xpss  4860  xpss1  4862  xpss2  4863  djussxp  4902  ssxpbm  5200  ssrnres  5207  cossxp  5287  cossxp2  5288  cocnvss  5290  relrelss  5291  fssxp  5532  oprabss  6141  pmss12g  6911  caserel  7380  casef  7381  dmaddpi  7642  dmmulpi  7643  rexpssxrxp  8320  ltrelxr  8336  dfz2  9652  phimullem  12926  znleval  14818  txuni2  15138  txbas  15140  neitx  15150  txcnp  15153  cnmpt2res  15179  psmetres2  15215  xmetres2  15261  metres2  15263  xmetresbl  15322  xmettx  15392  qtopbasss  15403  tgqioo  15437  resubmet  15438  limccnp2lem  15558  limccnp2cntop  15559  mpodvdsmulf1o  15875  fsumdvdsmul  15876