Theorem fco 6670

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ^◡ccnv 5610   “ cima 5614   ∘ ccom 5615  Fun wfun 6470  ⟶wf 6472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-fun 6478  df-fn 6479  df-f 6480

This theorem is referenced by:  fcod  6671  fco2  6672  mapen  9049  fsuppco2  9282  mapfienlem1  9284  unxpwdom2  9469  wemapwe  9582  cfcoflem  10158  isf34lem7  10265  isf34lem6  10266  inar1  10661  addnqf  10834  mulnqf  10835  axdc4uzlem  13885  seqf1olem2  13944  wrdco  14733  lenco  14734  lo1o1  15434  o1co  15488  caucvgrlem2  15577  fsumcl2lem  15633  fsumadd  15642  fsummulc2  15686  fsumrelem  15709  supcvg  15758  fprodcl2lem  15852  fprodmul  15862  fproddiv  15863  fprodn0  15881  algcvg  16482  cofucl  17790  setccatid  17986  estrccatid  18033  funcestrcsetclem9  18049  funcsetcestrclem9  18064  yonedalem3b  18180  mgmhmco  18617  mhmco  18726  pwsco1mhm  18735  pwsco2mhm  18736  gsumwmhm  18748  efmndcl  18785  f1omvdconj  19353  pmtrfinv  19368  symgtrinv  19379  psgnunilem1  19400  gsumval3lem1  19812  gsumval3  19814  gsumzcl2  19817  gsumzf1o  19819  gsumzaddlem  19828  gsumzmhm  19844  gsumzoppg  19851  gsumzinv  19852  gsumsub  19855  dprdf1o  19941  ablfaclem2  19995  cnfldds  21298  cnflddsOLD  21311  dsmmbas2  21669  f1lindf  21754  lindfmm  21759  psrnegcl  21886  coe1f2  22117  cpmadumatpolylem1  22791  cnco  23176  cnpco  23177  lmcnp  23214  cnmpt11  23573  cnmpt21  23581  qtopcn  23624  fmco  23871  flfcnp  23914  tsmsf1o  24055  tsmsmhm  24056  tsmssub  24059  imasdsf1olem  24283  nrmmetd  24484  isngp2  24507  isngp3  24508  tngngp2  24562  cnmet  24681  cnfldms  24685  cncfco  24822  cnfldcusp  25279  ovolfioo  25390  ovolficc  25391  ovolfsf  25394  ovollb  25402  ovolctb  25413  ovolicc2lem4  25443  ovolicc2  25445  volsup  25479  uniioovol  25502  uniioombllem3a  25507  uniioombllem3  25508  uniioombllem4  25509  uniioombllem5  25510  uniioombl  25512  mbfdm  25549  ismbfcn  25552  mbfres  25567  mbfimaopnlem  25578  cncombf  25581  limccnp  25814  dvcobrOLD  25872  dvcof  25874  dvcjbr  25875  dvcj  25876  dvmptco  25898  dvlip2  25922  itgsubstlem  25977  coecj  26206  coecjOLD  26208  pserulm  26353  jensenlem2  26920  jensen  26921  amgmlem  26922  gamf  26975  dchrinv  27194  motcgrg  28517  vsfval  30605  imsdf  30661  lnocoi  30729  hocofi  31738  homco1  31773  homco2  31949  hmopco  31995  kbass2  32089  kbass5  32092  opsqrlem1  32112  opsqrlem6  32117  pjinvari  32163  fmptco1f1o  32607  fcobij  32695  fcobijfs  32696  fcobijfs2  32697  mbfmco  34269  dstfrvclim1  34483  reprpmtf1o  34631  mrsubco  35557  mclsppslem  35619  circum  35710  mblfinlem2  37698  mbfresfi  37706  ftc1anclem5  37737  ghomco  37931  rngohomco  38014  tendococl  40811  mapco2g  42747  diophrw  42792  hausgraph  43238  sblpnf  44343  fcoss  45247  limccog  45660  mbfres2cn  45996  volioof  46025  volioofmpt  46032  voliooicof  46034  stoweidlem31  46069  stoweidlem59  46097  subsaliuncllem  46395  sge0resrnlem  46441  hoicvr  46586  ovolval2lem  46681  ovolval2  46682  ovolval3  46685  ovolval4lem1  46687  gricushgr  47948  amgmwlem  49834