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

Theorem fss 5749
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 3425 . . . . 5  |-  ( ran 
F  C_  B  ->  ( B  C_  C  ->  ran 
F  C_  C )
)
21com12 31 . . . 4  |-  ( B 
C_  C  ->  ( ran  F  C_  B  ->  ran 
F  C_  C )
)
32anim2d 575 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 5593 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5593 . . 3  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
63, 4, 53imtr4g 278 . 2  |-  ( B 
C_  C  ->  ( F : A --> B  ->  F : A --> C ) )
76impcom 437 1  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    C_ wss 3390   ran crn 4840    Fn wfn 5584   -->wf 5585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404  df-f 5593
This theorem is referenced by:  fssd  5750  f1ss  5797  frnssb  6067  fsn2  6078  fsnex  6199  ofco  6570  ffoss  6773  issmo2  7086  smoiso  7099  mapsn  7531  ssdomg  7633  alephfplem4  8556  cofsmo  8717  fin23lem17  8786  hsmexlem1  8874  axdc3lem4  8901  ac6s  8932  gruen  9255  intgru  9257  ingru  9258  1fv  11935  hashf1lem1  12659  sswrd  12726  sswrdOLD  12727  wrdv  12733  repsdf2  12935  limsupgre  13619  limsupgreOLD  13620  abscn2  13739  recn2  13741  imcn2  13742  climabs  13744  climre  13746  climim  13747  rlimabs  13749  rlimre  13751  rlimim  13752  caucvgrlem  13813  caucvgrlemOLD  13814  caurcvgr  13815  caurcvgrOLD  13816  caucvgrlem2  13817  caurcvg  13819  caurcvgOLD  13820  fsumre  13945  fsumim  13946  0ram  15057  ramub1  15065  ramcl  15066  acsinfd  16504  acsdomd  16505  gsumval1  16598  resmhm2  16685  prdsgrpd  16873  prdsinvgd  16874  symgtrinv  17191  prdscmnd  17577  prdsabld  17578  pgpfaclem1  17792  prdsringd  17918  prdscrngd  17919  abvf  18129  prdslmodd  18270  psrridm  18705  coe1fval3  18878  zntoslem  19204  frgpcyg  19221  regsumsupp  19267  dsmmsubg  19383  dsmmlss  19384  islinds2  19448  lindsmm  19463  lsslindf  19465  1stccnp  20554  1stckgen  20646  prdstps  20721  pthaus  20730  txcmplem2  20734  ptcmpfi  20905  ptcmplem1  21145  ptcmpg  21150  prdstmdd  21216  prdstgpd  21217  ismet2  21426  prdsxmetlem  21461  imasdsf1olem  21466  prdsms  21624  isngp2  21689  metdscn  21951  metdscnOLD  21966  lmmbr  22306  causs  22346  ovolfioo  22498  ovolficc  22499  ovolfsf  22502  elovolm  22506  ovollb  22510  ovolunlem1a  22527  ovolunlem1  22528  ovolicc2lem1  22548  ovolicc2lem2  22549  ovolicc2lem3  22550  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ovolicc2  22554  uniiccdif  22614  uniioovol  22615  uniiccvol  22616  uniioombllem2  22619  uniioombllem2OLD  22620  uniioombllem3a  22621  uniioombllem3  22622  uniioombllem4  22623  uniioombllem5  22624  uniioombl  22626  dyadmbl  22637  vitalilem3  22647  vitalilem4  22648  vitalilem5  22649  ismbf  22665  mbfid  22671  0plef  22709  i1f1  22727  i1faddlem  22730  i1fsub  22745  itg1sub  22746  mbfi1fseqlem4  22755  itg2le  22776  itg2mulclem  22783  itg2mulc  22784  itg2monolem1  22787  itg2monolem2  22788  itg2monolem3  22789  itg2mono  22790  itg2i1fseqle  22791  itg2i1fseq3  22794  itg2addlem  22795  itg2gt0  22797  itg2cnlem1  22798  itg2cnlem2  22799  dvfre  22984  dvnfre  22985  dvferm1  23016  dvferm2  23018  rolle  23021  dvgt0lem1  23033  dvivthlem1  23039  dvne0  23042  lhop1lem  23044  lhop2  23046  lhop  23047  dvcnvrelem1  23048  dvcnvre  23050  dvcvx  23051  dvfsumrlim  23062  tdeglem3  23087  elplyr  23234  taylthlem2  23408  taylth  23409  ulmcn  23433  iblulm  23441  efcvx  23483  dvrelog  23661  relogcn  23662  dvlog2  23677  leibpi  23947  efrlim  23974  jensenlem2  23992  jensen  23993  amgmlem  23994  amgm  23995  wilthlem2  24073  wilthlem3  24074  basellem7  24092  basellem9  24094  lgsfcl  24311  lgsdchr  24355  dchrvmasumlem1  24412  dchrisum0lem3  24436  axlowdimlem4  25054  axlowdimlem7  25057  axlowdimlem10  25060  umisuhgra  25133  2trllemG  25367  constr3trllem1  25457  0oo  26511  hhsscms  27011  nlelchi  27795  hmopidmchi  27885  pjinvari  27925  padct  28382  smatrcl  28696  lmlim  28827  rge0scvg  28829  lmdvg  28833  lmdvglim  28834  rrhre  28899  esumfsupre  28966  hashf2  28979  eulerpartlems  29266  eulerpartlemgs2  29286  coinfliprv  29388  ptpcon  30028  fprb  30484  poimirlem8  32012  poimirlem18  32022  poimirlem21  32025  poimirlem22  32026  mblfinlem2  32042  mbfresfi  32051  itg2addnclem  32057  itg2addnclem2  32058  itg2addnc  32060  itg2gt0cn  32061  ftc1anclem8  32088  fdc  32138  heiborlem6  32212  heibor  32217  lfl0f  32706  mzpexpmpt  35658  mzpresrename  35663  diophrw  35672  rabren3dioph  35729  lnrfg  36049  seff  36727  sblpnf  36728  binomcxplemnotnn0  36775  mapsnd  37547  stoweidlem44  38017  stirlinglem8  38055  fourierdlem62  38144  fouriersw  38207  nnsum3primes4  39028  upgruhgr  39347  konigsbergssiedgw  40163  resmgmhm2  40307  zlmodzxzldeplem1  40801  aacllem  41046
  Copyright terms: Public domain W3C validator