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

Theorem fss 5555
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 3351 . . . . 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 560 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 5410 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5410 . . 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 3316   ran crn 4828    Fn wfn 5401   -->wf 5402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330  df-f 5410
This theorem is referenced by:  fconst6g  5587  f1ss  5599  fsn2  5870  ofco  6329  ffoss  6527  tposf2  6758  issmo2  6796  smoiso  6809  mapsn  7242  mapss  7243  ralxpmap  7250  ssdomg  7343  ac6sfi  7544  infpwfien  8220  alephfplem4  8265  infmap2  8375  cofsmo  8426  fin23lem17  8495  fin23lem32  8501  hsmexlem1  8583  axdc3lem4  8610  ac6s  8641  pwfseqlem4a  8816  gruen  8967  intgru  8969  ingru  8970  1fv  11516  fseq1p1m1  11518  seqf1olem2  11830  hashf1lem1  12192  sswrd  12226  snopiswrd  12227  repsdf2  12400  wrdlen2i  12530  limsupgre  12943  abscn2  13060  recn2  13062  imcn2  13063  climabs  13065  climre  13067  climim  13068  rlimabs  13070  rlimre  13072  rlimim  13073  caucvgrlem  13134  caurcvgr  13135  caucvgrlem2  13136  caurcvg  13138  fsumre  13254  fsumim  13255  supcvg  13301  vdwlem8  14032  0ram  14064  ramub1  14072  ramcl  14073  isacs2  14574  funcres2b  14790  acsinfd  15333  acsdomd  15334  resmhm2  15470  gsumress  15487  gsumval1  15489  gsumwsubmcl  15496  gsumws1  15497  prdsgrpd  15644  prdsinvgd  15645  symgtrinv  15958  pj1ghm  16180  prdscmnd  16323  prdsabld  16324  gsumval3eu  16361  gsumval3OLD  16362  gsumval3  16365  gsumsubmcl  16384  gsumsubmclOLD  16385  gsumzadd  16389  gsumzaddOLD  16391  gsumzoppg  16416  gsumzoppgOLD  16417  dprdsn  16507  pgpfaclem1  16556  prdsrngd  16639  prdscrngd  16640  abvf  16832  prdslmodd  16972  pwssplit1  17062  psrridm  17410  psrridmOLD  17411  coe1fval3  17563  zntoslem  17831  frgpcyg  17848  regsumsupp  17894  pjdm2  17978  dsmmsubg  18010  dsmmlss  18011  islinds2  18084  lindsmm  18099  lsslindf  18101  cnrest2  18732  cnprest2  18736  1stcelcls  18907  1stccnp  18908  1stckgen  18969  prdstps  19044  pthaus  19053  txcmplem2  19057  xkoptsub  19069  pt1hmeo  19221  ptcmpfi  19228  ptcmplem1  19466  ptcmpg  19471  prdstmdd  19536  prdstgpd  19537  tsmssubm  19558  ismet2  19750  prdsxmetlem  19785  imasdsf1olem  19790  prdsms  19948  isngp2  20031  metdscn  20274  cncfss  20317  ipcn  20600  lmmbr  20611  causs  20651  equivcau  20653  lmcau  20665  ovolfioo  20793  ovolficc  20794  ovolfsf  20797  elovolm  20800  ovollb  20804  ovolunlem1a  20821  ovolunlem1  20822  ovolicc2lem1  20842  ovolicc2lem2  20843  ovolicc2lem3  20844  ovolicc2lem4  20845  ovolicc2  20847  uniiccdif  20900  uniioovol  20901  uniiccvol  20902  uniioombllem2  20905  uniioombllem3a  20906  uniioombllem3  20907  uniioombllem4  20908  uniioombllem5  20909  uniioombl  20911  dyadmbl  20922  vitalilem3  20932  vitalilem4  20933  vitalilem5  20934  ismbf  20950  mbfid  20956  0plef  20992  i1f1  21010  i1faddlem  21013  i1fmulclem  21022  i1fres  21025  i1fsub  21028  itg1sub  21029  mbfi1fseqlem4  21038  itg2le  21059  itg2mulclem  21066  itg2mulc  21067  itg2monolem1  21070  itg2monolem2  21071  itg2monolem3  21072  itg2mono  21073  itg2i1fseqle  21074  itg2i1fseq3  21077  itg2addlem  21078  itg2gt0  21080  itg2cnlem1  21081  itg2cnlem2  21082  limccnp  21208  dvcmulf  21261  dvcobr  21262  dvfre  21267  dvnfre  21268  dvcnvlem  21290  dvcnv  21291  dvef  21294  dvferm1  21299  dvferm2  21301  rolle  21304  dvgt0lem1  21316  dvivthlem1  21322  dvne0  21325  lhop1lem  21327  lhop2  21329  lhop  21330  dvcnvrelem1  21331  dvcnvre  21333  dvcvx  21334  dvfsumrlim  21345  tdeglem3  21413  elply2  21549  elplyr  21554  plyeq0lem  21563  plyaddlem  21568  plymullem  21569  dgrlem  21582  coeidlem  21590  taylthlem2  21724  taylth  21725  ulmcn  21749  iblulm  21757  efcvx  21799  dvrelog  21967  relogcn  21968  dvlog2  21983  leibpi  22222  efrlim  22248  jensenlem2  22266  jensen  22267  amgmlem  22268  amgm  22269  wilthlem2  22292  wilthlem3  22293  basellem7  22309  basellem9  22311  lgsfcl  22528  lgsdchr  22572  dchrvmasumlem1  22629  dchrisum0lem3  22653  axlowdimlem4  23014  axlowdimlem7  23017  axlowdimlem10  23020  umgra1  23083  umisuhgra  23084  2trllemH  23274  2trllemG  23280  constr1trl  23310  constr3trllem1  23359  constr3trllem3  23361  eupa0  23418  eupap1  23420  0oo  24012  minvecolem3  24100  minvecolem4  24104  hhsscms  24503  occllem  24529  chscllem2  24864  chscllem4  24866  pjhf  24934  nlelchi  25288  hmopidmchi  25378  pjinvari  25418  resf1o  25855  lmlim  26231  rge0scvg  26233  lmdvg  26237  lmdvglim  26238  rrhre  26301  esumsn  26369  esumfsupre  26374  hashf2  26387  eulerpartlems  26591  eulerpartlemgs2  26611  coinfliprv  26713  ptpcon  26970  fprb  27431  mblfinlem2  28273  mbfresfi  28282  itg2addnclem  28287  itg2addnclem2  28288  itg2addnc  28290  itg2gt0cn  28291  ftc1anclem8  28318  fdc  28485  heiborlem6  28559  heibor  28564  ismrc  28882  mapfzcons  28897  mzpexpmpt  28926  mzpresrename  28932  diophrw  28942  rabren3dioph  28999  pwssplit4  29287  lnrfg  29320  seff  29440  sblpnf  29441  climreeq  29632  stoweidlem39  29680  stoweidlem44  29685  stoweidlem59  29700  stirlinglem8  29722  mapsnop  30579  mapprop  30580  zlmodzxzel  30586  snlindsntorlem  30713  zlmodzxzldeplem1  30751  lfl0f  32287  dochpolN  34708
  Copyright terms: Public domain W3C validator