Theorem fss 6056

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

Step	Hyp	Ref	Expression
1		sstr2 3610	. . . . 5 |- ( ran F C_ B -> ( B C_ C -> ran F C_ C ) )
2	1	com12 32	. . . 4 |- ( B C_ C -> ( ran F C_ B -> ran F C_ C ) )
3	2	anim2d 589	. . 3 |- ( B C_ C -> ( ( F Fn A /\ ran F C_ B ) -> ( F Fn A /\ ran F C_ C ) ) )
4		df-f 5892	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5		df-f 5892	. . 3 |- ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
6	3, 4, 5	3imtr4g 285	. 2 |- ( B C_ C -> ( F : A --> B -> F : A --> C ) )
7	6	impcom 446	1 |- ( ( F : A --> B /\ B C_ C ) -> F : A --> C )

Syntax hints:   -> wi 4   /\ wa 384   C_ wss 3574   ran crn 5115   Fn wfn 5883   -->wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-f 5892

This theorem is referenced by:  fssd  6057  f1ss  6106  frnssb  6391  fsn2  6403  fsnex  6538  ofco  6917  ffoss  7127  issmo2  7446  smoiso  7459  mapsn  7899  ssdomg  8001  alephfplem4  8930  cofsmo  9091  fin23lem17  9160  hsmexlem1  9248  axdc3lem4  9275  ac6s  9306  gruen  9634  intgru  9636  ingru  9637  hashf1lem1  13239  sswrd  13313  wrdv  13320  repsdf2  13525  limsupgre  14212  abscn2  14329  recn2  14331  imcn2  14332  climabs  14334  climre  14336  climim  14337  rlimabs  14339  rlimre  14341  rlimim  14342  caucvgrlem  14403  caurcvgr  14404  caucvgrlem2  14405  caurcvg  14407  fsumre  14540  fsumim  14541  0ram  15724  ramub1  15732  ramcl  15733  acsinfd  17180  acsdomd  17181  gsumval1  17277  resmhm2  17360  prdsgrpd  17525  prdsinvgd  17526  symgtrinv  17892  prdscmnd  18264  prdsabld  18265  pgpfaclem1  18480  prdsringd  18612  prdscrngd  18613  abvf  18823  prdslmodd  18969  psrridm  19404  coe1fval3  19578  zntoslem  19905  regsumsupp  19968  dsmmsubg  20087  dsmmlss  20088  islinds2  20152  lindsmm  20167  lsslindf  20169  1stccnp  21265  1stckgen  21357  prdstps  21432  pthaus  21441  txcmplem2  21445  ptcmpfi  21616  ptcmplem1  21856  ptcmpg  21861  prdstmdd  21927  prdstgpd  21928  ismet2  22138  prdsxmetlem  22173  imasdsf1olem  22178  prdsms  22336  isngp2  22401  metdscn  22659  lmmbr  23056  causs  23096  ovolfioo  23236  ovolficc  23237  ovolfsf  23240  elovolm  23243  ovollb  23247  ovolunlem1a  23264  ovolunlem1  23265  ovolicc2lem1  23285  ovolicc2lem2  23286  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2  23290  uniiccdif  23346  uniioovol  23347  uniiccvol  23348  uniioombllem2  23351  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombl  23357  dyadmbl  23368  vitalilem3  23379  vitalilem4  23380  vitalilem5  23381  ismbf  23397  mbfid  23403  0plef  23439  i1f1  23457  i1faddlem  23460  i1fsub  23475  itg1sub  23476  mbfi1fseqlem4  23485  itg2le  23506  itg2mulclem  23513  itg2mulc  23514  itg2monolem1  23517  itg2monolem2  23518  itg2monolem3  23519  itg2mono  23520  itg2i1fseqle  23521  itg2i1fseq3  23524  itg2addlem  23525  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  dvfre  23714  dvnfre  23715  dvferm1  23748  dvferm2  23750  rolle  23753  dvgt0lem1  23765  dvivthlem1  23771  dvne0  23774  lhop1lem  23776  lhop2  23778  lhop  23779  dvcnvrelem1  23780  dvcnvre  23782  dvcvx  23783  dvfsumrlim  23794  tdeglem3  23819  elplyr  23957  taylthlem2  24128  taylth  24129  ulmcn  24153  iblulm  24161  efcvx  24203  dvrelog  24383  relogcn  24384  dvlog2  24399  leibpi  24669  efrlim  24696  jensenlem2  24714  jensen  24715  amgmlem  24716  amgm  24717  wilthlem2  24795  wilthlem3  24796  basellem7  24813  basellem9  24815  lgsfcl  25030  lgsdchr  25080  dchrvmasumlem1  25184  dchrisum0lem3  25208  axlowdimlem4  25825  axlowdimlem7  25828  axlowdimlem10  25831  upgruhgr  25997  konigsbergssiedgw  27111  pliguhgr  27338  0oo  27644  hhsscms  28136  nlelchi  28920  hmopidmchi  29010  pjinvari  29050  padct  29497  smatrcl  29862  lmlim  29993  rge0scvg  29995  lmdvg  29999  lmdvglim  30000  rrhre  30065  esumfsupre  30133  hashf2  30146  eulerpartlems  30422  eulerpartlemgs2  30442  coinfliprv  30544  fdvposlt  30677  fdvposle  30679  breprexpnat  30712  circlemethnat  30719  circlevma  30720  tgoldbachgtde  30738  ptpconn  31215  fprb  31669  poimirlem8  33417  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  mblfinlem2  33447  mbfresfi  33456  itg2addnclem  33461  itg2addnclem2  33462  itg2addnc  33464  itg2gt0cn  33465  ftc1anclem8  33492  fdc  33541  heiborlem6  33615  heibor  33620  lfl0f  34356  mzpexpmpt  37308  mzpresrename  37313  diophrw  37322  rabren3dioph  37379  lnrfg  37689  seff  38508  sblpnf  38509  binomcxplemnotnn0  38555  mapsnd  39388  stoweidlem44  40261  stirlinglem8  40298  fourierdlem62  40385  fouriersw  40448  nnsum3primes4  41676  resmgmhm2  41799  zlmodzxzldeplem1  42289  aacllem  42547  amgmwlem  42548