Theorem fco 6680

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ^◡ccnv 5622   “ cima 5626   ∘ ccom 5627  Fun wfun 6480  ⟶wf 6482

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 5238  ax-nul 5248  ax-pr 5374

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  fcod  6681  fco2  6682  mapen  9065  fsuppco2  9312  mapfienlem1  9314  unxpwdom2  9499  wemapwe  9612  cfcoflem  10185  isf34lem7  10292  isf34lem6  10293  inar1  10688  addnqf  10861  mulnqf  10862  axdc4uzlem  13908  seqf1olem2  13967  wrdco  14756  lenco  14757  lo1o1  15457  o1co  15511  caucvgrlem2  15600  fsumcl2lem  15656  fsumadd  15665  fsummulc2  15709  fsumrelem  15732  supcvg  15781  fprodcl2lem  15875  fprodmul  15885  fproddiv  15886  fprodn0  15904  algcvg  16505  cofucl  17813  setccatid  18009  estrccatid  18056  funcestrcsetclem9  18072  funcsetcestrclem9  18087  yonedalem3b  18203  mgmhmco  18606  mhmco  18715  pwsco1mhm  18724  pwsco2mhm  18725  gsumwmhm  18737  efmndcl  18774  f1omvdconj  19343  pmtrfinv  19358  symgtrinv  19369  psgnunilem1  19390  gsumval3lem1  19802  gsumval3  19804  gsumzcl2  19807  gsumzf1o  19809  gsumzaddlem  19818  gsumzmhm  19834  gsumzoppg  19841  gsumzinv  19842  gsumsub  19845  dprdf1o  19931  ablfaclem2  19985  cnfldds  21291  cnflddsOLD  21304  dsmmbas2  21662  f1lindf  21747  lindfmm  21752  psrnegcl  21879  coe1f2  22110  cpmadumatpolylem1  22784  cnco  23169  cnpco  23170  lmcnp  23207  cnmpt11  23566  cnmpt21  23574  qtopcn  23617  fmco  23864  flfcnp  23907  tsmsf1o  24048  tsmsmhm  24049  tsmssub  24052  imasdsf1olem  24277  nrmmetd  24478  isngp2  24501  isngp3  24502  tngngp2  24556  cnmet  24675  cnfldms  24679  cncfco  24816  cnfldcusp  25273  ovolfioo  25384  ovolficc  25385  ovolfsf  25388  ovollb  25396  ovolctb  25407  ovolicc2lem4  25437  ovolicc2  25439  volsup  25473  uniioovol  25496  uniioombllem3a  25501  uniioombllem3  25502  uniioombllem4  25503  uniioombllem5  25504  uniioombl  25506  mbfdm  25543  ismbfcn  25546  mbfres  25561  mbfimaopnlem  25572  cncombf  25575  limccnp  25808  dvcobrOLD  25866  dvcof  25868  dvcjbr  25869  dvcj  25870  dvmptco  25892  dvlip2  25916  itgsubstlem  25971  coecj  26200  coecjOLD  26202  pserulm  26347  jensenlem2  26914  jensen  26915  amgmlem  26916  gamf  26969  dchrinv  27188  motcgrg  28507  vsfval  30595  imsdf  30651  lnocoi  30719  hocofi  31728  homco1  31763  homco2  31939  hmopco  31985  kbass2  32079  kbass5  32082  opsqrlem1  32102  opsqrlem6  32107  pjinvari  32153  fmptco1f1o  32590  fcobij  32678  fcobijfs  32679  mbfmco  34234  dstfrvclim1  34448  reprpmtf1o  34596  mrsubco  35496  mclsppslem  35558  circum  35649  mblfinlem2  37640  mbfresfi  37648  ftc1anclem5  37679  ghomco  37873  rngohomco  37956  tendococl  40754  mapco2g  42690  diophrw  42735  hausgraph  43181  sblpnf  44286  fcoss  45191  limccog  45605  mbfres2cn  45943  volioof  45972  volioofmpt  45979  voliooicof  45981  stoweidlem31  46016  stoweidlem59  46044  subsaliuncllem  46342  sge0resrnlem  46388  hoicvr  46533  ovolval2lem  46628  ovolval2  46629  ovolval3  46632  ovolval4lem1  46634  gricushgr  47905  amgmwlem  49791