Theorem fco 6764

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 6742	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6763	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 605	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6762	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2769	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 487	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6723	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 260	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ^◡ccnv 5657   “ cima 5661   ∘ ccom 5662  Fun wfun 6560  ⟶wf 6562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-fun 6568  df-fn 6569  df-f 6570

This theorem is used by:  fcod  6765  fco2  6766  mapen  9198  fsuppco2  9432  mapfienlem1  9434  unxpwdom2  9619  wemapwe  9735  cfcoflem  10389  isf34lem7  10496  isf34lem6  10497  inar1  10899  addnqf  11072  mulnqf  11073  axdc4uzlem  14166  seqf1olem2  14225  wrdco  15024  lenco  15025  lo1o1  15743  o1co  15797  caucvgrlem2  15886  fsumcl2lem  15941  fsumadd  15950  fsummulc2  15994  fsumrelem  16018  supcvg  16069  fprodcl2lem  16161  fprodmul  16171  fproddiv  16172  fprodn0  16190  algcvg  16795  cofucl  18113  setccatid  18309  estrccatid  18356  funcestrcsetclem9  18372  funcsetcestrclem9  18387  yonedalem3b  18503  mgmhmco  18953  mhmco  19069  pwsco1mhm  19078  pwsco2mhm  19079  gsumwmhm  19091  efmndcl  19128  f1omvdconj  19711  pmtrfinv  19726  symgtrinv  19737  psgnunilem1  19758  gsumval3lem1  20170  gsumval3  20172  gsumzcl2  20175  gsumzf1o  20177  gsumzaddlem  20186  gsumzmhm  20202  gsumzoppg  20209  gsumzinv  20210  gsumsub  20213  dprdf1o  20299  ablfaclem2  20353  cnfldds  21741  dsmmbas2  22098  f1lindf  22183  lindfmm  22188  psrnegcl  22317  coe1f2  22582  cpmadumatpolylem1  23254  cnco  23639  cnpco  23640  lmcnp  23677  cnmpt11  24037  cnmpt21  24045  qtopcn  24088  fmco  24335  flfcnp  24378  tsmsf1o  24519  tsmsmhm  24520  tsmssub  24523  imasdsf1olem  24747  nrmmetd  24948  isngp2  24971  isngp3  24972  tngngp2  25026  cnmet  25145  cnfldms  25149  cncfco  25283  cnfldcusp  25733  ovolfioo  25843  ovolficc  25844  ovolfsf  25847  ovollb  25855  ovolctb  25866  ovolicc2lem4  25896  ovolicc2  25898  volsup  25932  uniioovol  25955  uniioombllem3a  25960  uniioombllem3  25961  uniioombllem4  25962  uniioombllem5  25963  uniioombl  25965  mbfdm  26002  ismbfcn  26005  mbfres  26020  mbfimaopnlem  26031  cncombf  26034  limccnp  26266  dvcof  26323  dvcjbr  26324  dvcj  26325  dvmptco  26347  dvlip2  26370  itgsubstlem  26423  coecj  26652  pserulm  26806  jensenlem2  27372  jensen  27373  amgmlem  27374  gamf  27427  dchrinv  27645  motcgrg  29064  vsfval  31292  imsdf  31348  lnocoi  31416  hocofi  32425  homco1  32460  homco2  32636  hmopco  32682  kbass2  32776  kbass5  32779  opsqrlem1  32799  opsqrlem6  32804  pjinvari  32850  fmptco1f1o  33325  fcobij  33408  fcobijfs  33409  fcobijfs2  33410  mbfmco  35007  dstfrvclim1  35221  reprpmtf1o  35366  mrsubco  36494  mclsppslem  36556  circum  36647  mblfinlem2  38844  mbfresfi  38852  ftc1anclem5  38883  ghomco  39091  rngohomco  39174  tendococl  42095  mapco2g  43991  diophrw  44036  hausgraph  44468  sblpnf  45555  fcoss  46496  limccog  46905  mbfres2cn  47241  volioof  47270  volioofmpt  47277  voliooicof  47279  stoweidlem31  47314  stoweidlem59  47342  subsaliuncllem  47640  sge0resrnlem  47686  ovolval2lem  47926  ovolval2  47927  ovolval3  47930  ovolval4lem1  47932  gricushgr  49288  amgmwlem  51415