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

Theorem fss 5738
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 3511 . . . . 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 565 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 5591 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5591 . . 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 430 1  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    C_ wss 3476   ran crn 5000    Fn wfn 5582   -->wf 5583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-f 5591
This theorem is referenced by:  fssd  5739  fconst6g  5773  f1ss  5785  fsn2  6060  ofco  6543  ffoss  6745  tposf2  6979  issmo2  7020  smoiso  7033  mapsn  7460  mapss  7461  ralxpmap  7468  ssdomg  7561  ac6sfi  7763  infpwfien  8442  alephfplem4  8487  infmap2  8597  cofsmo  8648  fin23lem17  8717  fin23lem32  8723  hsmexlem1  8805  axdc3lem4  8832  ac6s  8863  pwfseqlem4a  9038  gruen  9189  intgru  9191  ingru  9192  fseq1p1m1  11751  1fv  11788  seqf1olem2  12114  hashf1lem1  12469  sswrd  12520  snopiswrd  12521  repsdf2  12712  wrdlen2i  12846  limsupgre  13266  abscn2  13383  recn2  13385  imcn2  13386  climabs  13388  climre  13390  climim  13391  rlimabs  13393  rlimre  13395  rlimim  13396  caucvgrlem  13457  caurcvgr  13458  caucvgrlem2  13459  caurcvg  13461  fsumre  13584  fsumim  13585  supcvg  13629  vdwlem8  14364  0ram  14396  ramub1  14404  ramcl  14405  isacs2  14907  funcres2b  15123  acsinfd  15666  acsdomd  15667  resmhm2  15807  gsumress  15826  gsumval1  15828  gsumwsubmcl  15835  gsumws1  15836  prdsgrpd  15986  prdsinvgd  15987  symgtrinv  16300  pj1ghm  16524  prdscmnd  16667  prdsabld  16668  gsumval3eu  16707  gsumval3OLD  16708  gsumval3  16711  gsumsubmcl  16730  gsumsubmclOLD  16731  gsumzadd  16735  gsumzaddOLD  16737  gsumzoppg  16767  gsumzoppgOLD  16768  dprdsn  16882  pgpfaclem1  16931  prdsrngd  17057  prdscrngd  17058  abvf  17267  prdslmodd  17410  pwssplit1  17500  psrridm  17845  psrridmOLD  17846  coe1fval3  18034  zntoslem  18378  frgpcyg  18395  regsumsupp  18441  pjdm2  18525  dsmmsubg  18557  dsmmlss  18558  islinds2  18631  lindsmm  18646  lsslindf  18648  mat1dimelbas  18756  mat1dimmul  18761  cnrest2  19569  cnprest2  19573  1stcelcls  19744  1stccnp  19745  1stckgen  19806  prdstps  19881  pthaus  19890  txcmplem2  19894  xkoptsub  19906  pt1hmeo  20058  ptcmpfi  20065  ptcmplem1  20303  ptcmpg  20308  prdstmdd  20373  prdstgpd  20374  tsmssubm  20395  ismet2  20587  prdsxmetlem  20622  imasdsf1olem  20627  prdsms  20785  isngp2  20868  metdscn  21111  cncfss  21154  ipcn  21437  lmmbr  21448  causs  21488  equivcau  21490  lmcau  21502  ovolfioo  21630  ovolficc  21631  ovolfsf  21634  elovolm  21637  ovollb  21641  ovolunlem1a  21658  ovolunlem1  21659  ovolicc2lem1  21679  ovolicc2lem2  21680  ovolicc2lem3  21681  ovolicc2lem4  21682  ovolicc2  21684  uniiccdif  21738  uniioovol  21739  uniiccvol  21740  uniioombllem2  21743  uniioombllem3a  21744  uniioombllem3  21745  uniioombllem4  21746  uniioombllem5  21747  uniioombl  21749  dyadmbl  21760  vitalilem3  21770  vitalilem4  21771  vitalilem5  21772  ismbf  21788  mbfid  21794  0plef  21830  i1f1  21848  i1faddlem  21851  i1fmulclem  21860  i1fres  21863  i1fsub  21866  itg1sub  21867  mbfi1fseqlem4  21876  itg2le  21897  itg2mulclem  21904  itg2mulc  21905  itg2monolem1  21908  itg2monolem2  21909  itg2monolem3  21910  itg2mono  21911  itg2i1fseqle  21912  itg2i1fseq3  21915  itg2addlem  21916  itg2gt0  21918  itg2cnlem1  21919  itg2cnlem2  21920  limccnp  22046  dvcmulf  22099  dvcobr  22100  dvfre  22105  dvnfre  22106  dvcnvlem  22128  dvcnv  22129  dvef  22132  dvferm1  22137  dvferm2  22139  rolle  22142  dvgt0lem1  22154  dvivthlem1  22160  dvne0  22163  lhop1lem  22165  lhop2  22167  lhop  22168  dvcnvrelem1  22169  dvcnvre  22171  dvcvx  22172  dvfsumrlim  22183  tdeglem3  22208  elply2  22344  elplyr  22349  plyeq0lem  22358  plyaddlem  22363  plymullem  22364  dgrlem  22377  coeidlem  22385  taylthlem2  22519  taylth  22520  ulmcn  22544  iblulm  22552  efcvx  22594  dvrelog  22762  relogcn  22763  dvlog2  22778  leibpi  23017  efrlim  23043  jensenlem2  23061  jensen  23062  amgmlem  23063  amgm  23064  wilthlem2  23087  wilthlem3  23088  basellem7  23104  basellem9  23106  lgsfcl  23323  lgsdchr  23367  dchrvmasumlem1  23424  dchrisum0lem3  23448  axlowdimlem4  23940  axlowdimlem7  23943  axlowdimlem10  23946  umgra1  24018  umisuhgra  24019  2trllemH  24246  2trllemG  24252  constr1trl  24282  constr3trllem1  24342  constr3trllem3  24344  eupa0  24666  eupap1  24668  0oo  25396  minvecolem3  25484  minvecolem4  25488  hhsscms  25887  occllem  25913  chscllem2  26248  chscllem4  26250  pjhf  26318  nlelchi  26672  hmopidmchi  26762  pjinvari  26802  resf1o  27241  lmlim  27581  rge0scvg  27583  lmdvg  27587  lmdvglim  27588  rrhre  27651  esumsn  27728  esumfsupre  27733  hashf2  27746  eulerpartlems  27955  eulerpartlemgs2  27975  coinfliprv  28077  ptpcon  28334  fprb  28796  mblfinlem2  29645  mbfresfi  29654  itg2addnclem  29659  itg2addnclem2  29660  itg2addnc  29662  itg2gt0cn  29663  ftc1anclem8  29690  fdc  29857  heiborlem6  29931  heibor  29936  ismrc  30253  mapfzcons  30268  mzpexpmpt  30297  mzpresrename  30303  diophrw  30312  rabren3dioph  30369  pwssplit4  30655  lnrfg  30688  seff  30808  sblpnf  30809  climreeq  31171  limccog  31178  limcrecl  31187  stoweidlem39  31355  stoweidlem44  31360  stoweidlem59  31375  stirlinglem8  31397  dirkercncflem3  31421  dirkercncf  31423  fourierdlem54  31477  fourierdlem62  31485  fourierdlem74  31497  fourierdlem75  31498  fourierdlem79  31502  fourierdlem88  31511  fourierdlem93  31516  fourierdlem103  31526  fourierdlem104  31527  fourierdlem111  31534  fouriersw  31548  mapsnop  32018  mapprop  32019  zlmodzxzel  32028  snlindsntorlem  32161  zlmodzxzldeplem1  32191  lfl0f  33875  dochpolN  36296
  Copyright terms: Public domain W3C validator