Theorem xpss12 4800

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 3195	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2		ssel 3195	. . . 4 |- ( C C_ D -> ( y e. C -> y e. D ) )
3	1, 2	im2anan9 598	. . 3 |- ( ( A C_ B /\ C C_ D ) -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. D ) ) )
4	3	ssopab2dv 4343	. 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 4699	. 2 |- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6		df-xp 4699	. 2 |- ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7	4, 5, 6	3sstr4g 3244	1 |- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2178   C_ wss 3174   {copab 4120   X. cxp 4691

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-in 3180  df-ss 3187  df-opab 4122  df-xp 4699

This theorem is referenced by:  xpss  4801  xpss1  4803  xpss2  4804  djussxp  4841  ssxpbm  5137  ssrnres  5144  cossxp  5224  cossxp2  5225  cocnvss  5227  relrelss  5228  fssxp  5463  oprabss  6054  pmss12g  6785  caserel  7215  casef  7216  dmaddpi  7473  dmmulpi  7474  rexpssxrxp  8152  ltrelxr  8168  dfz2  9480  phimullem  12662  znleval  14530  txuni2  14843  txbas  14845  neitx  14855  txcnp  14858  cnmpt2res  14884  psmetres2  14920  xmetres2  14966  metres2  14968  xmetresbl  15027  xmettx  15097  qtopbasss  15108  tgqioo  15142  resubmet  15143  limccnp2lem  15263  limccnp2cntop  15264  mpodvdsmulf1o  15577  fsumdvdsmul  15578