Theorem fco 6742

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 6721	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6741	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 594	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6740	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2739	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 483	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6704	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 257	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  ^◡ccnv 5676   “ cima 5680   ∘ ccom 5681  Fun wfun 6538  ⟶wf 6540

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-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-fun 6546  df-fn 6547  df-f 6548

This theorem is referenced by:  fcod  6744  fco2  6745  f1coOLD  6801  mapen  9141  fsuppco2  9398  mapfienlem1  9400  unxpwdom2  9583  wemapwe  9692  cfcoflem  10267  isf34lem7  10374  isf34lem6  10375  inar1  10770  addnqf  10943  mulnqf  10944  axdc4uzlem  13948  seqf1olem2  14008  wrdco  14782  lenco  14783  lo1o1  15476  o1co  15530  caucvgrlem2  15621  fsumcl2lem  15677  fsumadd  15686  fsummulc2  15730  fsumrelem  15753  supcvg  15802  fprodcl2lem  15894  fprodmul  15904  fproddiv  15905  fprodn0  15923  algcvg  16513  cofucl  17838  setccatid  18034  estrccatid  18083  funcestrcsetclem9  18100  funcsetcestrclem9  18115  yonedalem3b  18232  mhmco  18704  pwsco1mhm  18713  pwsco2mhm  18714  gsumwmhm  18726  efmndcl  18763  f1omvdconj  19314  pmtrfinv  19329  symgtrinv  19340  psgnunilem1  19361  gsumval3lem1  19773  gsumval3  19775  gsumzcl2  19778  gsumzf1o  19780  gsumzaddlem  19789  gsumzmhm  19805  gsumzoppg  19812  gsumzinv  19813  gsumsub  19816  dprdf1o  19902  ablfaclem2  19956  cnfldds  20954  dsmmbas2  21292  f1lindf  21377  lindfmm  21382  psrass1lemOLD  21493  psrnegcl  21515  coe1f2  21733  cpmadumatpolylem1  22383  cnco  22770  cnpco  22771  lmcnp  22808  cnmpt11  23167  cnmpt21  23175  qtopcn  23218  fmco  23465  flfcnp  23508  tsmsf1o  23649  tsmsmhm  23650  tsmssub  23653  imasdsf1olem  23879  nrmmetd  24083  isngp2  24106  isngp3  24107  tngngp2  24169  cnmet  24288  cnfldms  24292  cncfco  24423  cnfldcusp  24874  ovolfioo  24984  ovolficc  24985  ovolfsf  24988  ovollb  24996  ovolctb  25007  ovolicc2lem4  25037  ovolicc2  25039  volsup  25073  uniioovol  25096  uniioombllem3a  25101  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  uniioombl  25106  mbfdm  25143  ismbfcn  25146  mbfres  25161  mbfimaopnlem  25172  cncombf  25175  limccnp  25408  dvcobr  25463  dvcof  25465  dvcjbr  25466  dvcj  25467  dvmptco  25489  dvlip2  25512  itgsubstlem  25565  coecj  25792  pserulm  25934  jensenlem2  26492  jensen  26493  amgmlem  26494  gamf  26547  dchrinv  26764  motcgrg  27795  vsfval  29886  imsdf  29942  lnocoi  30010  hocofi  31019  homco1  31054  homco2  31230  hmopco  31276  kbass2  31370  kbass5  31373  opsqrlem1  31393  opsqrlem6  31398  pjinvari  31444  fmptco1f1o  31857  fcobij  31947  fcobijfs  31948  mbfmco  33263  dstfrvclim1  33476  reprpmtf1o  33638  mrsubco  34512  mclsppslem  34574  circum  34659  mblfinlem2  36526  mbfresfi  36534  ftc1anclem5  36565  ghomco  36759  rngohomco  36842  tendococl  39643  mapco2g  41452  diophrw  41497  hausgraph  41954  sblpnf  43069  fcoss  43909  limccog  44336  mbfres2cn  44674  volioof  44703  volioofmpt  44710  voliooicof  44712  stoweidlem31  44747  stoweidlem59  44775  subsaliuncllem  45073  sge0resrnlem  45119  hoicvr  45264  ovolval2lem  45359  ovolval2  45360  ovolval3  45363  ovolval4lem1  45365  isomushgr  46494  mgmhmco  46571  amgmwlem  47849