Theorem fco 6735

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  ^◡ccnv 5649   “ cima 5653   ∘ ccom 5654  Fun wfun 6533  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6541  df-fn 6542  df-f 6543

This theorem is used by:  fcod  6736  fco2  6737  mapen  9164  fsuppco2  9399  mapfienlem1  9401  unxpwdom2  9586  wemapwe  9702  cfcoflem  10354  isf34lem7  10461  isf34lem6  10462  inar1  10864  addnqf  11037  mulnqf  11038  axdc4uzlem  14130  seqf1olem2  14189  wrdco  14987  lenco  14988  lo1o1  15705  o1co  15759  caucvgrlem2  15848  fsumcl2lem  15903  fsumadd  15912  fsummulc2  15956  fsumrelem  15980  supcvg  16031  fprodcl2lem  16123  fprodmul  16133  fproddiv  16134  fprodn0  16152  algcvg  16757  cofucl  18069  setccatid  18265  estrccatid  18312  funcestrcsetclem9  18328  funcsetcestrclem9  18343  yonedalem3b  18459  mgmhmco  18909  mhmco  19025  pwsco1mhm  19034  pwsco2mhm  19035  gsumwmhm  19047  efmndcl  19084  f1omvdconj  19666  pmtrfinv  19681  symgtrinv  19692  psgnunilem1  19713  gsumval3lem1  20125  gsumval3  20127  gsumzcl2  20130  gsumzf1o  20132  gsumzaddlem  20141  gsumzmhm  20157  gsumzoppg  20164  gsumzinv  20165  gsumsub  20168  dprdf1o  20254  ablfaclem2  20308  cnfldds  21696  dsmmbas2  22049  f1lindf  22134  lindfmm  22139  psrnegcl  22268  coe1f2  22533  cpmadumatpolylem1  23205  cnco  23590  cnpco  23591  lmcnp  23628  cnmpt11  23988  cnmpt21  23996  qtopcn  24039  fmco  24286  flfcnp  24329  tsmsf1o  24470  tsmsmhm  24471  tsmssub  24474  imasdsf1olem  24698  nrmmetd  24899  isngp2  24922  isngp3  24923  tngngp2  24977  cnmet  25096  cnfldms  25100  cncfco  25234  cnfldcusp  25684  ovolfioo  25794  ovolficc  25795  ovolfsf  25798  ovollb  25806  ovolctb  25817  ovolicc2lem4  25847  ovolicc2  25849  volsup  25883  uniioovol  25906  uniioombllem3a  25911  uniioombllem3  25912  uniioombllem4  25913  uniioombllem5  25914  uniioombl  25916  mbfdm  25953  ismbfcn  25956  mbfres  25971  mbfimaopnlem  25982  cncombf  25985  limccnp  26217  dvcof  26274  dvcjbr  26275  dvcj  26276  dvmptco  26298  dvlip2  26321  itgsubstlem  26374  coecj  26603  pserulm  26755  jensenlem2  27321  jensen  27322  amgmlem  27323  gamf  27376  dchrinv  27594  motcgrg  29013  vsfval  31241  imsdf  31297  lnocoi  31365  hocofi  32374  homco1  32409  homco2  32585  hmopco  32631  kbass2  32725  kbass5  32728  opsqrlem1  32748  opsqrlem6  32753  pjinvari  32799  fmptco1f1o  33275  fcobij  33359  fcobijfs  33360  fcobijfs2  33361  mbfmco  34943  dstfrvclim1  35157  reprpmtf1o  35302  mrsubco  36373  mclsppslem  36435  circum  36526  mblfinlem2  38670  mbfresfi  38678  ftc1anclem5  38709  ghomco  38919  rngohomco  39002  tendococl  41923  mapco2g  43819  diophrw  43864  hausgraph  44301  sblpnf  45388  fcoss  46317  limccog  46726  mbfres2cn  47062  volioof  47091  volioofmpt  47098  voliooicof  47100  stoweidlem31  47135  stoweidlem59  47163  subsaliuncllem  47461  sge0resrnlem  47507  ovolval2lem  47747  ovolval2  47748  ovolval3  47751  ovolval4lem1  47753  gricushgr  49109  amgmwlem  51156