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

Theorem xpss12 4745
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 3116 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3116 . . . 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 4230 . 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 4640 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4640 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3161 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 3094   {copab 4016    X. cxp 4624
This theorem is referenced by:  xpss  4746  xpss1  4748  xpss2  4749  djussxp  4782  ssxpb  5063  ssrnres  5069  cossxp  5147  relrelss  5148  coexg  5167  fssxp  5303  oprabss  5832  pmss12g  6727  marypha1lem  7119  marypha2lem1  7121  hartogslem1  7190  infxpenlem  7574  dfac5lem4  7686  axdc4lem  8014  fpwwe2lem1  8186  fpwwe2lem11  8195  fpwwe2lem12  8196  fpwwe2lem13  8197  canthwe  8206  tskxpss  8327  dmaddpi  8447  dmmulpi  8448  addnqf  8505  mulnqf  8506  ltrelxr  8819  mulnzcnopr  9347  dfz2  9973  elq  10250  leiso  11327  xpnnenOLD  12415  znnen  12418  eucalg  12684  phimullem  12774  imasless  13369  sscpwex  13619  fullsubc  13651  fullresc  13652  wunfunc  13700  funcres2c  13702  homaf  13789  dmcoass  13825  catcoppccl  13867  catcfuccl  13868  catcxpccl  13908  znleval  16435  txuni2  17187  txbas  17189  txcld  17225  txcls  17226  txcnp  17241  txlly  17257  txnlly  17258  hausdiag  17266  tx1stc  17271  txkgen  17273  xkococnlem  17280  cnmpt2res  17298  clssubg  17718  tsmsxplem1  17762  tsmsxplem2  17763  tsmsxp  17764  xmetres2  17852  metres2  17854  ressprdsds  17862  xmetresbl  17910  ressxms  17998  nrginvrcn  18129  qtopbaslem  18194  tgqioo  18233  re2ndc  18234  resubmet  18235  xrsdsre  18243  bndth  18383  lebnumii  18391  iscfil2  18619  cmsss  18699  minveclem3a  18718  ovolfioo  18754  ovolficc  18755  ovolficcss  18756  ovolfsf  18758  ovollb  18765  ovolicc2  18808  ovolfs2  18853  uniiccdif  18860  uniioovol  18861  uniiccvol  18862  uniioombllem2  18865  uniioombllem3a  18866  uniioombllem3  18867  uniioombllem4  18868  uniioombllem5  18869  uniioombl  18871  dyadmbllem  18881  opnmbllem  18883  opnmblALT  18885  mbfimaopnlem  18937  itg1addlem4  18981  limccnp2  19169  taylfval  19665  taylf  19667  dvdsmulf1o  20361  fsumdvdsmul  20362  resgrprn  20872  issubgoi  20902  ghgrp  20960  sspg  21229  ssps  21231  sspmlem  21233  issh2  21713  hhssabloi  21764  hhssnv  21766  hhshsslem1  21769  shsel  21818  cvmlift2lem9  23179  cvmlift2lem10  23180  cvmlift2lem11  23181  cvmlift2lem12  23182  ghomfo  23335  residcp  24408  nZdef  24512  svs2  24819  prdnei  24905  limptlimpr2lem2  24907  prismorcsetlem  25244  prismorcset  25246  prismorcsetlemc  25249  pgapspf  25384  ssbnd  25844  prdsbnd2  25851  cnpwstotbnd  25853  reheibor  25895  exidreslem  25899  divrngcl  25920  isdrngo2  25921  dibss  30489
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-in 3101  df-ss 3108  df-opab 4018  df-xp 4640
  Copyright terms: Public domain W3C validator