Theorem xpss12 4711

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 3136	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2		ssel 3136	. . . 4 |- ( C C_ D -> ( y e. C -> y e. D ) )
3	1, 2	im2anan9 588	. . 3 |- ( ( A C_ B /\ C C_ D ) -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. D ) ) )
4	3	ssopab2dv 4256	. 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 4610	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6		df-xp 4610	. 2 |- ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7	4, 5, 6	3sstr4g 3185	1 |- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2136   C_ wss 3116   {copab 4042   X. cxp 4602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-in 3122  df-ss 3129  df-opab 4044  df-xp 4610

This theorem is referenced by:  xpss  4712  xpss1  4714  xpss2  4715  djussxp  4749  ssxpbm  5039  ssrnres  5046  cossxp  5126  cossxp2  5127  cocnvss  5129  relrelss  5130  fssxp  5355  oprabss  5928  pmss12g  6641  caserel  7052  casef  7053  dmaddpi  7266  dmmulpi  7267  rexpssxrxp  7943  ltrelxr  7959  dfz2  9263  phimullem  12157  txuni2  12896  txbas  12898  neitx  12908  txcnp  12911  cnmpt2res  12937  psmetres2  12973  xmetres2  13019  metres2  13021  xmetresbl  13080  xmettx  13150  qtopbasss  13161  tgqioo  13187  resubmet  13188  limccnp2lem  13285  limccnp2cntop  13286