Theorem fss 6513

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	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Proof of Theorem fss

Step	Hyp	Ref	Expression
1		sstr2 3900	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 615	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6340	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6340	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 300	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 412	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3859  ran crn 5526   Fn wfn 6331  ⟶wf 6332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3866  df-ss 3876  df-f 6340

This theorem is referenced by:  fssd  6514  f1ss  6567  frnssb  6877  fsn2  6890  fprb  6948  ofco  7428  ffoss  7652  issmo2  7997  smoiso  8010  ssdomg  8574  alephfplem4  9568  cofsmo  9730  fin23lem17  9799  hsmexlem1  9887  axdc3lem4  9914  ac6s  9945  gruen  10273  intgru  10275  ingru  10276  hashf1lem1  13865  hashf1lem1OLD  13866  sswrd  13922  repsdf2  14188  limsupgre  14887  abscn2  15004  recn2  15006  imcn2  15007  climabs  15009  climre  15011  climim  15012  rlimabs  15014  rlimre  15016  rlimim  15017  caucvgrlem  15078  caurcvgr  15079  caucvgrlem2  15080  caurcvg  15082  fsumre  15212  fsumim  15213  0ram  16412  ramub1  16420  ramcl  16421  acsinfd  17857  acsdomd  17858  gsumval1  17960  resmhm2  18053  prdsgrpd  18277  prdsinvgd  18278  symgtrinv  18668  prdscmnd  19050  prdsabld  19051  pgpfaclem1  19272  prdsringd  19434  prdscrngd  19435  abvf  19663  prdslmodd  19810  zntoslem  20325  regsumsupp  20388  dsmmsubg  20509  dsmmlss  20510  islinds2  20579  lindsmm  20594  lsslindf  20596  psrridm  20733  coe1fval3  20933  1stccnp  22163  1stckgen  22255  prdstps  22330  pthaus  22339  txcmplem2  22343  ptcmpfi  22514  ptcmplem1  22753  ptcmpg  22758  prdstmdd  22825  prdstgpd  22826  ismet2  23036  prdsxmetlem  23071  imasdsf1olem  23076  prdsms  23234  isngp2  23300  metdscn  23558  lmmbr  23959  causs  23999  ovolfioo  24168  ovolficc  24169  ovolfsf  24172  elovolm  24176  ovollb  24180  ovolunlem1a  24197  ovolunlem1  24198  ovolicc2lem1  24218  ovolicc2lem2  24219  ovolicc2lem3  24220  ovolicc2lem4  24221  ovolicc2  24223  uniiccdif  24279  uniioovol  24280  uniiccvol  24281  uniioombllem2  24284  uniioombllem3a  24285  uniioombllem3  24286  uniioombllem4  24287  uniioombllem5  24288  uniioombl  24290  dyadmbl  24301  vitalilem3  24311  vitalilem4  24312  vitalilem5  24313  ismbf  24329  mbfid  24336  0plef  24373  i1f1  24391  i1faddlem  24394  i1fsub  24409  itg1sub  24410  mbfi1fseqlem4  24419  itg2le  24440  itg2mulclem  24447  itg2mulc  24448  itg2monolem1  24451  itg2monolem2  24452  itg2monolem3  24453  itg2mono  24454  itg2i1fseq3  24458  itg2addlem  24459  itg2gt0  24461  itg2cnlem1  24462  itg2cnlem2  24463  dvfre  24651  dvnfre  24652  dvferm1  24685  dvferm2  24687  rolle  24690  dvgt0lem1  24702  dvivthlem1  24708  dvne0  24711  lhop1lem  24713  lhop2  24715  lhop  24716  dvcnvrelem1  24717  dvcnvre  24719  dvcvx  24720  dvfsumrlim  24731  tdeglem3  24758  tdeglem3OLD  24759  elplyr  24898  taylthlem2  25069  taylth  25070  ulmcn  25094  iblulm  25102  efcvx  25144  dvrelog  25328  relogcn  25329  dvlog2  25344  leibpi  25628  efrlim  25655  jensenlem2  25673  jensen  25674  amgmlem  25675  amgm  25676  wilthlem2  25754  wilthlem3  25755  basellem7  25772  basellem9  25774  lgsfcl  25989  lgsdchr  26039  dchrvmasumlem1  26179  dchrisum0lem3  26203  axlowdimlem4  26839  axlowdimlem7  26842  axlowdimlem10  26845  upgruhgr  26995  konigsbergssiedgw  28135  pliguhgr  28369  0oo  28672  hhsscms  29161  nlelchi  29944  hmopidmchi  30034  pjinvari  30074  padct  30579  smatrcl  31268  lmlim  31419  rge0scvg  31421  lmdvg  31425  lmdvglim  31426  rrhre  31491  esumfsupre  31559  hashf2  31572  eulerpartlems  31847  eulerpartlemgs2  31867  coinfliprv  31969  fdvposlt  32099  fdvposle  32101  breprexpnat  32134  circlemethnat  32141  circlevma  32142  tgoldbachgtde  32160  lfuhgr  32596  subgrwlk  32611  ptpconn  32712  poimirlem8  35346  poimirlem18  35356  poimirlem21  35359  poimirlem22  35360  mblfinlem2  35376  mbfresfi  35384  itg2addnclem  35389  itg2addnclem2  35390  itg2addnc  35392  itg2gt0cn  35393  ftc1anclem8  35418  fdc  35464  heiborlem6  35535  heibor  35540  lfl0f  36646  intlewftc  39629  mzpexpmpt  40060  mzpresrename  40065  diophrw  40074  rabren3dioph  40130  lnrfg  40437  seff  41387  sblpnf  41388  binomcxplemnotnn0  41434  stoweidlem44  43053  stirlinglem8  43090  fourierdlem62  43177  fouriersw  43240  nnsum3primes4  44674  resmgmhm2  44787  zlmodzxzldeplem1  45275  aacllem  45721  amgmwlem  45722