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

Theorem fss 5532
Description: Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
fss  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )

Proof of Theorem fss
StepHypRef Expression
1 sstr2 3291 . . . . 5  |-  ( ran 
F  C_  B  ->  ( B  C_  C  ->  ran 
F  C_  C )
)
21com12 29 . . . 4  |-  ( B 
C_  C  ->  ( ran  F  C_  B  ->  ran 
F  C_  C )
)
32anim2d 549 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 5391 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5391 . . 3  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
63, 4, 53imtr4g 262 . 2  |-  ( B 
C_  C  ->  ( F : A --> B  ->  F : A --> C ) )
76impcom 420 1  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    C_ wss 3256   ran crn 4812    Fn wfn 5382   -->wf 5383
This theorem is referenced by:  fconst6g  5565  f1ss  5577  ffoss  5640  fsn2  5840  ofco  6256  tposf2  6432  issmo2  6540  smoiso  6553  mapsn  6984  mapss  6985  ssdomg  7082  ac6sfi  7280  infpwfien  7869  alephfplem4  7914  infmap2  8024  cofsmo  8075  fin23lem17  8144  fin23lem32  8150  hsmexlem1  8232  axdc3lem4  8259  ac6s  8290  pwfseqlem4a  8462  gruen  8613  intgru  8615  ingru  8616  1fv  11043  fseq1p1m1  11045  seqf1olem2  11283  hashf1lem1  11624  sswrd  11657  s1cl  11675  limsupgre  12195  abscn2  12312  recn2  12314  imcn2  12315  climabs  12317  climre  12319  climim  12320  rlimabs  12322  rlimre  12324  rlimim  12325  caucvgrlem  12386  caurcvgr  12387  caucvgrlem2  12388  caurcvg  12390  fsumre  12507  fsumim  12508  supcvg  12555  vdwlem8  13276  0ram  13308  ramub1  13316  ramcl  13317  isacs2  13798  funcres2b  14014  acsinfd  14526  acsdomd  14527  resmhm2  14680  gsumress  14697  gsumval1  14699  gsumwsubmcl  14704  gsumws1  14705  prdsgrpd  14847  prdsinvgd  14848  pj1ghm  15255  prdscmnd  15396  prdsabld  15397  gsumval3eu  15433  gsumval3  15434  gsumsubmcl  15444  gsumzadd  15447  gsumzoppg  15459  dprdsn  15514  pgpfaclem1  15559  prdsrngd  15638  prdscrngd  15639  abvf  15831  prdslmodd  15965  psrridm  16388  coe1fval3  16526  zntoslem  16753  frgpcyg  16770  pjdm2  16854  cnrest2  17265  cnprest2  17269  1stcelcls  17438  1stccnp  17439  1stckgen  17500  prdstps  17575  pthaus  17584  txcmplem2  17588  xkoptsub  17600  pt1hmeo  17752  ptcmpfi  17759  ptcmplem1  17997  ptcmpg  18002  prdstmdd  18067  prdstgpd  18068  tsmssubm  18086  ismet2  18265  prdsxmetlem  18299  imasdsf1olem  18304  prdsms  18444  isngp2  18508  metdscn  18750  cncfss  18793  ipcn  19064  lmmbr  19075  causs  19115  equivcau  19117  lmcau  19129  ovolfioo  19224  ovolficc  19225  ovolfsf  19228  elovolm  19231  ovollb  19235  ovolunlem1a  19252  ovolunlem1  19253  ovolicc2lem1  19273  ovolicc2lem2  19274  ovolicc2lem3  19275  ovolicc2lem4  19276  ovolicc2  19278  uniiccdif  19330  uniioovol  19331  uniiccvol  19332  uniioombllem2  19335  uniioombllem3a  19336  uniioombllem3  19337  uniioombllem4  19338  uniioombllem5  19339  uniioombl  19341  dyadmbl  19352  vitalilem3  19362  vitalilem4  19363  vitalilem5  19364  ismbf  19382  mbfid  19388  0plef  19424  i1f1  19442  i1faddlem  19445  i1fmulclem  19454  i1fres  19457  i1fsub  19460  itg1sub  19461  mbfi1fseqlem4  19470  itg2le  19491  itg2mulclem  19498  itg2mulc  19499  itg2monolem1  19502  itg2monolem2  19503  itg2monolem3  19504  itg2mono  19505  itg2i1fseqle  19506  itg2i1fseq3  19509  itg2addlem  19510  itg2gt0  19512  itg2cnlem1  19513  itg2cnlem2  19514  limccnp  19638  dvcmulf  19691  dvcobr  19692  dvfre  19697  dvnfre  19698  dvcnvlem  19720  dvcnv  19721  dvef  19724  dvferm1  19729  dvferm2  19731  rolle  19734  dvgt0lem1  19746  dvivthlem1  19752  dvne0  19755  lhop1lem  19757  lhop2  19759  lhop  19760  dvcnvrelem1  19761  dvcnvre  19763  dvcvx  19764  dvfsumrlim  19775  tdeglem3  19842  elply2  19975  elplyr  19980  plyeq0lem  19989  plyaddlem  19994  plymullem  19995  dgrlem  20008  coeidlem  20016  taylthlem2  20150  taylth  20151  ulmcn  20175  iblulm  20183  efcvx  20225  dvrelog  20388  relogcn  20389  dvlog2  20404  leibpi  20642  efrlim  20668  jensenlem2  20686  jensen  20687  amgmlem  20688  amgm  20689  wilthlem2  20712  wilthlem3  20713  basellem7  20729  basellem9  20731  lgsfcl  20948  lgsdchr  20992  dchrvmasumlem1  21049  dchrisum0lem3  21073  umgra1  21221  umisuhgra  21222  constr1trl  21429  constr2trl  21439  constr3trllem1  21478  constr3trllem3  21480  eupa0  21537  eupap1  21539  0oo  22131  minvecolem3  22219  minvecolem4  22223  hhsscms  22620  occllem  22646  chscllem2  22981  chscllem4  22983  pjhf  23051  nlelchi  23405  hmopidmchi  23495  pjinvari  23535  lmlim  24130  rge0scvg  24132  lmdvg  24135  lmdvglim  24136  rrhre  24176  esumsn  24245  esumfsupre  24250  hashf2  24263  coinfliprv  24512  ptpcon  24692  fprb  25146  axlowdimlem4  25591  axlowdimlem7  25594  axlowdimlem10  25597  itg2addnclem  25950  itg2addnclem2  25951  itg2addnc  25952  itg2gt0cn  25953  fdc  26133  heiborlem6  26209  heibor  26214  ralxpmap  26426  ismrc  26439  mapfzcons  26456  mzpexpmpt  26486  mzpresrename  26491  diophrw  26501  rabren3dioph  26560  pwssplit1  26850  pwssplit4  26853  dsmmsubg  26871  dsmmlss  26872  islinds2  26945  lindsmm  26960  lsslindf  26962  lnrfg  26985  symgtrinv  27075  seff  27200  sblpnf  27201  climreeq  27400  stoweidlem39  27449  stoweidlem44  27454  stoweidlem59  27469  stirlinglem8  27491  lfl0f  29235  dochpolN  31656
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-in 3263  df-ss 3270  df-f 5391
  Copyright terms: Public domain W3C validator