Theorem fco 6747

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 6725	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6746	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 592	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6745	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2734	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 481	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6708	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 257	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534  ^◡ccnv 5677   “ cima 5681   ∘ ccom 5682  Fun wfun 6542  ⟶wf 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149  df-opab 5211  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-fun 6550  df-fn 6551  df-f 6552

This theorem is referenced by:  fcod  6749  fco2  6750  f1coOLD  6806  mapen  9166  fsuppco2  9427  mapfienlem1  9429  unxpwdom2  9612  wemapwe  9721  cfcoflem  10296  isf34lem7  10403  isf34lem6  10404  inar1  10799  addnqf  10972  mulnqf  10973  axdc4uzlem  13981  seqf1olem2  14040  wrdco  14815  lenco  14816  lo1o1  15509  o1co  15563  caucvgrlem2  15654  fsumcl2lem  15710  fsumadd  15719  fsummulc2  15763  fsumrelem  15786  supcvg  15835  fprodcl2lem  15927  fprodmul  15937  fproddiv  15938  fprodn0  15956  algcvg  16547  cofucl  17874  setccatid  18073  estrccatid  18122  funcestrcsetclem9  18139  funcsetcestrclem9  18154  yonedalem3b  18271  mgmhmco  18674  mhmco  18775  pwsco1mhm  18784  pwsco2mhm  18785  gsumwmhm  18797  efmndcl  18834  f1omvdconj  19401  pmtrfinv  19416  symgtrinv  19427  psgnunilem1  19448  gsumval3lem1  19860  gsumval3  19862  gsumzcl2  19865  gsumzf1o  19867  gsumzaddlem  19876  gsumzmhm  19892  gsumzoppg  19899  gsumzinv  19900  gsumsub  19903  dprdf1o  19989  ablfaclem2  20043  cnfldds  21291  cnflddsOLD  21304  dsmmbas2  21671  f1lindf  21756  lindfmm  21761  psrass1lemOLD  21874  psrnegcl  21897  coe1f2  22128  cpmadumatpolylem1  22796  cnco  23183  cnpco  23184  lmcnp  23221  cnmpt11  23580  cnmpt21  23588  qtopcn  23631  fmco  23878  flfcnp  23921  tsmsf1o  24062  tsmsmhm  24063  tsmssub  24066  imasdsf1olem  24292  nrmmetd  24496  isngp2  24519  isngp3  24520  tngngp2  24582  cnmet  24701  cnfldms  24705  cncfco  24840  cnfldcusp  25298  ovolfioo  25409  ovolficc  25410  ovolfsf  25413  ovollb  25421  ovolctb  25432  ovolicc2lem4  25462  ovolicc2  25464  volsup  25498  uniioovol  25521  uniioombllem3a  25526  uniioombllem3  25527  uniioombllem4  25528  uniioombllem5  25529  uniioombl  25531  mbfdm  25568  ismbfcn  25571  mbfres  25586  mbfimaopnlem  25597  cncombf  25600  limccnp  25833  dvcobrOLD  25891  dvcof  25893  dvcjbr  25894  dvcj  25895  dvmptco  25917  dvlip2  25941  itgsubstlem  25996  coecj  26226  pserulm  26371  jensenlem2  26933  jensen  26934  amgmlem  26935  gamf  26988  dchrinv  27207  motcgrg  28361  vsfval  30456  imsdf  30512  lnocoi  30580  hocofi  31589  homco1  31624  homco2  31800  hmopco  31846  kbass2  31940  kbass5  31943  opsqrlem1  31963  opsqrlem6  31968  pjinvari  32014  fmptco1f1o  32431  fcobij  32517  fcobijfs  32518  mbfmco  33884  dstfrvclim1  34097  reprpmtf1o  34258  mrsubco  35131  mclsppslem  35193  circum  35278  mblfinlem2  37131  mbfresfi  37139  ftc1anclem5  37170  ghomco  37364  rngohomco  37447  tendococl  40245  mapco2g  42134  diophrw  42179  hausgraph  42633  sblpnf  43747  fcoss  44583  limccog  45008  mbfres2cn  45346  volioof  45375  volioofmpt  45382  voliooicof  45384  stoweidlem31  45419  stoweidlem59  45447  subsaliuncllem  45745  sge0resrnlem  45791  hoicvr  45936  ovolval2lem  46031  ovolval2  46032  ovolval3  46035  ovolval4lem1  46037  gricushgr  47183  amgmwlem  48235