Theorem fss 6395

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 3896	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 611	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6229	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6229	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 297	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 408	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3859  ran crn 5444   Fn wfn 6220  ⟶wf 6221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-in 3866  df-ss 3874  df-f 6229

This theorem is referenced by:  fssd  6396  f1ss  6448  frnssb  6748  fsn2  6761  fprb  6823  ofco  7287  ffoss  7503  issmo2  7838  smoiso  7851  ssdomg  8403  alephfplem4  9379  cofsmo  9537  fin23lem17  9606  hsmexlem1  9694  axdc3lem4  9721  ac6s  9752  gruen  10080  intgru  10082  ingru  10083  hashf1lem1  13661  sswrd  13715  wrdvOLD  13724  repsdf2  13976  limsupgre  14672  abscn2  14789  recn2  14791  imcn2  14792  climabs  14794  climre  14796  climim  14797  rlimabs  14799  rlimre  14801  rlimim  14802  caucvgrlem  14863  caurcvgr  14864  caucvgrlem2  14865  caurcvg  14867  fsumre  14996  fsumim  14997  0ram  16185  ramub1  16193  ramcl  16194  acsinfd  17619  acsdomd  17620  gsumval1  17716  resmhm2  17799  prdsgrpd  17966  prdsinvgd  17967  symgtrinv  18331  prdscmnd  18704  prdsabld  18705  pgpfaclem1  18920  prdsringd  19052  prdscrngd  19053  abvf  19284  prdslmodd  19431  psrridm  19872  coe1fval3  20059  zntoslem  20385  regsumsupp  20448  dsmmsubg  20569  dsmmlss  20570  islinds2  20639  lindsmm  20654  lsslindf  20656  1stccnp  21754  1stckgen  21846  prdstps  21921  pthaus  21930  txcmplem2  21934  ptcmpfi  22105  ptcmplem1  22344  ptcmpg  22349  prdstmdd  22415  prdstgpd  22416  ismet2  22626  prdsxmetlem  22661  imasdsf1olem  22666  prdsms  22824  isngp2  22889  metdscn  23147  lmmbr  23544  causs  23584  ovolfioo  23751  ovolficc  23752  ovolfsf  23755  elovolm  23759  ovollb  23763  ovolunlem1a  23780  ovolunlem1  23781  ovolicc2lem1  23801  ovolicc2lem2  23802  ovolicc2lem3  23803  ovolicc2lem4  23804  ovolicc2  23806  uniiccdif  23862  uniioovol  23863  uniiccvol  23864  uniioombllem2  23867  uniioombllem3a  23868  uniioombllem3  23869  uniioombllem4  23870  uniioombllem5  23871  uniioombl  23873  dyadmbl  23884  vitalilem3  23894  vitalilem4  23895  vitalilem5  23896  ismbf  23912  mbfid  23919  0plef  23956  i1f1  23974  i1faddlem  23977  i1fsub  23992  itg1sub  23993  mbfi1fseqlem4  24002  itg2le  24023  itg2mulclem  24030  itg2mulc  24031  itg2monolem1  24034  itg2monolem2  24035  itg2monolem3  24036  itg2mono  24037  itg2i1fseq3  24041  itg2addlem  24042  itg2gt0  24044  itg2cnlem1  24045  itg2cnlem2  24046  dvfre  24231  dvnfre  24232  dvferm1  24265  dvferm2  24267  rolle  24270  dvgt0lem1  24282  dvivthlem1  24288  dvne0  24291  lhop1lem  24293  lhop2  24295  lhop  24296  dvcnvrelem1  24297  dvcnvre  24299  dvcvx  24300  dvfsumrlim  24311  tdeglem3  24336  elplyr  24474  taylthlem2  24645  taylth  24646  ulmcn  24670  iblulm  24678  efcvx  24720  dvrelog  24901  relogcn  24902  dvlog2  24917  leibpi  25202  efrlim  25229  jensenlem2  25247  jensen  25248  amgmlem  25249  amgm  25250  wilthlem2  25328  wilthlem3  25329  basellem7  25346  basellem9  25348  lgsfcl  25563  lgsdchr  25613  dchrvmasumlem1  25753  dchrisum0lem3  25777  axlowdimlem4  26414  axlowdimlem7  26417  axlowdimlem10  26420  upgruhgr  26570  konigsbergssiedgw  27719  pliguhgr  27954  0oo  28257  hhsscms  28746  nlelchi  29529  hmopidmchi  29619  pjinvari  29659  padct  30143  smatrcl  30676  lmlim  30807  rge0scvg  30809  lmdvg  30813  lmdvglim  30814  rrhre  30879  esumfsupre  30947  hashf2  30960  eulerpartlems  31235  eulerpartlemgs2  31255  coinfliprv  31357  fdvposlt  31487  fdvposle  31489  breprexpnat  31522  circlemethnat  31529  circlevma  31530  tgoldbachgtde  31548  lfuhgr  31976  subgrwlk  31988  ptpconn  32089  poimirlem8  34450  poimirlem18  34460  poimirlem21  34463  poimirlem22  34464  mblfinlem2  34480  mbfresfi  34488  itg2addnclem  34493  itg2addnclem2  34494  itg2addnc  34496  itg2gt0cn  34497  ftc1anclem8  34524  fdc  34571  heiborlem6  34645  heibor  34650  lfl0f  35755  mzpexpmpt  38846  mzpresrename  38851  diophrw  38860  rabren3dioph  38916  lnrfg  39223  seff  40198  sblpnf  40199  binomcxplemnotnn0  40245  stoweidlem44  41891  stirlinglem8  41928  fourierdlem62  42015  fouriersw  42078  nnsum3primes4  43455  resmgmhm2  43568  zlmodzxzldeplem1  44055  aacllem  44402  amgmwlem  44403