Theorem fco 6761

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ^◡ccnv 5688   “ cima 5692   ∘ ccom 5693  Fun wfun 6557  ⟶wf 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-fun 6565  df-fn 6566  df-f 6567

This theorem is referenced by:  fcod  6762  fco2  6763  mapen  9180  fsuppco2  9441  mapfienlem1  9443  unxpwdom2  9626  wemapwe  9735  cfcoflem  10310  isf34lem7  10417  isf34lem6  10418  inar1  10813  addnqf  10986  mulnqf  10987  axdc4uzlem  14021  seqf1olem2  14080  wrdco  14867  lenco  14868  lo1o1  15565  o1co  15619  caucvgrlem2  15708  fsumcl2lem  15764  fsumadd  15773  fsummulc2  15817  fsumrelem  15840  supcvg  15889  fprodcl2lem  15983  fprodmul  15993  fproddiv  15994  fprodn0  16012  algcvg  16610  cofucl  17939  setccatid  18138  estrccatid  18187  funcestrcsetclem9  18204  funcsetcestrclem9  18219  yonedalem3b  18336  mgmhmco  18740  mhmco  18849  pwsco1mhm  18858  pwsco2mhm  18859  gsumwmhm  18871  efmndcl  18908  f1omvdconj  19479  pmtrfinv  19494  symgtrinv  19505  psgnunilem1  19526  gsumval3lem1  19938  gsumval3  19940  gsumzcl2  19943  gsumzf1o  19945  gsumzaddlem  19954  gsumzmhm  19970  gsumzoppg  19977  gsumzinv  19978  gsumsub  19981  dprdf1o  20067  ablfaclem2  20121  cnfldds  21394  cnflddsOLD  21407  dsmmbas2  21775  f1lindf  21860  lindfmm  21865  psrnegcl  21992  coe1f2  22227  cpmadumatpolylem1  22903  cnco  23290  cnpco  23291  lmcnp  23328  cnmpt11  23687  cnmpt21  23695  qtopcn  23738  fmco  23985  flfcnp  24028  tsmsf1o  24169  tsmsmhm  24170  tsmssub  24173  imasdsf1olem  24399  nrmmetd  24603  isngp2  24626  isngp3  24627  tngngp2  24689  cnmet  24808  cnfldms  24812  cncfco  24947  cnfldcusp  25405  ovolfioo  25516  ovolficc  25517  ovolfsf  25520  ovollb  25528  ovolctb  25539  ovolicc2lem4  25569  ovolicc2  25571  volsup  25605  uniioovol  25628  uniioombllem3a  25633  uniioombllem3  25634  uniioombllem4  25635  uniioombllem5  25636  uniioombl  25638  mbfdm  25675  ismbfcn  25678  mbfres  25693  mbfimaopnlem  25704  cncombf  25707  limccnp  25941  dvcobrOLD  25999  dvcof  26001  dvcjbr  26002  dvcj  26003  dvmptco  26025  dvlip2  26049  itgsubstlem  26104  coecj  26333  coecjOLD  26335  pserulm  26480  jensenlem2  27046  jensen  27047  amgmlem  27048  gamf  27101  dchrinv  27320  motcgrg  28567  vsfval  30662  imsdf  30718  lnocoi  30786  hocofi  31795  homco1  31830  homco2  32006  hmopco  32052  kbass2  32146  kbass5  32149  opsqrlem1  32169  opsqrlem6  32174  pjinvari  32220  fmptco1f1o  32650  fcobij  32740  fcobijfs  32741  mbfmco  34246  dstfrvclim1  34459  reprpmtf1o  34620  mrsubco  35506  mclsppslem  35568  circum  35659  mblfinlem2  37645  mbfresfi  37653  ftc1anclem5  37684  ghomco  37878  rngohomco  37961  tendococl  40755  mapco2g  42702  diophrw  42747  hausgraph  43194  sblpnf  44306  fcoss  45153  limccog  45576  mbfres2cn  45914  volioof  45943  volioofmpt  45950  voliooicof  45952  stoweidlem31  45987  stoweidlem59  46015  subsaliuncllem  46313  sge0resrnlem  46359  hoicvr  46504  ovolval2lem  46599  ovolval2  46600  ovolval3  46603  ovolval4lem1  46605  gricushgr  47824  amgmwlem  49033