Theorem xpss12 4839

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 3222	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2		ssel 3222	. . . 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 4379	. 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 4737	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6		df-xp 4737	. 2 |- ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7	4, 5, 6	3sstr4g 3271	1 |- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202   C_ wss 3201   {copab 4154   X. cxp 4729

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-in 3207  df-ss 3214  df-opab 4156  df-xp 4737

This theorem is referenced by:  xpss  4840  xpss1  4842  xpss2  4843  djussxp  4881  ssxpbm  5179  ssrnres  5186  cossxp  5266  cossxp2  5267  cocnvss  5269  relrelss  5270  fssxp  5510  oprabss  6117  pmss12g  6887  caserel  7329  casef  7330  dmaddpi  7588  dmmulpi  7589  rexpssxrxp  8266  ltrelxr  8282  dfz2  9596  phimullem  12860  znleval  14732  txuni2  15050  txbas  15052  neitx  15062  txcnp  15065  cnmpt2res  15091  psmetres2  15127  xmetres2  15173  metres2  15175  xmetresbl  15234  xmettx  15304  qtopbasss  15315  tgqioo  15349  resubmet  15350  limccnp2lem  15470  limccnp2cntop  15471  mpodvdsmulf1o  15787  fsumdvdsmul  15788