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

Theorem xpss12 4808
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.
StepHypRef Expression
1 ssel 3187 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3187 . . . 4  |-  ( C 
C_  D  ->  (
y  e.  C  -> 
y  e.  D ) )
31, 2im2anan9 808 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  D )
) )
43ssopab2dv 4309 . 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 4711 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4711 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3232 1  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  X.  C
)  C_  ( B  X.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696    C_ wss 3165   {copab 4092    X. cxp 4703
This theorem is referenced by:  xpss  4809  xpss1  4811  xpss2  4812  djussxp  4845  ssxpb  5126  ssrnres  5132  cossxp  5211  relrelss  5212  coexg  5231  fssxp  5416  oprabss  5949  pmss12g  6810  marypha1lem  7202  marypha2lem1  7204  hartogslem1  7273  infxpenlem  7657  dfac5lem4  7769  axdc4lem  8097  fpwwe2lem1  8269  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe2lem13  8280  canthwe  8289  tskxpss  8410  dmaddpi  8530  dmmulpi  8531  addnqf  8588  mulnqf  8589  ltrelxr  8902  mulnzcnopr  9430  dfz2  10057  elq  10334  leiso  11413  xpnnenOLD  12504  znnen  12507  eucalg  12773  phimullem  12863  imasless  13458  sscpwex  13708  fullsubc  13740  fullresc  13741  wunfunc  13789  funcres2c  13791  homaf  13878  dmcoass  13914  catcoppccl  13956  catcfuccl  13957  catcxpccl  13997  znleval  16524  txuni2  17276  txbas  17278  txcld  17314  txcls  17315  txcnp  17330  txlly  17346  txnlly  17347  hausdiag  17355  tx1stc  17360  txkgen  17362  xkococnlem  17369  cnmpt2res  17387  clssubg  17807  tsmsxplem1  17851  tsmsxplem2  17852  tsmsxp  17853  xmetres2  17941  metres2  17943  ressprdsds  17951  xmetresbl  17999  ressxms  18087  nrginvrcn  18218  qtopbaslem  18283  tgqioo  18322  re2ndc  18323  resubmet  18324  xrsdsre  18332  bndth  18472  lebnumii  18480  iscfil2  18708  cmsss  18788  minveclem3a  18807  ovolfioo  18843  ovolficc  18844  ovolficcss  18845  ovolfsf  18847  ovollb  18854  ovolicc2  18897  ovolfs2  18942  uniiccdif  18949  uniioovol  18950  uniiccvol  18951  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  uniioombl  18960  dyadmbllem  18970  opnmbllem  18972  opnmblALT  18974  mbfimaopnlem  19026  itg1addlem4  19070  limccnp2  19258  taylfval  19754  taylf  19756  dvdsmulf1o  20450  fsumdvdsmul  20451  resgrprn  20963  issubgoi  20993  ghgrp  21051  sspg  21320  ssps  21322  sspmlem  21324  issh2  21804  hhssabloi  21855  hhssnv  21857  hhshsslem1  21860  shsel  21909  ofrn2  23222  gtiso  23256  df1stres  23258  df2ndres  23259  xrofsup  23270  tpr2rico  23311  raddcn  23317  xrge0pluscn  23337  br2base  23589  cvmlift2lem9  23857  cvmlift2lem10  23858  cvmlift2lem11  23859  cvmlift2lem12  23860  ghomfo  24013  residcp  25180  nZdef  25283  svs2  25590  prdnei  25676  limptlimpr2lem2  25678  prismorcsetlem  26015  prismorcset  26017  prismorcsetlemc  26020  pgapspf  26155  ssbnd  26615  prdsbnd2  26622  cnpwstotbnd  26624  reheibor  26666  exidreslem  26670  divrngcl  26691  isdrngo2  26692  dibss  31981
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179  df-opab 4094  df-xp 4711
  Copyright terms: Public domain W3C validator