Theorem xpss12 4733

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148   C_ wss 3129   {copab 4063   X. cxp 4624

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-in 3135  df-ss 3142  df-opab 4065  df-xp 4632

This theorem is referenced by:  xpss  4734  xpss1  4736  xpss2  4737  djussxp  4772  ssxpbm  5064  ssrnres  5071  cossxp  5151  cossxp2  5152  cocnvss  5154  relrelss  5155  fssxp  5383  oprabss  5960  pmss12g  6674  caserel  7085  casef  7086  dmaddpi  7323  dmmulpi  7324  rexpssxrxp  8001  ltrelxr  8017  dfz2  9324  phimullem  12224  txuni2  13726  txbas  13728  neitx  13738  txcnp  13741  cnmpt2res  13767  psmetres2  13803  xmetres2  13849  metres2  13851  xmetresbl  13910  xmettx  13980  qtopbasss  13991  tgqioo  14017  resubmet  14018  limccnp2lem  14115  limccnp2cntop  14116