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

Theorem fss 5397
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 3186 . . . . 5  |-  ( ran 
F  C_  B  ->  ( B  C_  C  ->  ran 
F  C_  C )
)
21com12 27 . . . 4  |-  ( B 
C_  C  ->  ( ran  F  C_  B  ->  ran 
F  C_  C )
)
32anim2d 548 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 5259 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5259 . . 3  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
63, 4, 53imtr4g 261 . 2  |-  ( B 
C_  C  ->  ( F : A --> B  ->  F : A --> C ) )
76impcom 419 1  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    C_ wss 3152   ran crn 4690    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  fconst6g  5430  f1ss  5442  ffoss  5505  fsn2  5698  ofco  6097  tposf2  6258  issmo2  6366  smoiso  6379  mapsn  6809  mapss  6810  ssdomg  6907  ac6sfi  7101  infpwfien  7689  alephfplem4  7734  infmap2  7844  cofsmo  7895  fin23lem17  7964  fin23lem32  7970  hsmexlem1  8052  axdc3lem4  8079  ac6s  8111  pwfseqlem4a  8283  gruen  8434  intgru  8436  ingru  8437  fseq1p1m1  10857  seqf1olem2  11086  hashf1lem1  11393  sswrd  11423  s1cl  11441  limsupgre  11955  abscn2  12072  recn2  12074  imcn2  12075  climabs  12077  climre  12079  climim  12080  rlimabs  12082  rlimre  12084  rlimim  12085  caucvgrlem  12145  caurcvgr  12146  caucvgrlem2  12147  caurcvg  12149  fsumre  12266  fsumim  12267  supcvg  12314  vdwlem8  13035  0ram  13067  ramub1  13075  ramcl  13076  isacs2  13555  funcres2b  13771  acsinfd  14283  acsdomd  14284  resmhm2  14437  gsumress  14454  gsumval1  14456  gsumwsubmcl  14461  gsumws1  14462  prdsgrpd  14604  prdsinvgd  14605  pj1ghm  15012  prdscmnd  15153  prdsabld  15154  gsumval3eu  15190  gsumval3  15191  gsumsubmcl  15201  gsumzadd  15204  gsumzoppg  15216  dprdsn  15271  pgpfaclem1  15316  prdsrngd  15395  prdscrngd  15396  abvf  15588  prdslmodd  15726  psrridm  16149  coe1fval3  16289  zntoslem  16510  frgpcyg  16527  pjdm2  16611  cnrest2  17014  cnprest2  17018  1stcelcls  17187  1stccnp  17188  1stckgen  17249  prdstps  17323  pthaus  17332  txcmplem2  17336  xkoptsub  17348  pt1hmeo  17497  ptcmpfi  17504  ptcmplem1  17746  ptcmpg  17751  prdstmdd  17806  prdstgpd  17807  tsmssubm  17825  ismet2  17898  prdsxmetlem  17932  imasdsf1olem  17937  prdsms  18077  isngp2  18119  metdscn  18360  cncfss  18403  ipcn  18673  lmmbr  18684  causs  18724  equivcau  18726  lmcau  18738  ovolfioo  18827  ovolficc  18828  ovolfsf  18831  elovolm  18834  ovollb  18838  ovolunlem1a  18855  ovolunlem1  18856  ovolicc2lem1  18876  ovolicc2lem2  18877  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2  18881  uniiccdif  18933  uniioovol  18934  uniiccvol  18935  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombl  18944  dyadmbl  18955  vitalilem3  18965  vitalilem4  18966  vitalilem5  18967  ismbf  18985  mbfid  18991  0plef  19027  i1f1  19045  i1faddlem  19048  i1fmulclem  19057  i1fres  19060  i1fsub  19063  itg1sub  19064  mbfi1fseqlem4  19073  itg2le  19094  itg2mulclem  19101  itg2mulc  19102  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq3  19112  itg2addlem  19113  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  limccnp  19241  dvcmulf  19294  dvcobr  19295  dvfre  19300  dvnfre  19301  dvcnvlem  19323  dvcnv  19324  dvef  19327  dvferm1  19332  dvferm2  19334  rolle  19337  dvgt0lem1  19349  dvivthlem1  19355  dvne0  19358  lhop1lem  19360  lhop2  19362  lhop  19363  dvcnvrelem1  19364  dvcnvre  19366  dvcvx  19367  dvfsumrlim  19378  tdeglem3  19445  elply2  19578  elplyr  19583  plyeq0lem  19592  plyaddlem  19597  plymullem  19598  dgrlem  19611  coeidlem  19619  taylthlem2  19753  taylth  19754  ulmcn  19776  iblulm  19783  efcvx  19825  dvrelog  19984  relogcn  19985  dvlog2  20000  leibpi  20238  efrlim  20264  jensenlem2  20282  jensen  20283  amgmlem  20284  amgm  20285  wilthlem2  20307  wilthlem3  20308  basellem7  20324  basellem9  20326  lgsfcl  20543  lgsdchr  20587  dchrvmasumlem1  20644  dchrisum0lem3  20668  0oo  21367  minvecolem3  21455  minvecolem4  21459  hhsscms  21856  occllem  21882  chscllem2  22217  chscllem4  22219  pjhf  22287  nlelchi  22641  hmopidmchi  22731  pjinvari  22771  lmlim  23371  rge0scvg  23373  lmdvg  23376  lmdvglim  23377  esumsn  23437  hashf2  23452  coinfliprv  23683  ptpcon  23764  umgra1  23878  eupa0  23898  eupap1  23900  fprb  24129  axlowdimlem4  24573  axlowdimlem7  24576  axlowdimlem10  24579  cbicp  25166  domrancur1c  25202  istopxc  25548  claddrvr  25648  rnegvex2  25661  negveudr  25669  clsmulrv  25683  divclrvd  25695  idsubfun  25858  1iskle  25989  phckle  26027  psckle  26028  pgapspf  26052  pgapspf2  26053  fdc  26455  heiborlem6  26540  heibor  26545  ralxpmap  26761  ismrc  26776  mapfzcons  26793  mzpexpmpt  26823  mzpresrename  26828  diophrw  26838  rabren3dioph  26898  pwssplit1  27188  pwssplit4  27191  dsmmsubg  27209  dsmmlss  27210  islinds2  27283  lindsmm  27298  lsslindf  27300  lnrfg  27323  symgtrinv  27413  seff  27538  sblpnf  27539  climreeq  27739  stoweidlem39  27788  stoweidlem44  27793  stoweidlem59  27808  stirlinglem8  27830  lfl0f  29259  dochpolN  31680
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-f 5259
  Copyright terms: Public domain W3C validator