Theorem xpss12 4604

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 3055	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2		ssel 3055	. . . 4 |- ( C C_ D -> ( y e. C -> y e. D ) )
3	1, 2	im2anan9 570	. . 3 |- ( ( A C_ B /\ C C_ D ) -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. D ) ) )
4	3	ssopab2dv 4158	. 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 4503	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6		df-xp 4503	. 2 |- ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7	4, 5, 6	3sstr4g 3104	1 |- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1461   C_ wss 3035   {copab 3946   X. cxp 4495

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-in 3041  df-ss 3048  df-opab 3948  df-xp 4503

This theorem is referenced by:  xpss  4605  xpss1  4607  xpss2  4608  djussxp  4642  ssxpbm  4930  ssrnres  4937  cossxp  5017  cossxp2  5018  cocnvss  5020  relrelss  5021  fssxp  5246  oprabss  5809  pmss12g  6521  caserel  6922  casef  6923  dmaddpi  7075  dmmulpi  7076  rexpssxrxp  7728  ltrelxr  7743  dfz2  9021  phimullem  11740  txuni2  12261  txbas  12263  neitx  12273  txcnp  12276  cnmpt2res  12302  psmetres2  12316  xmetres2  12362  metres2  12364  xmetresbl  12423  xmettx  12493  qtopbasss  12504  tgqioo  12527  resubmet  12528  limccnp2lem  12595  limccnp2cntop  12596