Theorem fco 6694

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 6673	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6693	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 593	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6692	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2735	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 481	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6654	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 257	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ^◡ccnv 5630   “ cima 5634   ∘ ccom 5635  Fun wfun 6493  ⟶wf 6495

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6501  df-fn 6502  df-f 6503

This theorem is referenced by:  fcod  6695  fco2  6696  mapen  9082  fsuppco2  9330  mapfienlem1  9332  unxpwdom2  9517  wemapwe  9626  cfcoflem  10201  isf34lem7  10308  isf34lem6  10309  inar1  10704  addnqf  10877  mulnqf  10878  axdc4uzlem  13924  seqf1olem2  13983  wrdco  14773  lenco  14774  lo1o1  15474  o1co  15528  caucvgrlem2  15617  fsumcl2lem  15673  fsumadd  15682  fsummulc2  15726  fsumrelem  15749  supcvg  15798  fprodcl2lem  15892  fprodmul  15902  fproddiv  15903  fprodn0  15921  algcvg  16522  cofucl  17826  setccatid  18022  estrccatid  18069  funcestrcsetclem9  18085  funcsetcestrclem9  18100  yonedalem3b  18216  mgmhmco  18617  mhmco  18726  pwsco1mhm  18735  pwsco2mhm  18736  gsumwmhm  18748  efmndcl  18785  f1omvdconj  19352  pmtrfinv  19367  symgtrinv  19378  psgnunilem1  19399  gsumval3lem1  19811  gsumval3  19813  gsumzcl2  19816  gsumzf1o  19818  gsumzaddlem  19827  gsumzmhm  19843  gsumzoppg  19850  gsumzinv  19851  gsumsub  19854  dprdf1o  19940  ablfaclem2  19994  cnfldds  21252  cnflddsOLD  21265  dsmmbas2  21622  f1lindf  21707  lindfmm  21712  psrnegcl  21839  coe1f2  22070  cpmadumatpolylem1  22744  cnco  23129  cnpco  23130  lmcnp  23167  cnmpt11  23526  cnmpt21  23534  qtopcn  23577  fmco  23824  flfcnp  23867  tsmsf1o  24008  tsmsmhm  24009  tsmssub  24012  imasdsf1olem  24237  nrmmetd  24438  isngp2  24461  isngp3  24462  tngngp2  24516  cnmet  24635  cnfldms  24639  cncfco  24776  cnfldcusp  25233  ovolfioo  25344  ovolficc  25345  ovolfsf  25348  ovollb  25356  ovolctb  25367  ovolicc2lem4  25397  ovolicc2  25399  volsup  25433  uniioovol  25456  uniioombllem3a  25461  uniioombllem3  25462  uniioombllem4  25463  uniioombllem5  25464  uniioombl  25466  mbfdm  25503  ismbfcn  25506  mbfres  25521  mbfimaopnlem  25532  cncombf  25535  limccnp  25768  dvcobrOLD  25826  dvcof  25828  dvcjbr  25829  dvcj  25830  dvmptco  25852  dvlip2  25876  itgsubstlem  25931  coecj  26160  coecjOLD  26162  pserulm  26307  jensenlem2  26874  jensen  26875  amgmlem  26876  gamf  26929  dchrinv  27148  motcgrg  28447  vsfval  30535  imsdf  30591  lnocoi  30659  hocofi  31668  homco1  31703  homco2  31879  hmopco  31925  kbass2  32019  kbass5  32022  opsqrlem1  32042  opsqrlem6  32047  pjinvari  32093  fmptco1f1o  32530  fcobij  32618  fcobijfs  32619  mbfmco  34228  dstfrvclim1  34442  reprpmtf1o  34590  mrsubco  35481  mclsppslem  35543  circum  35634  mblfinlem2  37625  mbfresfi  37633  ftc1anclem5  37664  ghomco  37858  rngohomco  37941  tendococl  40739  mapco2g  42675  diophrw  42720  hausgraph  43167  sblpnf  44272  fcoss  45177  limccog  45591  mbfres2cn  45929  volioof  45958  volioofmpt  45965  voliooicof  45967  stoweidlem31  46002  stoweidlem59  46030  subsaliuncllem  46328  sge0resrnlem  46374  hoicvr  46519  ovolval2lem  46614  ovolval2  46615  ovolval3  46618  ovolval4lem1  46620  gricushgr  47890  amgmwlem  49764