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

Theorem xpss12 4791
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 ) )
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem xpss12
StepHypRef Expression
1 ssel 3175 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3175 . . . 4  |-  ( C 
C_  D  ->  (
y  e.  C  -> 
y  e.  D ) )
31, 2im2anan9 810 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  D )
) )
43ssopab2dv 4292 . 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 4694 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4694 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3220 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 1685    C_ wss 3153   {copab 4077    X. cxp 4686
This theorem is referenced by:  xpss  4792  xpss1  4794  xpss2  4795  djussxp  4828  ssxpb  5109  ssrnres  5115  cossxp  5193  relrelss  5194  coexg  5213  fssxp  5365  oprabss  5894  pmss12g  6789  marypha1lem  7181  marypha2lem1  7183  hartogslem1  7252  infxpenlem  7636  dfac5lem4  7748  axdc4lem  8076  fpwwe2lem1  8248  fpwwe2lem11  8257  fpwwe2lem12  8258  fpwwe2lem13  8259  canthwe  8268  tskxpss  8389  dmaddpi  8509  dmmulpi  8510  addnqf  8567  mulnqf  8568  ltrelxr  8881  mulnzcnopr  9409  dfz2  10036  elq  10313  leiso  11391  xpnnenOLD  12482  znnen  12485  eucalg  12751  phimullem  12841  imasless  13436  sscpwex  13686  fullsubc  13718  fullresc  13719  wunfunc  13767  funcres2c  13769  homaf  13856  dmcoass  13892  catcoppccl  13934  catcfuccl  13935  catcxpccl  13975  znleval  16502  txuni2  17254  txbas  17256  txcld  17292  txcls  17293  txcnp  17308  txlly  17324  txnlly  17325  hausdiag  17333  tx1stc  17338  txkgen  17340  xkococnlem  17347  cnmpt2res  17365  clssubg  17785  tsmsxplem1  17829  tsmsxplem2  17830  tsmsxp  17831  xmetres2  17919  metres2  17921  ressprdsds  17929  xmetresbl  17977  ressxms  18065  nrginvrcn  18196  qtopbaslem  18261  tgqioo  18300  re2ndc  18301  resubmet  18302  xrsdsre  18310  bndth  18450  lebnumii  18458  iscfil2  18686  cmsss  18766  minveclem3a  18785  ovolfioo  18821  ovolficc  18822  ovolficcss  18823  ovolfsf  18825  ovollb  18832  ovolicc2  18875  ovolfs2  18920  uniiccdif  18927  uniioovol  18928  uniiccvol  18929  uniioombllem2  18932  uniioombllem3a  18933  uniioombllem3  18934  uniioombllem4  18935  uniioombllem5  18936  uniioombl  18938  dyadmbllem  18948  opnmbllem  18950  opnmblALT  18952  mbfimaopnlem  19004  itg1addlem4  19048  limccnp2  19236  taylfval  19732  taylf  19734  dvdsmulf1o  20428  fsumdvdsmul  20429  resgrprn  20939  issubgoi  20969  ghgrp  21027  sspg  21296  ssps  21298  sspmlem  21300  issh2  21780  hhssabloi  21831  hhssnv  21833  hhshsslem1  21836  shsel  21885  cvmlift2lem9  23246  cvmlift2lem10  23247  cvmlift2lem11  23248  cvmlift2lem12  23249  ghomfo  23402  residcp  24475  nZdef  24579  svs2  24886  prdnei  24972  limptlimpr2lem2  24974  prismorcsetlem  25311  prismorcset  25313  prismorcsetlemc  25316  pgapspf  25451  ssbnd  25911  prdsbnd2  25918  cnpwstotbnd  25920  reheibor  25962  exidreslem  25966  divrngcl  25987  isdrngo2  25988  dibss  30626
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-in 3160  df-ss 3167  df-opab 4079  df-xp 4694
  Copyright terms: Public domain W3C validator