Theorem fco 6654

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1539  ^◡ccnv 5599   “ cima 5603   ∘ ccom 5604  Fun wfun 6452  ⟶wf 6454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-fun 6460  df-fn 6461  df-f 6462

This theorem is referenced by:  fcod  6656  fco2  6657  f1coOLD  6713  mapen  8966  fsuppco2  9206  mapfienlem1  9208  unxpwdom2  9391  wemapwe  9499  cfcoflem  10074  isf34lem7  10181  isf34lem6  10182  inar1  10577  addnqf  10750  mulnqf  10751  axdc4uzlem  13749  seqf1olem2  13809  wrdco  14589  lenco  14590  lo1o1  15286  o1co  15340  caucvgrlem2  15431  fsumcl2lem  15488  fsumadd  15497  fsummulc2  15541  fsumrelem  15564  supcvg  15613  fprodcl2lem  15705  fprodmul  15715  fproddiv  15716  fprodn0  15734  algcvg  16326  cofucl  17648  setccatid  17844  estrccatid  17893  funcestrcsetclem9  17910  funcsetcestrclem9  17925  yonedalem3b  18042  mhmco  18507  pwsco1mhm  18515  pwsco2mhm  18516  gsumwmhm  18529  efmndcl  18566  f1omvdconj  19099  pmtrfinv  19114  symgtrinv  19125  psgnunilem1  19146  gsumval3lem1  19551  gsumval3  19553  gsumzcl2  19556  gsumzf1o  19558  gsumzaddlem  19567  gsumzmhm  19583  gsumzoppg  19590  gsumzinv  19591  gsumsub  19594  dprdf1o  19680  ablfaclem2  19734  cnfldds  20652  dsmmbas2  20989  f1lindf  21074  lindfmm  21079  psrass1lemOLD  21188  psrnegcl  21210  coe1f2  21425  cpmadumatpolylem1  22075  cnco  22462  cnpco  22463  lmcnp  22500  cnmpt11  22859  cnmpt21  22867  qtopcn  22910  fmco  23157  flfcnp  23200  tsmsf1o  23341  tsmsmhm  23342  tsmssub  23345  imasdsf1olem  23571  nrmmetd  23775  isngp2  23798  isngp3  23799  tngngp2  23861  cnmet  23980  cnfldms  23984  cncfco  24115  cnfldcusp  24566  ovolfioo  24676  ovolficc  24677  ovolfsf  24680  ovollb  24688  ovolctb  24699  ovolicc2lem4  24729  ovolicc2  24731  volsup  24765  uniioovol  24788  uniioombllem3a  24793  uniioombllem3  24794  uniioombllem4  24795  uniioombllem5  24796  uniioombl  24798  mbfdm  24835  ismbfcn  24838  mbfres  24853  mbfimaopnlem  24864  cncombf  24867  limccnp  25100  dvcobr  25155  dvcof  25157  dvcjbr  25158  dvcj  25159  dvmptco  25181  dvlip2  25204  itgsubstlem  25257  coecj  25484  pserulm  25626  jensenlem2  26182  jensen  26183  amgmlem  26184  gamf  26237  dchrinv  26454  motcgrg  26950  vsfval  29040  imsdf  29096  lnocoi  29164  hocofi  30173  homco1  30208  homco2  30384  hmopco  30430  kbass2  30524  kbass5  30527  opsqrlem1  30547  opsqrlem6  30552  pjinvari  30598  fmptco1f1o  31013  fcobij  31102  fcobijfs  31103  mbfmco  32276  dstfrvclim1  32489  reprpmtf1o  32651  mrsubco  33528  mclsppslem  33590  circum  33677  mblfinlem2  35859  mbfresfi  35867  ftc1anclem5  35898  ghomco  36093  rngohomco  36176  tendococl  38828  mapco2g  40573  diophrw  40618  hausgraph  41075  sblpnf  41966  fcoss  42794  limccog  43210  mbfres2cn  43548  volioof  43577  volioofmpt  43584  voliooicof  43586  stoweidlem31  43621  stoweidlem59  43649  subsaliuncllem  43945  sge0resrnlem  43991  hoicvr  44136  ovolval2lem  44231  ovolval2  44232  ovolval3  44235  ovolval4lem1  44237  isomushgr  45336  mgmhmco  45413  amgmwlem  46564