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

Theorem xpss12 4940
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 3302 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3302 . . . 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 4443 . 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 4843 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4843 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3349 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 1721    C_ wss 3280   {copab 4225    X. cxp 4835
This theorem is referenced by:  xpss  4941  xpss1  4943  xpss2  4944  djussxp  4977  ssxpb  5262  ssrnres  5268  cossxp  5351  relrelss  5352  fssxp  5561  oprabss  6118  pmss12g  6999  marypha1lem  7396  marypha2lem1  7398  hartogslem1  7467  infxpenlem  7851  dfac5lem4  7963  axdc4lem  8291  fpwwe2lem1  8462  fpwwe2lem11  8471  fpwwe2lem12  8472  fpwwe2lem13  8473  canthwe  8482  tskxpss  8603  dmaddpi  8723  dmmulpi  8724  addnqf  8781  mulnqf  8782  ltrelxr  9095  mulnzcnopr  9624  dfz2  10255  elq  10532  leiso  11663  xpnnenOLD  12764  znnen  12767  eucalg  13033  phimullem  13123  imasless  13720  sscpwex  13970  fullsubc  14002  fullresc  14003  wunfunc  14051  funcres2c  14053  homaf  14140  dmcoass  14176  catcoppccl  14218  catcfuccl  14219  catcxpccl  14259  znleval  16790  txuni2  17550  txbas  17552  txcld  17588  txcls  17589  neitx  17592  txcnp  17605  txlly  17621  txnlly  17622  hausdiag  17630  tx1stc  17635  txkgen  17637  xkococnlem  17644  cnmpt2res  17662  clssubg  18091  tsmsxplem1  18135  tsmsxplem2  18136  tsmsxp  18137  trust  18212  ustuqtop1  18224  psmetres2  18298  xmetres2  18344  metres2  18346  ressprdsds  18354  xmetresbl  18420  ressxms  18508  metustexhalfOLD  18546  metustexhalf  18547  cfilucfilOLD  18552  cfilucfil  18553  restmetu  18570  nrginvrcn  18680  qtopbaslem  18745  tgqioo  18784  re2ndc  18785  resubmet  18786  xrsdsre  18794  bndth  18936  lebnumii  18944  iscfil2  19172  cmsss  19256  minveclem3a  19281  ovolfioo  19317  ovolficc  19318  ovolficcss  19319  ovolfsf  19321  ovollb  19328  ovolicc2  19371  ovolfs2  19416  uniiccdif  19423  uniioovol  19424  uniiccvol  19425  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombl  19434  dyadmbllem  19444  opnmbllem  19446  opnmblALT  19448  mbfimaopnlem  19500  itg1addlem4  19544  limccnp2  19732  taylfval  20228  taylf  20230  dvdsmulf1o  20932  fsumdvdsmul  20933  resgrprn  21821  issubgoi  21851  ghgrp  21909  sspg  22180  ssps  22182  sspmlem  22184  issh2  22664  hhssabloi  22715  hhssnv  22717  hhshsslem1  22720  shsel  22769  ofrn2  24006  gtiso  24041  xrofsup  24079  tpr2rico  24263  raddcn  24268  xrge0pluscn  24279  br2base  24572  dya2iocnrect  24584  dya2iocucvr  24587  cvmlift2lem9  24951  cvmlift2lem10  24952  cvmlift2lem11  24953  cvmlift2lem12  24954  ghomfo  25055  mblfinlem  26143  ssbnd  26387  prdsbnd2  26394  cnpwstotbnd  26396  reheibor  26438  exidreslem  26442  divrngcl  26463  isdrngo2  26464  dibss  31652
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-in 3287  df-ss 3294  df-opab 4227  df-xp 4843
  Copyright terms: Public domain W3C validator