Theorem fss 6678

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 3929	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 613	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6496	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6496	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 407	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3890  ran crn 5625   Fn wfn 6487  ⟶wf 6488

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3907  df-f 6496

This theorem is referenced by:  fssd  6679  f1ss  6735  fcdmssb  7068  fsn2  7083  fprb  7142  ofco  7649  ffoss  7892  issmo2  8282  smoiso  8295  ssdomg  8940  alephfplem4  10020  cofsmo  10182  fin23lem17  10251  hsmexlem1  10339  axdc3lem4  10366  ac6s  10397  gruen  10726  intgru  10728  ingru  10729  hashf1lem1  14408  sswrd  14475  repsdf2  14731  limsupgre  15434  abscn2  15552  recn2  15554  imcn2  15555  climabs  15557  climre  15559  climim  15560  rlimabs  15562  rlimre  15564  rlimim  15565  caucvgrlem  15626  caurcvgr  15627  caucvgrlem2  15628  caurcvg  15630  fsumre  15762  fsumim  15763  0ram  16982  ramub1  16990  ramcl  16991  acsinfd  18513  acsdomd  18514  gsumval1  18642  resmgmhm2  18671  resmhm2  18780  prdsgrpd  19017  prdsinvgd  19018  symgtrinv  19438  prdscmnd  19827  prdsabld  19828  pgpfaclem1  20049  prdsrngd  20148  prdsmulrcl  20290  prdsringd  20291  prdscrngd  20292  abvf  20783  prdslmodd  20955  zntoslem  21546  regsumsupp  21612  dsmmsubg  21733  dsmmlss  21734  islinds2  21803  lindsmm  21818  lsslindf  21820  psrridm  21951  coe1fval3  22182  1stccnp  23437  1stckgen  23529  prdstps  23604  pthaus  23613  txcmplem2  23617  ptcmpfi  23788  ptcmplem1  24027  ptcmpg  24032  prdstmdd  24099  prdstgpd  24100  ismet2  24308  prdsxmetlem  24343  imasdsf1olem  24348  prdsms  24506  isngp2  24572  metdscn  24832  lmmbr  25235  causs  25275  ovolfioo  25444  ovolficc  25445  ovolfsf  25448  elovolm  25452  ovollb  25456  ovolunlem1a  25473  ovolunlem1  25474  ovolicc2lem1  25494  ovolicc2lem2  25495  ovolicc2lem3  25496  ovolicc2lem4  25497  ovolicc2  25499  uniiccdif  25555  uniioovol  25556  uniiccvol  25557  uniioombllem2  25560  uniioombllem3a  25561  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  uniioombl  25566  dyadmbl  25577  vitalilem3  25587  vitalilem4  25588  vitalilem5  25589  ismbf  25605  mbfid  25612  0plef  25649  i1f1  25667  i1faddlem  25670  i1fsub  25685  itg1sub  25686  mbfi1fseqlem4  25695  itg2le  25716  itg2mulclem  25723  itg2mulc  25724  itg2monolem1  25727  itg2monolem2  25728  itg2monolem3  25729  itg2mono  25730  itg2i1fseq3  25734  itg2addlem  25735  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  dvfre  25928  dvnfre  25929  dvferm1  25962  dvferm2  25964  rolle  25967  dvgt0lem1  25979  dvivthlem1  25985  dvne0  25988  lhop1lem  25990  lhop2  25992  lhop  25993  dvcnvrelem1  25994  dvcnvre  25996  dvcvx  25997  dvfsumrlim  26008  tdeglem3  26034  elplyr  26176  taylthlem2  26351  taylthlem2OLD  26352  taylth  26353  ulmcn  26377  iblulm  26385  efcvx  26427  dvrelog  26614  relogcn  26615  dvlog2  26630  leibpi  26919  efrlim  26946  efrlimOLD  26947  jensenlem2  26965  jensen  26966  amgmlem  26967  amgm  26968  wilthlem2  27046  wilthlem3  27047  basellem7  27064  basellem9  27066  lgsfcl  27282  lgsdchr  27332  dchrvmasumlem1  27472  dchrisum0lem3  27496  axlowdimlem4  29028  axlowdimlem7  29031  axlowdimlem10  29034  upgruhgr  29185  konigsbergssiedgw  30335  pliguhgr  30572  0oo  30875  hhsscms  31364  nlelchi  32147  hmopidmchi  32237  pjinvari  32277  padct  32806  smatrcl  33956  lmlim  34107  rge0scvg  34109  lmdvg  34113  lmdvglim  34114  rrhre  34181  esumfsupre  34231  hashf2  34244  eulerpartlems  34520  eulerpartlemgs2  34540  coinfliprv  34643  fdvposlt  34759  fdvposle  34761  breprexpnat  34794  circlemethnat  34801  circlevma  34802  tgoldbachgtde  34820  lfuhgr  35316  subgrwlk  35330  ptpconn  35431  poimirlem8  37963  poimirlem18  37973  poimirlem21  37976  poimirlem22  37977  mblfinlem2  37993  mbfresfi  38001  itg2addnclem  38006  itg2addnclem2  38007  itg2addnc  38009  itg2gt0cn  38010  ftc1anclem8  38035  fdc  38080  heiborlem6  38151  heibor  38156  lfl0f  39529  intlewftc  42514  sticksstones3  42601  sticksstones9  42607  sticksstones11  42609  sticksstones17  42616  sticksstones18  42617  aks6d1c6lem5  42630  mzpexpmpt  43191  mzpresrename  43196  diophrw  43205  rabren3dioph  43261  lnrfg  43565  seff  44754  sblpnf  44755  binomcxplemnotnn0  44801  stoweidlem44  46490  stirlinglem8  46527  fourierdlem62  46614  fouriersw  46677  nnsum3primes4  48276  grtriclwlk3  48433  zlmodzxzldeplem1  48988  aacllem  50288  amgmwlem  50289