Theorem fco 6686

Description: Composition of two functions with domain and codomain as a function with domain and codomain. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) (Proof shortened by AV, 20-Sep-2024.)

Assertion

Ref	Expression
fco	⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Proof of Theorem fco

Step	Hyp	Ref	Expression
1		ffun 6665	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6685	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 593	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6684	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2742	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 481	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6646	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 257	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ^◡ccnv 5623   “ cima 5627   ∘ ccom 5628  Fun wfun 6486  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fcod  6687  fco2  6688  mapen  9069  fsuppco2  9306  mapfienlem1  9308  unxpwdom2  9493  wemapwe  9606  cfcoflem  10182  isf34lem7  10289  isf34lem6  10290  inar1  10686  addnqf  10859  mulnqf  10860  axdc4uzlem  13906  seqf1olem2  13965  wrdco  14754  lenco  14755  lo1o1  15455  o1co  15509  caucvgrlem2  15598  fsumcl2lem  15654  fsumadd  15663  fsummulc2  15707  fsumrelem  15730  supcvg  15779  fprodcl2lem  15873  fprodmul  15883  fproddiv  15884  fprodn0  15902  algcvg  16503  cofucl  17812  setccatid  18008  estrccatid  18055  funcestrcsetclem9  18071  funcsetcestrclem9  18086  yonedalem3b  18202  mgmhmco  18639  mhmco  18748  pwsco1mhm  18757  pwsco2mhm  18758  gsumwmhm  18770  efmndcl  18807  f1omvdconj  19375  pmtrfinv  19390  symgtrinv  19401  psgnunilem1  19422  gsumval3lem1  19834  gsumval3  19836  gsumzcl2  19839  gsumzf1o  19841  gsumzaddlem  19850  gsumzmhm  19866  gsumzoppg  19873  gsumzinv  19874  gsumsub  19877  dprdf1o  19963  ablfaclem2  20017  cnfldds  21321  cnflddsOLD  21334  dsmmbas2  21692  f1lindf  21777  lindfmm  21782  psrnegcl  21910  coe1f2  22150  cpmadumatpolylem1  22825  cnco  23210  cnpco  23211  lmcnp  23248  cnmpt11  23607  cnmpt21  23615  qtopcn  23658  fmco  23905  flfcnp  23948  tsmsf1o  24089  tsmsmhm  24090  tsmssub  24093  imasdsf1olem  24317  nrmmetd  24518  isngp2  24541  isngp3  24542  tngngp2  24596  cnmet  24715  cnfldms  24719  cncfco  24856  cnfldcusp  25313  ovolfioo  25424  ovolficc  25425  ovolfsf  25428  ovollb  25436  ovolctb  25447  ovolicc2lem4  25477  ovolicc2  25479  volsup  25513  uniioovol  25536  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombl  25546  mbfdm  25583  ismbfcn  25586  mbfres  25601  mbfimaopnlem  25612  cncombf  25615  limccnp  25848  dvcobrOLD  25906  dvcof  25908  dvcjbr  25909  dvcj  25910  dvmptco  25932  dvlip2  25956  itgsubstlem  26011  coecj  26240  coecjOLD  26242  pserulm  26387  jensenlem2  26954  jensen  26955  amgmlem  26956  gamf  27009  dchrinv  27228  motcgrg  28616  vsfval  30708  imsdf  30764  lnocoi  30832  hocofi  31841  homco1  31876  homco2  32052  hmopco  32098  kbass2  32192  kbass5  32195  opsqrlem1  32215  opsqrlem6  32220  pjinvari  32266  fmptco1f1o  32711  fcobij  32799  fcobijfs  32800  fcobijfs2  32801  mbfmco  34421  dstfrvclim1  34635  reprpmtf1o  34783  mrsubco  35715  mclsppslem  35777  circum  35868  mblfinlem2  37859  mbfresfi  37867  ftc1anclem5  37898  ghomco  38092  rngohomco  38175  tendococl  41032  mapco2g  42956  diophrw  43001  hausgraph  43447  sblpnf  44551  fcoss  45454  limccog  45866  mbfres2cn  46202  volioof  46231  volioofmpt  46238  voliooicof  46240  stoweidlem31  46275  stoweidlem59  46303  subsaliuncllem  46601  sge0resrnlem  46647  hoicvr  46792  ovolval2lem  46887  ovolval2  46888  ovolval3  46891  ovolval4lem1  46893  gricushgr  48163  amgmwlem  50047