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

Theorem xpss12 4792
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 3174 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3174 . . . 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 4293 . 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 4695 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4695 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3219 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 1684    C_ wss 3152   {copab 4076    X. cxp 4687
This theorem is referenced by:  xpss  4793  xpss1  4795  xpss2  4796  djussxp  4829  ssxpb  5110  ssrnres  5116  cossxp  5195  relrelss  5196  coexg  5215  fssxp  5400  oprabss  5933  pmss12g  6794  marypha1lem  7186  marypha2lem1  7188  hartogslem1  7257  infxpenlem  7641  dfac5lem4  7753  axdc4lem  8081  fpwwe2lem1  8253  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2lem13  8264  canthwe  8273  tskxpss  8394  dmaddpi  8514  dmmulpi  8515  addnqf  8572  mulnqf  8573  ltrelxr  8886  mulnzcnopr  9414  dfz2  10041  elq  10318  leiso  11397  xpnnenOLD  12488  znnen  12491  eucalg  12757  phimullem  12847  imasless  13442  sscpwex  13692  fullsubc  13724  fullresc  13725  wunfunc  13773  funcres2c  13775  homaf  13862  dmcoass  13898  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981  znleval  16508  txuni2  17260  txbas  17262  txcld  17298  txcls  17299  txcnp  17314  txlly  17330  txnlly  17331  hausdiag  17339  tx1stc  17344  txkgen  17346  xkococnlem  17353  cnmpt2res  17371  clssubg  17791  tsmsxplem1  17835  tsmsxplem2  17836  tsmsxp  17837  xmetres2  17925  metres2  17927  ressprdsds  17935  xmetresbl  17983  ressxms  18071  nrginvrcn  18202  qtopbaslem  18267  tgqioo  18306  re2ndc  18307  resubmet  18308  xrsdsre  18316  bndth  18456  lebnumii  18464  iscfil2  18692  cmsss  18772  minveclem3a  18791  ovolfioo  18827  ovolficc  18828  ovolficcss  18829  ovolfsf  18831  ovollb  18838  ovolicc2  18881  ovolfs2  18926  uniiccdif  18933  uniioovol  18934  uniiccvol  18935  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombl  18944  dyadmbllem  18954  opnmbllem  18956  opnmblALT  18958  mbfimaopnlem  19010  itg1addlem4  19054  limccnp2  19242  taylfval  19738  taylf  19740  dvdsmulf1o  20434  fsumdvdsmul  20435  resgrprn  20947  issubgoi  20977  ghgrp  21035  sspg  21304  ssps  21306  sspmlem  21308  issh2  21788  hhssabloi  21839  hhssnv  21841  hhshsslem1  21844  shsel  21893  ofrn2  23207  gtiso  23241  df1stres  23243  df2ndres  23244  xrofsup  23255  tpr2rico  23296  raddcn  23302  xrge0pluscn  23322  br2base  23574  cvmlift2lem9  23842  cvmlift2lem10  23843  cvmlift2lem11  23844  cvmlift2lem12  23845  ghomfo  23998  residcp  25077  nZdef  25180  svs2  25487  prdnei  25573  limptlimpr2lem2  25575  prismorcsetlem  25912  prismorcset  25914  prismorcsetlemc  25917  pgapspf  26052  ssbnd  26512  prdsbnd2  26519  cnpwstotbnd  26521  reheibor  26563  exidreslem  26567  divrngcl  26588  isdrngo2  26589  dibss  31359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-opab 4078  df-xp 4695
  Copyright terms: Public domain W3C validator