Theorem fco 6711

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 6689	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6710	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 602	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6709	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2767	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 485	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6670	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 259	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559  ^◡ccnv 5642   “ cima 5646   ∘ ccom 5647  Fun wfun 6510  ⟶wf 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-fun 6518  df-fn 6519  df-f 6520

This theorem is referenced by:  fcod  6712  fco2  6713  mapen  9107  fsuppco2  9343  mapfienlem1  9345  unxpwdom2  9530  wemapwe  9646  cfcoflem  10223  isf34lem7  10330  isf34lem6  10331  inar1  10727  addnqf  10900  mulnqf  10901  axdc4uzlem  13990  seqf1olem2  14049  wrdco  14838  lenco  14839  lo1o1  15550  o1co  15604  caucvgrlem2  15693  fsumcl2lem  15749  fsumadd  15758  fsummulc2  15802  fsumrelem  15826  supcvg  15877  fprodcl2lem  15971  fprodmul  15981  fproddiv  15982  fprodn0  16000  algcvg  16601  cofucl  17912  setccatid  18108  estrccatid  18155  funcestrcsetclem9  18171  funcsetcestrclem9  18186  yonedalem3b  18302  mgmhmco  18739  mhmco  18848  pwsco1mhm  18857  pwsco2mhm  18858  gsumwmhm  18870  efmndcl  18907  f1omvdconj  19477  pmtrfinv  19492  symgtrinv  19503  psgnunilem1  19524  gsumval3lem1  19936  gsumval3  19938  gsumzcl2  19941  gsumzf1o  19943  gsumzaddlem  19952  gsumzmhm  19968  gsumzoppg  19975  gsumzinv  19976  gsumsub  19979  dprdf1o  20065  ablfaclem2  20119  cnfldds  21424  dsmmbas2  21777  f1lindf  21862  lindfmm  21867  psrnegcl  21994  coe1f2  22259  cpmadumatpolylem1  22929  cnco  23314  cnpco  23315  lmcnp  23352  cnmpt11  23711  cnmpt21  23719  qtopcn  23762  fmco  24009  flfcnp  24052  tsmsf1o  24193  tsmsmhm  24194  tsmssub  24197  imasdsf1olem  24421  nrmmetd  24622  isngp2  24645  isngp3  24646  tngngp2  24700  cnmet  24819  cnfldms  24823  cncfco  24957  cnfldcusp  25407  ovolfioo  25517  ovolficc  25518  ovolfsf  25521  ovollb  25529  ovolctb  25540  ovolicc2lem4  25570  ovolicc2  25572  volsup  25606  uniioovol  25629  uniioombllem3a  25634  uniioombllem3  25635  uniioombllem4  25636  uniioombllem5  25637  uniioombl  25639  mbfdm  25676  ismbfcn  25679  mbfres  25694  mbfimaopnlem  25705  cncombf  25708  limccnp  25941  dvcof  25998  dvcjbr  25999  dvcj  26000  dvmptco  26022  dvlip2  26045  itgsubstlem  26098  coecj  26326  coecjOLD  26328  pserulm  26473  jensenlem2  27040  jensen  27041  amgmlem  27042  gamf  27095  dchrinv  27313  motcgrg  28701  vsfval  30793  imsdf  30849  lnocoi  30917  hocofi  31926  homco1  31961  homco2  32137  hmopco  32183  kbass2  32277  kbass5  32280  opsqrlem1  32300  opsqrlem6  32305  pjinvari  32351  fmptco1f1o  32796  fcobij  32883  fcobijfs  32884  fcobijfs2  32885  mbfmco  34522  dstfrvclim1  34736  reprpmtf1o  34881  mrsubco  35832  mclsppslem  35894  circum  35985  mblfinlem2  38118  mbfresfi  38126  ftc1anclem5  38157  ghomco  38351  rngohomco  38434  tendococl  41357  mapco2g  43256  diophrw  43301  hausgraph  43743  sblpnf  44847  fcoss  45747  limccog  46157  mbfres2cn  46493  volioof  46522  volioofmpt  46529  voliooicof  46531  stoweidlem31  46566  stoweidlem59  46594  subsaliuncllem  46892  sge0resrnlem  46938  ovolval2lem  47178  ovolval2  47179  ovolval3  47182  ovolval4lem1  47184  gricushgr  48500  amgmwlem  50384