Theorem fss 6732

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

Syntax hints:   → wi 4   ∧ wa 397   ⊆ wss 3948  ran crn 5677   Fn wfn 6536  ⟶wf 6537

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-f 6545

This theorem is referenced by:  fssd  6733  f1ss  6791  fcdmssb  7118  fsn2  7131  fprb  7192  ofco  7690  ffoss  7929  issmo2  8346  smoiso  8359  ssdomg  8993  alephfplem4  10099  cofsmo  10261  fin23lem17  10330  hsmexlem1  10418  axdc3lem4  10445  ac6s  10476  gruen  10804  intgru  10806  ingru  10807  hashf1lem1  14412  hashf1lem1OLD  14413  sswrd  14469  repsdf2  14725  limsupgre  15422  abscn2  15540  recn2  15542  imcn2  15543  climabs  15545  climre  15547  climim  15548  rlimabs  15550  rlimre  15552  rlimim  15553  caucvgrlem  15616  caurcvgr  15617  caucvgrlem2  15618  caurcvg  15620  fsumre  15751  fsumim  15752  0ram  16950  ramub1  16958  ramcl  16959  acsinfd  18506  acsdomd  18507  gsumval1  18599  resmhm2  18699  prdsgrpd  18930  prdsinvgd  18931  symgtrinv  19335  prdscmnd  19724  prdsabld  19725  pgpfaclem1  19946  prdsringd  20128  prdscrngd  20129  abvf  20424  prdslmodd  20573  zntoslem  21104  regsumsupp  21167  dsmmsubg  21290  dsmmlss  21291  islinds2  21360  lindsmm  21375  lsslindf  21377  psrridm  21516  coe1fval3  21724  1stccnp  22958  1stckgen  23050  prdstps  23125  pthaus  23134  txcmplem2  23138  ptcmpfi  23309  ptcmplem1  23548  ptcmpg  23553  prdstmdd  23620  prdstgpd  23621  ismet2  23831  prdsxmetlem  23866  imasdsf1olem  23871  prdsms  24032  isngp2  24098  metdscn  24364  lmmbr  24767  causs  24807  ovolfioo  24976  ovolficc  24977  ovolfsf  24980  elovolm  24984  ovollb  24988  ovolunlem1a  25005  ovolunlem1  25006  ovolicc2lem1  25026  ovolicc2lem2  25027  ovolicc2lem3  25028  ovolicc2lem4  25029  ovolicc2  25031  uniiccdif  25087  uniioovol  25088  uniiccvol  25089  uniioombllem2  25092  uniioombllem3a  25093  uniioombllem3  25094  uniioombllem4  25095  uniioombllem5  25096  uniioombl  25098  dyadmbl  25109  vitalilem3  25119  vitalilem4  25120  vitalilem5  25121  ismbf  25137  mbfid  25144  0plef  25181  i1f1  25199  i1faddlem  25202  i1fsub  25218  itg1sub  25219  mbfi1fseqlem4  25228  itg2le  25249  itg2mulclem  25256  itg2mulc  25257  itg2monolem1  25260  itg2monolem2  25261  itg2monolem3  25262  itg2mono  25263  itg2i1fseq3  25267  itg2addlem  25268  itg2gt0  25270  itg2cnlem1  25271  itg2cnlem2  25272  dvfre  25460  dvnfre  25461  dvferm1  25494  dvferm2  25496  rolle  25499  dvgt0lem1  25511  dvivthlem1  25517  dvne0  25520  lhop1lem  25522  lhop2  25524  lhop  25525  dvcnvrelem1  25526  dvcnvre  25528  dvcvx  25529  dvfsumrlim  25540  tdeglem3  25567  tdeglem3OLD  25568  elplyr  25707  taylthlem2  25878  taylth  25879  ulmcn  25903  iblulm  25911  efcvx  25953  dvrelog  26137  relogcn  26138  dvlog2  26153  leibpi  26437  efrlim  26464  jensenlem2  26482  jensen  26483  amgmlem  26484  amgm  26485  wilthlem2  26563  wilthlem3  26564  basellem7  26581  basellem9  26583  lgsfcl  26798  lgsdchr  26848  dchrvmasumlem1  26988  dchrisum0lem3  27012  axlowdimlem4  28193  axlowdimlem7  28196  axlowdimlem10  28199  upgruhgr  28352  konigsbergssiedgw  29493  pliguhgr  29727  0oo  30030  hhsscms  30519  nlelchi  31302  hmopidmchi  31392  pjinvari  31432  padct  31932  smatrcl  32765  lmlim  32916  rge0scvg  32918  lmdvg  32922  lmdvglim  32923  rrhre  32990  esumfsupre  33058  hashf2  33071  eulerpartlems  33348  eulerpartlemgs2  33368  coinfliprv  33470  fdvposlt  33600  fdvposle  33602  breprexpnat  33635  circlemethnat  33642  circlevma  33643  tgoldbachgtde  33661  lfuhgr  34097  subgrwlk  34112  ptpconn  34213  poimirlem8  36485  poimirlem18  36495  poimirlem21  36498  poimirlem22  36499  mblfinlem2  36515  mbfresfi  36523  itg2addnclem  36528  itg2addnclem2  36529  itg2addnc  36531  itg2gt0cn  36532  ftc1anclem8  36557  fdc  36602  heiborlem6  36673  heibor  36678  lfl0f  37928  intlewftc  40915  sticksstones3  40953  sticksstones9  40959  sticksstones11  40961  sticksstones17  40968  sticksstones18  40969  mzpexpmpt  41469  mzpresrename  41474  diophrw  41483  rabren3dioph  41539  lnrfg  41847  seff  43054  sblpnf  43055  binomcxplemnotnn0  43101  stoweidlem44  44747  stirlinglem8  44784  fourierdlem62  44871  fouriersw  44934  nnsum3primes4  46443  resmgmhm2  46556  prdsrngd  46664  zlmodzxzldeplem1  47135  aacllem  47802  amgmwlem  47803