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

Theorem xpss12 4902
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 3401 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3401 . . . 4  |-  ( C 
C_  D  ->  (
y  e.  C  -> 
y  e.  D ) )
31, 2im2anan9 843 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  D )
) )
43ssopab2dv 4692 . 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 4802 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4802 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3448 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 370    e. wcel 1872    C_ wss 3379   {copab 4424    X. cxp 4794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-in 3386  df-ss 3393  df-opab 4426  df-xp 4802
This theorem is referenced by:  xpss  4903  xpss1  4905  xpss2  4906  djussxp  4942  ssxpb  5233  ssrnres  5237  cossxp  5320  relrelss  5321  fssxp  5701  oprabss  6340  pmss12g  7453  marypha1lem  7900  marypha2lem1  7902  hartogslem1  8010  infxpenlem  8396  dfac5lem4  8508  axdc4lem  8836  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  10209  dfz2  10906  elq  11217  leiso  12570  znnen  14208  eucalg  14489  phimullem  14670  imasless  15389  sscpwex  15663  fullsubc  15698  fullresc  15699  wunfunc  15747  funcres2c  15749  homaf  15868  dmcoass  15904  catcoppccl  15946  catcfuccl  15947  catcxpccl  16035  znleval  19067  txuni2  20522  txbas  20524  txcld  20560  txcls  20561  neitx  20564  txcnp  20577  txlly  20593  txnlly  20594  hausdiag  20602  tx1stc  20607  txkgen  20609  xkococnlem  20616  cnmpt2res  20634  clssubg  21065  tsmsxplem1  21109  tsmsxplem2  21110  tsmsxp  21111  trust  21186  ustuqtop1  21198  psmetres2  21272  xmetres2  21318  metres2  21320  ressprdsds  21328  xmetresbl  21394  ressxms  21482  metustexhalf  21513  cfilucfil  21516  restmetu  21527  nrginvrcn  21636  qtopbaslem  21721  tgqioo  21760  re2ndc  21761  resubmet  21762  xrsdsre  21770  bndth  21928  lebnumii  21939  iscfil2  22178  cmsss  22260  minveclem3a  22311  minveclem3aOLD  22323  ovolfsf  22366  opnmblALT  22503  mbfimaopnlem  22553  itg1addlem4  22599  limccnp2  22789  taylfval  23256  taylf  23258  dvdsmulf1o  24065  fsumdvdsmul  24066  resgrprn  25950  issubgoi  25980  ghgrpOLD  26038  sspg  26309  ssps  26311  sspmlem  26313  issh2  26804  hhssabloi  26855  hhssnv  26857  hhshsslem1  26860  shsel  26909  ofrn2  28187  gtiso  28227  xrofsup  28303  fimaproj  28612  txomap  28613  tpr2rico  28670  prsss  28674  raddcn  28687  xrge0pluscn  28698  br2base  29043  dya2iocnrect  29055  dya2iocucvr  29058  eulerpartlemgh  29163  eulerpartlemgs2  29165  cvmlift2lem9  29986  cvmlift2lem10  29987  cvmlift2lem11  29988  cvmlift2lem12  29989  mpstssv  30129  ghomfo  30261  elxp8  31681  mblfinlem2  31885  ftc1anc  31932  ssbnd  32027  prdsbnd2  32034  cnpwstotbnd  32036  reheibor  32078  exidreslem  32082  divrngcl  32103  isdrngo2  32104  dibss  34649  arearect  36013  rtrclex  36137  rtrclexi  36141  rp-imass  36279  idhe  36296  fourierdlem42  37895  fourierdlem42OLD  37896  rnghmresfn  39566  rnghmsscmap2  39576  rnghmsscmap  39577  rhmresfn  39612  rhmsscmap2  39622  rhmsscmap  39623  rhmsscrnghm  39629  rngcrescrhm  39688  rngcrescrhmALTV  39707
  Copyright terms: Public domain W3C validator