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

Theorem xpss12 5094
Description: Subset theorem for Cartesian 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 3480 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3480 . . . 4  |-  ( C 
C_  D  ->  (
y  e.  C  -> 
y  e.  D ) )
31, 2im2anan9 833 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  D )
) )
43ssopab2dv 4762 . 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 4991 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4991 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3527 1  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  X.  C
)  C_  ( B  X.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1802    C_ wss 3458   {copab 4490    X. cxp 4983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-in 3465  df-ss 3472  df-opab 4492  df-xp 4991
This theorem is referenced by:  xpss  5095  xpss1  5097  xpss2  5098  djussxp  5134  ssxpb  5427  ssrnres  5431  cossxp  5516  relrelss  5517  fssxp  5729  oprabss  6369  pmss12g  7443  marypha1lem  7891  marypha2lem1  7893  hartogslem1  7965  infxpenlem  8389  dfac5lem4  8505  axdc4lem  8833  fpwwe2lem1  9007  fpwwe2lem11  9016  fpwwe2lem12  9017  fpwwe2lem13  9018  canthwe  9027  tskxpss  9148  dmaddpi  9266  dmmulpi  9267  addnqf  9324  mulnqf  9325  rexpssxrxp  9636  ltrelxr  9646  mulnzcnopr  10196  dfz2  10883  elq  11188  leiso  12482  xpnnenOLD  13815  znnen  13818  eucalg  14088  phimullem  14181  imasless  14809  sscpwex  15056  fullsubc  15088  fullresc  15089  wunfunc  15137  funcres2c  15139  homaf  15226  dmcoass  15262  catcoppccl  15304  catcfuccl  15305  catcxpccl  15345  znleval  18460  txuni2  19932  txbas  19934  txcld  19970  txcls  19971  neitx  19974  txcnp  19987  txlly  20003  txnlly  20004  hausdiag  20012  tx1stc  20017  txkgen  20019  xkococnlem  20026  cnmpt2res  20044  clssubg  20473  tsmsxplem1  20521  tsmsxplem2  20522  tsmsxp  20523  trust  20598  ustuqtop1  20610  psmetres2  20684  xmetres2  20730  metres2  20732  ressprdsds  20740  xmetresbl  20806  ressxms  20894  metustexhalfOLD  20932  metustexhalf  20933  cfilucfilOLD  20938  cfilucfil  20939  restmetu  20956  nrginvrcn  21066  qtopbaslem  21131  tgqioo  21171  re2ndc  21172  resubmet  21173  xrsdsre  21181  bndth  21324  lebnumii  21332  iscfil2  21571  cmsss  21655  minveclem3a  21708  ovolfsf  21749  opnmblALT  21878  mbfimaopnlem  21928  itg1addlem4  21972  limccnp2  22162  taylfval  22619  taylf  22621  dvdsmulf1o  23335  fsumdvdsmul  23336  resgrprn  25147  issubgoi  25177  ghgrpOLD  25235  sspg  25506  ssps  25508  sspmlem  25510  issh2  25991  hhssabloi  26043  hhssnv  26045  hhshsslem1  26048  shsel  26097  ofrn2  27345  gtiso  27384  xrofsup  27447  fimaproj  27702  txomap  27703  tpr2rico  27760  prsss  27764  raddcn  27777  xrge0pluscn  27788  br2base  28106  dya2iocnrect  28118  dya2iocucvr  28121  eulerpartlemgh  28183  eulerpartlemgs2  28185  cvmlift2lem9  28622  cvmlift2lem10  28623  cvmlift2lem11  28624  cvmlift2lem12  28625  mpstssv  28765  ghomfo  28897  mblfinlem2  30020  ftc1anc  30066  ssbnd  30252  prdsbnd2  30259  cnpwstotbnd  30261  reheibor  30303  exidreslem  30307  divrngcl  30328  isdrngo2  30329  arearect  31152  fourierdlem42  31816  rnghmresfn  32490  rnghmsscmap2  32500  rnghmsscmap  32501  rhmresfn  32530  rhmsscmap2  32540  rhmsscmap  32541  rhmsscrnghm  32547  rngcrescrhm  32601  rngcrescrhmOLD  32620  dibss  36598  rp-imass  37444
  Copyright terms: Public domain W3C validator