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

Theorem fss 5721
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 3496 . . . . 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 563 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 5574 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5574 . . 3  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
63, 4, 53imtr4g 270 . 2  |-  ( B 
C_  C  ->  ( F : A --> B  ->  F : A --> C ) )
76impcom 428 1  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    C_ wss 3461   ran crn 4989    Fn wfn 5565   -->wf 5566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475  df-f 5574
This theorem is referenced by:  fssd  5722  f1ss  5768  fsn2  6047  ofco  6533  ffoss  6734  issmo2  7012  smoiso  7025  mapsn  7453  ssdomg  7554  alephfplem4  8479  cofsmo  8640  fin23lem17  8709  hsmexlem1  8797  axdc3lem4  8824  ac6s  8855  gruen  9179  intgru  9181  ingru  9182  1fv  11796  hashf1lem1  12488  sswrd  12541  sswrdOLD  12542  repsdf2  12741  limsupgre  13386  abscn2  13503  recn2  13505  imcn2  13506  climabs  13508  climre  13510  climim  13511  rlimabs  13513  rlimre  13515  rlimim  13516  caucvgrlem  13577  caurcvgr  13578  caucvgrlem2  13579  caurcvg  13581  fsumre  13704  fsumim  13705  0ram  14622  ramub1  14630  ramcl  14631  acsinfd  16009  acsdomd  16010  gsumval1  16103  resmhm2  16190  prdsgrpd  16378  prdsinvgd  16379  symgtrinv  16696  prdscmnd  17066  prdsabld  17067  gsumval3OLD  17107  gsumsubmclOLD  17130  gsumzaddOLD  17136  gsumzoppgOLD  17166  pgpfaclem1  17327  prdsringd  17456  prdscrngd  17457  abvf  17667  prdslmodd  17810  psrridm  18253  psrridmOLD  18254  coe1fval3  18442  zntoslem  18768  frgpcyg  18785  regsumsupp  18831  dsmmsubg  18947  dsmmlss  18948  islinds2  19015  lindsmm  19030  lsslindf  19032  1stccnp  20129  1stckgen  20221  prdstps  20296  pthaus  20305  txcmplem2  20309  ptcmpfi  20480  ptcmplem1  20718  ptcmpg  20723  prdstmdd  20788  prdstgpd  20789  ismet2  21002  prdsxmetlem  21037  imasdsf1olem  21042  prdsms  21200  isngp2  21283  metdscn  21526  lmmbr  21863  causs  21903  ovolfioo  22045  ovolficc  22046  ovolfsf  22049  elovolm  22052  ovollb  22056  ovolunlem1a  22073  ovolunlem1  22074  ovolicc2lem1  22094  ovolicc2lem2  22095  ovolicc2lem3  22096  ovolicc2lem4  22097  ovolicc2  22099  uniiccdif  22153  uniioovol  22154  uniiccvol  22155  uniioombllem2  22158  uniioombllem3a  22159  uniioombllem3  22160  uniioombllem4  22161  uniioombllem5  22162  uniioombl  22164  dyadmbl  22175  vitalilem3  22185  vitalilem4  22186  vitalilem5  22187  ismbf  22203  mbfid  22209  0plef  22245  i1f1  22263  i1faddlem  22266  i1fsub  22281  itg1sub  22282  mbfi1fseqlem4  22291  itg2le  22312  itg2mulclem  22319  itg2mulc  22320  itg2monolem1  22323  itg2monolem2  22324  itg2monolem3  22325  itg2mono  22326  itg2i1fseqle  22327  itg2i1fseq3  22330  itg2addlem  22331  itg2gt0  22333  itg2cnlem1  22334  itg2cnlem2  22335  dvfre  22520  dvnfre  22521  dvferm1  22552  dvferm2  22554  rolle  22557  dvgt0lem1  22569  dvivthlem1  22575  dvne0  22578  lhop1lem  22580  lhop2  22582  lhop  22583  dvcnvrelem1  22584  dvcnvre  22586  dvcvx  22587  dvfsumrlim  22598  tdeglem3  22623  elplyr  22764  taylthlem2  22935  taylth  22936  ulmcn  22960  iblulm  22968  efcvx  23010  dvrelog  23186  relogcn  23187  dvlog2  23202  leibpi  23470  efrlim  23497  jensenlem2  23515  jensen  23516  amgmlem  23517  amgm  23518  wilthlem2  23541  wilthlem3  23542  basellem7  23558  basellem9  23560  lgsfcl  23777  lgsdchr  23821  dchrvmasumlem1  23878  dchrisum0lem3  23902  axlowdimlem4  24450  axlowdimlem7  24453  axlowdimlem10  24456  umisuhgra  24529  2trllemG  24762  constr3trllem1  24852  0oo  25902  hhsscms  26393  nlelchi  27178  hmopidmchi  27268  pjinvari  27308  padct  27776  lmlim  28164  rge0scvg  28166  lmdvg  28170  lmdvglim  28171  rrhre  28233  esumfsupre  28300  hashf2  28313  eulerpartlems  28563  eulerpartlemgs2  28583  coinfliprv  28685  ptpcon  28942  fprb  29443  mblfinlem2  30292  mbfresfi  30301  itg2addnclem  30306  itg2addnclem2  30307  itg2addnc  30309  itg2gt0cn  30310  ftc1anclem8  30337  fdc  30478  heiborlem6  30552  heibor  30557  mzpexpmpt  30917  mzpresrename  30922  diophrw  30931  rabren3dioph  30988  lnrfg  31309  seff  31430  sblpnf  31431  binomcxplemnotnn0  31502  stoweidlem44  32065  stirlinglem8  32102  fourierdlem62  32190  fouriersw  32253  resmgmhm2  32859  zlmodzxzldeplem1  33355  aacllem  33604  lfl0f  35191
  Copyright terms: Public domain W3C validator