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

Theorem fss 5558
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 3315 . . . . 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 5417 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5417 . . 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 3280   ran crn 4838    Fn wfn 5408   -->wf 5409
This theorem is referenced by:  fconst6g  5591  f1ss  5603  ffoss  5666  fsn2  5867  ofco  6283  tposf2  6462  issmo2  6570  smoiso  6583  mapsn  7014  mapss  7015  ssdomg  7112  ac6sfi  7310  infpwfien  7899  alephfplem4  7944  infmap2  8054  cofsmo  8105  fin23lem17  8174  fin23lem32  8180  hsmexlem1  8262  axdc3lem4  8289  ac6s  8320  pwfseqlem4a  8492  gruen  8643  intgru  8645  ingru  8646  1fv  11075  fseq1p1m1  11077  seqf1olem2  11318  hashf1lem1  11659  sswrd  11692  s1cl  11710  limsupgre  12230  abscn2  12347  recn2  12349  imcn2  12350  climabs  12352  climre  12354  climim  12355  rlimabs  12357  rlimre  12359  rlimim  12360  caucvgrlem  12421  caurcvgr  12422  caucvgrlem2  12423  caurcvg  12425  fsumre  12542  fsumim  12543  supcvg  12590  vdwlem8  13311  0ram  13343  ramub1  13351  ramcl  13352  isacs2  13833  funcres2b  14049  acsinfd  14561  acsdomd  14562  resmhm2  14715  gsumress  14732  gsumval1  14734  gsumwsubmcl  14739  gsumws1  14740  prdsgrpd  14882  prdsinvgd  14883  pj1ghm  15290  prdscmnd  15431  prdsabld  15432  gsumval3eu  15468  gsumval3  15469  gsumsubmcl  15479  gsumzadd  15482  gsumzoppg  15494  dprdsn  15549  pgpfaclem1  15594  prdsrngd  15673  prdscrngd  15674  abvf  15866  prdslmodd  16000  psrridm  16423  coe1fval3  16561  zntoslem  16792  frgpcyg  16809  pjdm2  16893  cnrest2  17304  cnprest2  17308  1stcelcls  17477  1stccnp  17478  1stckgen  17539  prdstps  17614  pthaus  17623  txcmplem2  17627  xkoptsub  17639  pt1hmeo  17791  ptcmpfi  17798  ptcmplem1  18036  ptcmpg  18041  prdstmdd  18106  prdstgpd  18107  tsmssubm  18125  ismet2  18316  prdsxmetlem  18351  imasdsf1olem  18356  prdsms  18514  isngp2  18597  metdscn  18839  cncfss  18882  ipcn  19153  lmmbr  19164  causs  19204  equivcau  19206  lmcau  19218  ovolfioo  19317  ovolficc  19318  ovolfsf  19321  elovolm  19324  ovollb  19328  ovolunlem1a  19345  ovolunlem1  19346  ovolicc2lem1  19366  ovolicc2lem2  19367  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2  19371  uniiccdif  19423  uniioovol  19424  uniiccvol  19425  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombl  19434  dyadmbl  19445  vitalilem3  19455  vitalilem4  19456  vitalilem5  19457  ismbf  19475  mbfid  19481  0plef  19517  i1f1  19535  i1faddlem  19538  i1fmulclem  19547  i1fres  19550  i1fsub  19553  itg1sub  19554  mbfi1fseqlem4  19563  itg2le  19584  itg2mulclem  19591  itg2mulc  19592  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq3  19602  itg2addlem  19603  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  limccnp  19731  dvcmulf  19784  dvcobr  19785  dvfre  19790  dvnfre  19791  dvcnvlem  19813  dvcnv  19814  dvef  19817  dvferm1  19822  dvferm2  19824  rolle  19827  dvgt0lem1  19839  dvivthlem1  19845  dvne0  19848  lhop1lem  19850  lhop2  19852  lhop  19853  dvcnvrelem1  19854  dvcnvre  19856  dvcvx  19857  dvfsumrlim  19868  tdeglem3  19935  elply2  20068  elplyr  20073  plyeq0lem  20082  plyaddlem  20087  plymullem  20088  dgrlem  20101  coeidlem  20109  taylthlem2  20243  taylth  20244  ulmcn  20268  iblulm  20276  efcvx  20318  dvrelog  20481  relogcn  20482  dvlog2  20497  leibpi  20735  efrlim  20761  jensenlem2  20779  jensen  20780  amgmlem  20781  amgm  20782  wilthlem2  20805  wilthlem3  20806  basellem7  20822  basellem9  20824  lgsfcl  21041  lgsdchr  21085  dchrvmasumlem1  21142  dchrisum0lem3  21166  umgra1  21314  umisuhgra  21315  2trllemH  21505  2trllemG  21511  constr1trl  21541  constr3trllem1  21590  constr3trllem3  21592  eupa0  21649  eupap1  21651  0oo  22243  minvecolem3  22331  minvecolem4  22335  hhsscms  22732  occllem  22758  chscllem2  23093  chscllem4  23095  pjhf  23163  nlelchi  23517  hmopidmchi  23607  pjinvari  23647  lmlim  24286  rge0scvg  24288  lmdvg  24291  lmdvglim  24292  rrhre  24340  esumsn  24409  esumfsupre  24414  hashf2  24427  coinfliprv  24693  ptpcon  24873  fprb  25343  axlowdimlem4  25788  axlowdimlem7  25791  axlowdimlem10  25794  mblfinlem  26143  mbfresfi  26152  itg2addnclem  26155  itg2addnclem2  26156  itg2addnc  26158  itg2gt0cn  26159  fdc  26339  heiborlem6  26415  heibor  26420  ralxpmap  26632  ismrc  26645  mapfzcons  26662  mzpexpmpt  26692  mzpresrename  26697  diophrw  26707  rabren3dioph  26766  pwssplit1  27056  pwssplit4  27059  dsmmsubg  27077  dsmmlss  27078  islinds2  27151  lindsmm  27166  lsslindf  27168  lnrfg  27191  symgtrinv  27281  seff  27406  sblpnf  27407  climreeq  27606  stoweidlem39  27655  stoweidlem44  27660  stoweidlem59  27675  stirlinglem8  27697  lfl0f  29552  dochpolN  31973
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294  df-f 5417
  Copyright terms: Public domain W3C validator