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

Theorem xpss12 4950
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 3355 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3355 . . . 4  |-  ( C 
C_  D  ->  (
y  e.  C  -> 
y  e.  D ) )
31, 2im2anan9 831 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  D )
) )
43ssopab2dv 4622 . 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 4851 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4851 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3402 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 1756    C_ wss 3333   {copab 4354    X. cxp 4843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-in 3340  df-ss 3347  df-opab 4356  df-xp 4851
This theorem is referenced by:  xpss  4951  xpss1  4953  xpss2  4954  djussxp  4990  ssxpb  5277  ssrnres  5281  cossxp  5365  relrelss  5366  fssxp  5575  oprabss  6181  pmss12g  7244  marypha1lem  7688  marypha2lem1  7690  hartogslem1  7761  infxpenlem  8185  dfac5lem4  8301  axdc4lem  8629  fpwwe2lem1  8803  fpwwe2lem11  8812  fpwwe2lem12  8813  fpwwe2lem13  8814  canthwe  8823  tskxpss  8944  dmaddpi  9064  dmmulpi  9065  addnqf  9122  mulnqf  9123  rexpssxrxp  9433  ltrelxr  9443  mulnzcnopr  9987  dfz2  10669  elq  10960  leiso  12217  xpnnenOLD  13497  znnen  13500  eucalg  13767  phimullem  13859  imasless  14483  sscpwex  14733  fullsubc  14765  fullresc  14766  wunfunc  14814  funcres2c  14816  homaf  14903  dmcoass  14939  catcoppccl  14981  catcfuccl  14982  catcxpccl  15022  znleval  17992  txuni2  19143  txbas  19145  txcld  19181  txcls  19182  neitx  19185  txcnp  19198  txlly  19214  txnlly  19215  hausdiag  19223  tx1stc  19228  txkgen  19230  xkococnlem  19237  cnmpt2res  19255  clssubg  19684  tsmsxplem1  19732  tsmsxplem2  19733  tsmsxp  19734  trust  19809  ustuqtop1  19821  psmetres2  19895  xmetres2  19941  metres2  19943  ressprdsds  19951  xmetresbl  20017  ressxms  20105  metustexhalfOLD  20143  metustexhalf  20144  cfilucfilOLD  20149  cfilucfil  20150  restmetu  20167  nrginvrcn  20277  qtopbaslem  20342  tgqioo  20382  re2ndc  20383  resubmet  20384  xrsdsre  20392  bndth  20535  lebnumii  20543  iscfil2  20782  cmsss  20866  minveclem3a  20919  ovolfsf  20960  opnmblALT  21088  mbfimaopnlem  21138  itg1addlem4  21182  limccnp2  21372  taylfval  21829  taylf  21831  dvdsmulf1o  22539  fsumdvdsmul  22540  resgrprn  23772  issubgoi  23802  ghgrp  23860  sspg  24131  ssps  24133  sspmlem  24135  issh2  24616  hhssabloi  24668  hhssnv  24670  hhshsslem1  24673  shsel  24722  ofrn2  25963  gtiso  26001  xrofsup  26060  tpr2rico  26347  prsss  26351  ordtrestNEW  26356  raddcn  26364  xrge0pluscn  26375  br2base  26689  dya2iocnrect  26701  dya2iocucvr  26704  eulerpartlemgh  26766  eulerpartlemgs2  26768  cvmlift2lem9  27205  cvmlift2lem10  27206  cvmlift2lem11  27207  cvmlift2lem12  27208  ghomfo  27315  mblfinlem2  28434  ftc1anc  28480  ssbnd  28692  prdsbnd2  28699  cnpwstotbnd  28701  reheibor  28743  exidreslem  28747  divrngcl  28768  isdrngo2  28769  arearect  29596  dibss  34819
  Copyright terms: Public domain W3C validator