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

Theorem xpss12 4972
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 3334 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3334 . . . 4  |-  ( C 
C_  D  ->  (
y  e.  C  -> 
y  e.  D ) )
31, 2im2anan9 809 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  D )
) )
43ssopab2dv 4475 . 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 4875 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4875 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3381 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 359    e. wcel 1725    C_ wss 3312   {copab 4257    X. cxp 4867
This theorem is referenced by:  xpss  4973  xpss1  4975  xpss2  4976  djussxp  5009  ssxpb  5294  ssrnres  5300  cossxp  5383  relrelss  5384  fssxp  5593  oprabss  6150  pmss12g  7031  marypha1lem  7429  marypha2lem1  7431  hartogslem1  7500  infxpenlem  7884  dfac5lem4  7996  axdc4lem  8324  fpwwe2lem1  8495  fpwwe2lem11  8504  fpwwe2lem12  8505  fpwwe2lem13  8506  canthwe  8515  tskxpss  8636  dmaddpi  8756  dmmulpi  8757  addnqf  8814  mulnqf  8815  ltrelxr  9128  mulnzcnopr  9657  dfz2  10288  elq  10565  leiso  11696  xpnnenOLD  12797  znnen  12800  eucalg  13066  phimullem  13156  imasless  13753  sscpwex  14003  fullsubc  14035  fullresc  14036  wunfunc  14084  funcres2c  14086  homaf  14173  dmcoass  14209  catcoppccl  14251  catcfuccl  14252  catcxpccl  14292  znleval  16823  txuni2  17585  txbas  17587  txcld  17623  txcls  17624  neitx  17627  txcnp  17640  txlly  17656  txnlly  17657  hausdiag  17665  tx1stc  17670  txkgen  17672  xkococnlem  17679  cnmpt2res  17697  clssubg  18126  tsmsxplem1  18170  tsmsxplem2  18171  tsmsxp  18172  trust  18247  ustuqtop1  18259  psmetres2  18333  xmetres2  18379  metres2  18381  ressprdsds  18389  xmetresbl  18455  ressxms  18543  metustexhalfOLD  18581  metustexhalf  18582  cfilucfilOLD  18587  cfilucfil  18588  restmetu  18605  nrginvrcn  18715  qtopbaslem  18780  tgqioo  18819  re2ndc  18820  resubmet  18821  xrsdsre  18829  bndth  18971  lebnumii  18979  iscfil2  19207  cmsss  19291  minveclem3a  19316  ovolfioo  19352  ovolficc  19353  ovolficcss  19354  ovolfsf  19356  ovollb  19363  ovolicc2  19406  ovolfs2  19451  uniiccdif  19458  uniioovol  19459  uniiccvol  19460  uniioombllem2  19463  uniioombllem3a  19464  uniioombllem3  19465  uniioombllem4  19466  uniioombllem5  19467  uniioombl  19469  dyadmbllem  19479  opnmbllem  19481  opnmblALT  19483  mbfimaopnlem  19535  itg1addlem4  19579  limccnp2  19767  taylfval  20263  taylf  20265  dvdsmulf1o  20967  fsumdvdsmul  20968  resgrprn  21856  issubgoi  21886  ghgrp  21944  sspg  22215  ssps  22217  sspmlem  22219  issh2  22699  hhssabloi  22750  hhssnv  22752  hhshsslem1  22755  shsel  22804  ofrn2  24041  gtiso  24076  xrofsup  24114  tpr2rico  24298  raddcn  24303  xrge0pluscn  24314  br2base  24607  dya2iocnrect  24619  dya2iocucvr  24622  cvmlift2lem9  24986  cvmlift2lem10  24987  cvmlift2lem11  24988  cvmlift2lem12  24989  ghomfo  25090  mblfinlem  26190  ssbnd  26434  prdsbnd2  26441  cnpwstotbnd  26443  reheibor  26485  exidreslem  26489  divrngcl  26510  isdrngo2  26511  dibss  31806
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-in 3319  df-ss 3326  df-opab 4259  df-xp 4875
  Copyright terms: Public domain W3C validator