Theorem fss 6744

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 3986	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 610	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6558	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6558	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 295	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 406	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 394   ⊆ wss 3947  ran crn 5683   Fn wfn 6549  ⟶wf 6550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804

This theorem depends on definitions:  df-bi 206  df-an 395  df-ss 3964  df-f 6558

This theorem is referenced by:  fssd  6745  f1ss  6803  fcdmssb  7136  fsn2  7150  fprb  7211  ofco  7714  ffoss  7959  issmo2  8379  smoiso  8392  ssdomg  9031  alephfplem4  10150  cofsmo  10312  fin23lem17  10381  hsmexlem1  10469  axdc3lem4  10496  ac6s  10527  gruen  10855  intgru  10857  ingru  10858  hashf1lem1  14473  hashf1lem1OLD  14474  sswrd  14530  repsdf2  14786  limsupgre  15483  abscn2  15601  recn2  15603  imcn2  15604  climabs  15606  climre  15608  climim  15609  rlimabs  15611  rlimre  15613  rlimim  15614  caucvgrlem  15677  caurcvgr  15678  caucvgrlem2  15679  caurcvg  15681  fsumre  15812  fsumim  15813  0ram  17022  ramub1  17030  ramcl  17031  acsinfd  18581  acsdomd  18582  gsumval1  18676  resmgmhm2  18705  resmhm2  18811  prdsgrpd  19044  prdsinvgd  19045  symgtrinv  19470  prdscmnd  19859  prdsabld  19860  pgpfaclem1  20081  prdsrngd  20159  prdsmulrcl  20299  prdsringd  20300  prdscrngd  20301  abvf  20794  prdslmodd  20946  zntoslem  21554  regsumsupp  21618  dsmmsubg  21741  dsmmlss  21742  islinds2  21811  lindsmm  21826  lsslindf  21828  psrridm  21972  coe1fval3  22198  1stccnp  23457  1stckgen  23549  prdstps  23624  pthaus  23633  txcmplem2  23637  ptcmpfi  23808  ptcmplem1  24047  ptcmpg  24052  prdstmdd  24119  prdstgpd  24120  ismet2  24330  prdsxmetlem  24365  imasdsf1olem  24370  prdsms  24531  isngp2  24597  metdscn  24863  lmmbr  25277  causs  25317  ovolfioo  25487  ovolficc  25488  ovolfsf  25491  elovolm  25495  ovollb  25499  ovolunlem1a  25516  ovolunlem1  25517  ovolicc2lem1  25537  ovolicc2lem2  25538  ovolicc2lem3  25539  ovolicc2lem4  25540  ovolicc2  25542  uniiccdif  25598  uniioovol  25599  uniiccvol  25600  uniioombllem2  25603  uniioombllem3a  25604  uniioombllem3  25605  uniioombllem4  25606  uniioombllem5  25607  uniioombl  25609  dyadmbl  25620  vitalilem3  25630  vitalilem4  25631  vitalilem5  25632  ismbf  25648  mbfid  25655  0plef  25692  i1f1  25710  i1faddlem  25713  i1fsub  25729  itg1sub  25730  mbfi1fseqlem4  25739  itg2le  25760  itg2mulclem  25767  itg2mulc  25768  itg2monolem1  25771  itg2monolem2  25772  itg2monolem3  25773  itg2mono  25774  itg2i1fseq3  25778  itg2addlem  25779  itg2gt0  25781  itg2cnlem1  25782  itg2cnlem2  25783  dvfre  25974  dvnfre  25975  dvferm1  26008  dvferm2  26010  rolle  26013  dvgt0lem1  26026  dvivthlem1  26032  dvne0  26035  lhop1lem  26037  lhop2  26039  lhop  26040  dvcnvrelem1  26041  dvcnvre  26043  dvcvx  26044  dvfsumrlim  26057  tdeglem3  26084  tdeglem3OLD  26085  elplyr  26228  taylthlem2  26402  taylthlem2OLD  26403  taylth  26404  ulmcn  26428  iblulm  26436  efcvx  26479  dvrelog  26664  relogcn  26665  dvlog2  26680  leibpi  26970  efrlim  26997  efrlimOLD  26998  jensenlem2  27016  jensen  27017  amgmlem  27018  amgm  27019  wilthlem2  27097  wilthlem3  27098  basellem7  27115  basellem9  27117  lgsfcl  27334  lgsdchr  27384  dchrvmasumlem1  27524  dchrisum0lem3  27548  axlowdimlem4  28879  axlowdimlem7  28882  axlowdimlem10  28885  upgruhgr  29038  konigsbergssiedgw  30183  pliguhgr  30419  0oo  30722  hhsscms  31211  nlelchi  31994  hmopidmchi  32084  pjinvari  32124  padct  32633  smatrcl  33611  lmlim  33762  rge0scvg  33764  lmdvg  33768  lmdvglim  33769  rrhre  33836  esumfsupre  33904  hashf2  33917  eulerpartlems  34194  eulerpartlemgs2  34214  coinfliprv  34316  fdvposlt  34445  fdvposle  34447  breprexpnat  34480  circlemethnat  34487  circlevma  34488  tgoldbachgtde  34506  lfuhgr  34945  subgrwlk  34960  ptpconn  35061  poimirlem8  37329  poimirlem18  37339  poimirlem21  37342  poimirlem22  37343  mblfinlem2  37359  mbfresfi  37367  itg2addnclem  37372  itg2addnclem2  37373  itg2addnc  37375  itg2gt0cn  37376  ftc1anclem8  37401  fdc  37446  heiborlem6  37517  heibor  37522  lfl0f  38767  intlewftc  41760  sticksstones3  41846  sticksstones9  41852  sticksstones11  41854  sticksstones17  41861  sticksstones18  41862  aks6d1c6lem5  41875  mzpexpmpt  42402  mzpresrename  42407  diophrw  42416  rabren3dioph  42472  lnrfg  42780  seff  43983  sblpnf  43984  binomcxplemnotnn0  44030  stoweidlem44  45665  stirlinglem8  45702  fourierdlem62  45789  fouriersw  45852  nnsum3primes4  47360  zlmodzxzldeplem1  47883  aacllem  48549  amgmwlem  48550