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

Theorem xpss12 4699
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 3097 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3097 . . . 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 4186 . 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 4594 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4594 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3140 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 3078   {copab 3973    X. cxp 4578
This theorem is referenced by:  xpss  4700  xpss1  4702  xpss2  4703  djussxp  4736  ssxpb  5017  ssrnres  5023  cossxp  5101  relrelss  5102  coexg  5121  fssxp  5257  oprabss  5785  pmss12g  6680  marypha1lem  7070  marypha2lem1  7072  hartogslem1  7141  infxpenlem  7525  dfac5lem4  7637  axdc4lem  7965  fpwwe2lem1  8133  fpwwe2lem11  8142  fpwwe2lem12  8143  fpwwe2lem13  8144  canthwe  8153  tskxpss  8274  dmaddpi  8394  dmmulpi  8395  addnqf  8452  mulnqf  8453  ltrelxr  8766  mulnzcnopr  9294  dfz2  9920  elq  10197  leiso  11274  xpnnenOLD  12362  znnen  12365  eucalg  12631  phimullem  12721  imasless  13316  sscpwex  13536  fullsubc  13568  fullresc  13569  wunfunc  13617  funcres2c  13619  homaf  13706  dmcoass  13742  catcoppccl  13784  catcfuccl  13785  catcxpccl  13825  znleval  16340  txuni2  17092  txbas  17094  txcld  17130  txcls  17131  txcnp  17146  txlly  17162  txnlly  17163  hausdiag  17171  tx1stc  17176  txkgen  17178  xkococnlem  17185  cnmpt2res  17203  clssubg  17623  tsmsxplem1  17667  tsmsxplem2  17668  tsmsxp  17669  xmetres2  17757  metres2  17759  ressprdsds  17767  xmetresbl  17815  ressxms  17903  nrginvrcn  18034  qtopbaslem  18099  tgqioo  18138  re2ndc  18139  resubmet  18140  xrsdsre  18148  bndth  18288  lebnumii  18296  iscfil2  18524  cmsss  18604  minveclem3a  18623  ovolfioo  18659  ovolficc  18660  ovolficcss  18661  ovolfsf  18663  ovollb  18670  ovolicc2  18713  ovolfs2  18758  uniiccdif  18765  uniioovol  18766  uniiccvol  18767  uniioombllem2  18770  uniioombllem3a  18771  uniioombllem3  18772  uniioombllem4  18773  uniioombllem5  18774  uniioombl  18776  dyadmbllem  18786  opnmbllem  18788  opnmblALT  18790  mbfimaopnlem  18842  itg1addlem4  18886  limccnp2  19074  taylfval  19570  taylf  19572  dvdsmulf1o  20266  fsumdvdsmul  20267  resgrprn  20777  issubgoi  20807  ghgrp  20865  sspg  21134  ssps  21136  sspmlem  21138  issh2  21618  hhssabloi  21669  hhssnv  21671  hhshsslem1  21674  shsel  21723  cvmlift2lem9  23013  cvmlift2lem10  23014  cvmlift2lem11  23015  cvmlift2lem12  23016  ghomfo  23169  residcp  24242  nZdef  24346  svs2  24653  prdnei  24739  limptlimpr2lem2  24741  prismorcsetlem  25078  prismorcset  25080  prismorcsetlemc  25083  pgapspf  25218  ssbnd  25678  prdsbnd2  25685  cnpwstotbnd  25687  reheibor  25729  exidreslem  25733  divrngcl  25754  isdrngo2  25755  dibss  30048
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-in 3085  df-ss 3089  df-opab 3975  df-xp 4594
  Copyright terms: Public domain W3C validator