MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpss12 Unicode version

Theorem xpss12 4780
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
StepHypRef 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 ) )
31, 2im2anan9 811 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  D )
) )
43ssopab2dv 4265 . 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 4675 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4675 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3194 1  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  X.  C
)  C_  ( B  X.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621    C_ wss 3127   {copab 4050    X. cxp 4659
This theorem is referenced by:  xpss  4781  xpss1  4783  xpss2  4784  djussxp  4817  ssxpb  5098  ssrnres  5104  cossxp  5182  relrelss  5183  coexg  5202  fssxp  5338  oprabss  5867  pmss12g  6762  marypha1lem  7154  marypha2lem1  7156  hartogslem1  7225  infxpenlem  7609  dfac5lem4  7721  axdc4lem  8049  fpwwe2lem1  8221  fpwwe2lem11  8230  fpwwe2lem12  8231  fpwwe2lem13  8232  canthwe  8241  tskxpss  8362  dmaddpi  8482  dmmulpi  8483  addnqf  8540  mulnqf  8541  ltrelxr  8854  mulnzcnopr  9382  dfz2  10008  elq  10285  leiso  11362  xpnnenOLD  12450  znnen  12453  eucalg  12719  phimullem  12809  imasless  13404  sscpwex  13654  fullsubc  13686  fullresc  13687  wunfunc  13735  funcres2c  13737  homaf  13824  dmcoass  13860  catcoppccl  13902  catcfuccl  13903  catcxpccl  13943  znleval  16470  txuni2  17222  txbas  17224  txcld  17260  txcls  17261  txcnp  17276  txlly  17292  txnlly  17293  hausdiag  17301  tx1stc  17306  txkgen  17308  xkococnlem  17315  cnmpt2res  17333  clssubg  17753  tsmsxplem1  17797  tsmsxplem2  17798  tsmsxp  17799  xmetres2  17887  metres2  17889  ressprdsds  17897  xmetresbl  17945  ressxms  18033  nrginvrcn  18164  qtopbaslem  18229  tgqioo  18268  re2ndc  18269  resubmet  18270  xrsdsre  18278  bndth  18418  lebnumii  18426  iscfil2  18654  cmsss  18734  minveclem3a  18753  ovolfioo  18789  ovolficc  18790  ovolficcss  18791  ovolfsf  18793  ovollb  18800  ovolicc2  18843  ovolfs2  18888  uniiccdif  18895  uniioovol  18896  uniiccvol  18897  uniioombllem2  18900  uniioombllem3a  18901  uniioombllem3  18902  uniioombllem4  18903  uniioombllem5  18904  uniioombl  18906  dyadmbllem  18916  opnmbllem  18918  opnmblALT  18920  mbfimaopnlem  18972  itg1addlem4  19016  limccnp2  19204  taylfval  19700  taylf  19702  dvdsmulf1o  20396  fsumdvdsmul  20397  resgrprn  20907  issubgoi  20937  ghgrp  20995  sspg  21264  ssps  21266  sspmlem  21268  issh2  21748  hhssabloi  21799  hhssnv  21801  hhshsslem1  21804  shsel  21853  cvmlift2lem9  23214  cvmlift2lem10  23215  cvmlift2lem11  23216  cvmlift2lem12  23217  ghomfo  23370  residcp  24443  nZdef  24547  svs2  24854  prdnei  24940  limptlimpr2lem2  24942  prismorcsetlem  25279  prismorcset  25281  prismorcsetlemc  25284  pgapspf  25419  ssbnd  25879  prdsbnd2  25886  cnpwstotbnd  25888  reheibor  25930  exidreslem  25934  divrngcl  25955  isdrngo2  25956  dibss  30526
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-in 3134  df-ss 3141  df-opab 4052  df-xp 4675
  Copyright terms: Public domain W3C validator