Theorem fco 6771

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 6750	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6770	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 592	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6769	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2746	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 481	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6733	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 257	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ^◡ccnv 5699   “ cima 5703   ∘ ccom 5704  Fun wfun 6567  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-fun 6575  df-fn 6576  df-f 6577

This theorem is referenced by:  fcod  6773  fco2  6774  f1coOLD  6829  mapen  9207  fsuppco2  9472  mapfienlem1  9474  unxpwdom2  9657  wemapwe  9766  cfcoflem  10341  isf34lem7  10448  isf34lem6  10449  inar1  10844  addnqf  11017  mulnqf  11018  axdc4uzlem  14034  seqf1olem2  14093  wrdco  14880  lenco  14881  lo1o1  15578  o1co  15632  caucvgrlem2  15723  fsumcl2lem  15779  fsumadd  15788  fsummulc2  15832  fsumrelem  15855  supcvg  15904  fprodcl2lem  15998  fprodmul  16008  fproddiv  16009  fprodn0  16027  algcvg  16623  cofucl  17952  setccatid  18151  estrccatid  18200  funcestrcsetclem9  18217  funcsetcestrclem9  18232  yonedalem3b  18349  mgmhmco  18752  mhmco  18858  pwsco1mhm  18867  pwsco2mhm  18868  gsumwmhm  18880  efmndcl  18917  f1omvdconj  19488  pmtrfinv  19503  symgtrinv  19514  psgnunilem1  19535  gsumval3lem1  19947  gsumval3  19949  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumzmhm  19979  gsumzoppg  19986  gsumzinv  19987  gsumsub  19990  dprdf1o  20076  ablfaclem2  20130  cnfldds  21399  cnflddsOLD  21412  dsmmbas2  21780  f1lindf  21865  lindfmm  21870  psrnegcl  21997  coe1f2  22232  cpmadumatpolylem1  22908  cnco  23295  cnpco  23296  lmcnp  23333  cnmpt11  23692  cnmpt21  23700  qtopcn  23743  fmco  23990  flfcnp  24033  tsmsf1o  24174  tsmsmhm  24175  tsmssub  24178  imasdsf1olem  24404  nrmmetd  24608  isngp2  24631  isngp3  24632  tngngp2  24694  cnmet  24813  cnfldms  24817  cncfco  24952  cnfldcusp  25410  ovolfioo  25521  ovolficc  25522  ovolfsf  25525  ovollb  25533  ovolctb  25544  ovolicc2lem4  25574  ovolicc2  25576  volsup  25610  uniioovol  25633  uniioombllem3a  25638  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  uniioombl  25643  mbfdm  25680  ismbfcn  25683  mbfres  25698  mbfimaopnlem  25709  cncombf  25712  limccnp  25946  dvcobrOLD  26004  dvcof  26006  dvcjbr  26007  dvcj  26008  dvmptco  26030  dvlip2  26054  itgsubstlem  26109  coecj  26338  pserulm  26483  jensenlem2  27049  jensen  27050  amgmlem  27051  gamf  27104  dchrinv  27323  motcgrg  28570  vsfval  30665  imsdf  30721  lnocoi  30789  hocofi  31798  homco1  31833  homco2  32009  hmopco  32055  kbass2  32149  kbass5  32152  opsqrlem1  32172  opsqrlem6  32177  pjinvari  32223  fmptco1f1o  32652  fcobij  32736  fcobijfs  32737  mbfmco  34229  dstfrvclim1  34442  reprpmtf1o  34603  mrsubco  35489  mclsppslem  35551  circum  35642  mblfinlem2  37618  mbfresfi  37626  ftc1anclem5  37657  ghomco  37851  rngohomco  37934  tendococl  40729  mapco2g  42670  diophrw  42715  hausgraph  43166  sblpnf  44279  fcoss  45117  limccog  45541  mbfres2cn  45879  volioof  45908  volioofmpt  45915  voliooicof  45917  stoweidlem31  45952  stoweidlem59  45980  subsaliuncllem  46278  sge0resrnlem  46324  hoicvr  46469  ovolval2lem  46564  ovolval2  46565  ovolval3  46568  ovolval4lem1  46570  gricushgr  47770  amgmwlem  48896