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

Theorem xpss12 4932
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 3338 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3338 . . . 4  |-  ( C 
C_  D  ->  (
y  e.  C  -> 
y  e.  D ) )
31, 2im2anan9 824 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  D )
) )
43ssopab2dv 4606 . 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 4833 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4833 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3385 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 1755    C_ wss 3316   {copab 4337    X. cxp 4825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-in 3323  df-ss 3330  df-opab 4339  df-xp 4833
This theorem is referenced by:  xpss  4933  xpss1  4935  xpss2  4936  djussxp  4972  ssxpb  5260  ssrnres  5264  cossxp  5348  relrelss  5349  fssxp  5558  oprabss  6165  pmss12g  7227  marypha1lem  7671  marypha2lem1  7673  hartogslem1  7744  infxpenlem  8168  dfac5lem4  8284  axdc4lem  8612  fpwwe2lem1  8785  fpwwe2lem11  8794  fpwwe2lem12  8795  fpwwe2lem13  8796  canthwe  8805  tskxpss  8926  dmaddpi  9046  dmmulpi  9047  addnqf  9104  mulnqf  9105  rexpssxrxp  9415  ltrelxr  9425  mulnzcnopr  9969  dfz2  10651  elq  10942  leiso  12195  xpnnenOLD  13474  znnen  13477  eucalg  13744  phimullem  13836  imasless  14460  sscpwex  14710  fullsubc  14742  fullresc  14743  wunfunc  14791  funcres2c  14793  homaf  14880  dmcoass  14916  catcoppccl  14958  catcfuccl  14959  catcxpccl  14999  znleval  17828  txuni2  18979  txbas  18981  txcld  19017  txcls  19018  neitx  19021  txcnp  19034  txlly  19050  txnlly  19051  hausdiag  19059  tx1stc  19064  txkgen  19066  xkococnlem  19073  cnmpt2res  19091  clssubg  19520  tsmsxplem1  19568  tsmsxplem2  19569  tsmsxp  19570  trust  19645  ustuqtop1  19657  psmetres2  19731  xmetres2  19777  metres2  19779  ressprdsds  19787  xmetresbl  19853  ressxms  19941  metustexhalfOLD  19979  metustexhalf  19980  cfilucfilOLD  19985  cfilucfil  19986  restmetu  20003  nrginvrcn  20113  qtopbaslem  20178  tgqioo  20218  re2ndc  20219  resubmet  20220  xrsdsre  20228  bndth  20371  lebnumii  20379  iscfil2  20618  cmsss  20702  minveclem3a  20755  ovolfsf  20796  opnmblALT  20924  mbfimaopnlem  20974  itg1addlem4  21018  limccnp2  21208  taylfval  21708  taylf  21710  dvdsmulf1o  22418  fsumdvdsmul  22419  resgrprn  23589  issubgoi  23619  ghgrp  23677  sspg  23948  ssps  23950  sspmlem  23952  issh2  24433  hhssabloi  24485  hhssnv  24487  hhshsslem1  24490  shsel  24539  ofrn2  25781  gtiso  25819  xrofsup  25877  tpr2rico  26195  prsss  26199  ordtrestNEW  26204  raddcn  26212  xrge0pluscn  26223  br2base  26537  dya2iocnrect  26549  dya2iocucvr  26552  eulerpartlemgh  26608  eulerpartlemgs2  26610  cvmlift2lem9  27047  cvmlift2lem10  27048  cvmlift2lem11  27049  cvmlift2lem12  27050  ghomfo  27156  mblfinlem2  28270  ftc1anc  28316  ssbnd  28528  prdsbnd2  28535  cnpwstotbnd  28537  reheibor  28579  exidreslem  28583  divrngcl  28604  isdrngo2  28605  arearect  29433  dibss  34384
  Copyright terms: Public domain W3C validator