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

Theorem xpss12 5106
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 3498 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3498 . . . 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 4776 . 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 5005 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 5005 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3545 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 1767    C_ wss 3476   {copab 4504    X. cxp 4997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3483  df-ss 3490  df-opab 4506  df-xp 5005
This theorem is referenced by:  xpss  5107  xpss1  5109  xpss2  5110  djussxp  5146  ssxpb  5439  ssrnres  5443  cossxp  5528  relrelss  5529  fssxp  5741  oprabss  6370  pmss12g  7442  marypha1lem  7889  marypha2lem1  7891  hartogslem1  7963  infxpenlem  8387  dfac5lem4  8503  axdc4lem  8831  fpwwe2lem1  9005  fpwwe2lem11  9014  fpwwe2lem12  9015  fpwwe2lem13  9016  canthwe  9025  tskxpss  9146  dmaddpi  9264  dmmulpi  9265  addnqf  9322  mulnqf  9323  rexpssxrxp  9634  ltrelxr  9644  mulnzcnopr  10191  dfz2  10878  elq  11180  leiso  12470  xpnnenOLD  13800  znnen  13803  eucalg  14071  phimullem  14164  imasless  14791  sscpwex  15041  fullsubc  15073  fullresc  15074  wunfunc  15122  funcres2c  15124  homaf  15211  dmcoass  15247  catcoppccl  15289  catcfuccl  15290  catcxpccl  15330  znleval  18360  txuni2  19801  txbas  19803  txcld  19839  txcls  19840  neitx  19843  txcnp  19856  txlly  19872  txnlly  19873  hausdiag  19881  tx1stc  19886  txkgen  19888  xkococnlem  19895  cnmpt2res  19913  clssubg  20342  tsmsxplem1  20390  tsmsxplem2  20391  tsmsxp  20392  trust  20467  ustuqtop1  20479  psmetres2  20553  xmetres2  20599  metres2  20601  ressprdsds  20609  xmetresbl  20675  ressxms  20763  metustexhalfOLD  20801  metustexhalf  20802  cfilucfilOLD  20807  cfilucfil  20808  restmetu  20825  nrginvrcn  20935  qtopbaslem  21000  tgqioo  21040  re2ndc  21041  resubmet  21042  xrsdsre  21050  bndth  21193  lebnumii  21201  iscfil2  21440  cmsss  21524  minveclem3a  21577  ovolfsf  21618  opnmblALT  21747  mbfimaopnlem  21797  itg1addlem4  21841  limccnp2  22031  taylfval  22488  taylf  22490  dvdsmulf1o  23198  fsumdvdsmul  23199  resgrprn  24958  issubgoi  24988  ghgrp  25046  sspg  25317  ssps  25319  sspmlem  25321  issh2  25802  hhssabloi  25854  hhssnv  25856  hhshsslem1  25859  shsel  25908  ofrn2  27153  gtiso  27191  xrofsup  27250  fimaproj  27499  txomap  27500  tpr2rico  27530  prsss  27534  ordtrestNEW  27539  raddcn  27547  xrge0pluscn  27558  br2base  27880  dya2iocnrect  27892  dya2iocucvr  27895  eulerpartlemgh  27957  eulerpartlemgs2  27959  cvmlift2lem9  28396  cvmlift2lem10  28397  cvmlift2lem11  28398  cvmlift2lem12  28399  ghomfo  28506  mblfinlem2  29629  ftc1anc  29675  ssbnd  29887  prdsbnd2  29894  cnpwstotbnd  29896  reheibor  29938  exidreslem  29942  divrngcl  29963  isdrngo2  29964  arearect  30788  fourierdlem42  31449  dibss  35966  rp-imass  36796
  Copyright terms: Public domain W3C validator