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  13909  seqf1olem2  13968  wrdco  14757  lenco  14758  lo1o1  15458  o1co  15512  caucvgrlem2  15601  fsumcl2lem  15657  fsumadd  15666  fsummulc2  15710  fsumrelem  15733  supcvg  15782  fprodcl2lem  15876  fprodmul  15886  fproddiv  15887  fprodn0  15905  algcvg  16506  cofucl  17814  setccatid  18010  estrccatid  18057  funcestrcsetclem9  18073  funcsetcestrclem9  18088  yonedalem3b  18204  mgmhmco  18607  mhmco  18716  pwsco1mhm  18725  pwsco2mhm  18726  gsumwmhm  18738  efmndcl  18775  f1omvdconj  19344  pmtrfinv  19359  symgtrinv  19370  psgnunilem1  19391  gsumval3lem1  19803  gsumval3  19805  gsumzcl2  19808  gsumzf1o  19810  gsumzaddlem  19819  gsumzmhm  19835  gsumzoppg  19842  gsumzinv  19843  gsumsub  19846  dprdf1o  19932  ablfaclem2  19986  cnfldds  21292  cnflddsOLD  21305  dsmmbas2  21663  f1lindf  21748  lindfmm  21753  psrnegcl  21880  coe1f2  22111  cpmadumatpolylem1  22785  cnco  23170  cnpco  23171  lmcnp  23208  cnmpt11  23567  cnmpt21  23575  qtopcn  23618  fmco  23865  flfcnp  23908  tsmsf1o  24049  tsmsmhm  24050  tsmssub  24053  imasdsf1olem  24278  nrmmetd  24479  isngp2  24502  isngp3  24503  tngngp2  24557  cnmet  24676  cnfldms  24680  cncfco  24817  cnfldcusp  25274  ovolfioo  25385  ovolficc  25386  ovolfsf  25389  ovollb  25397  ovolctb  25408  ovolicc2lem4  25438  ovolicc2  25440  volsup  25474  uniioovol  25497  uniioombllem3a  25502  uniioombllem3  25503  uniioombllem4  25504  uniioombllem5  25505  uniioombl  25507  mbfdm  25544  ismbfcn  25547  mbfres  25562  mbfimaopnlem  25573  cncombf  25576  limccnp  25809  dvcobrOLD  25867  dvcof  25869  dvcjbr  25870  dvcj  25871  dvmptco  25893  dvlip2  25917  itgsubstlem  25972  coecj  26201  coecjOLD  26203  pserulm  26348  jensenlem2  26915  jensen  26916  amgmlem  26917  gamf  26970  dchrinv  27189  motcgrg  28508  vsfval  30596  imsdf  30652  lnocoi  30720  hocofi  31729  homco1  31764  homco2  31940  hmopco  31986  kbass2  32080  kbass5  32083  opsqrlem1  32103  opsqrlem6  32108  pjinvari  32154  fmptco1f1o  32595  fcobij  32683  fcobijfs  32684  fcobijfs2  32685  mbfmco  34251  dstfrvclim1  34465  reprpmtf1o  34613  mrsubco  35513  mclsppslem  35575  circum  35666  mblfinlem2  37657  mbfresfi  37665  ftc1anclem5  37696  ghomco  37890  rngohomco  37973  tendococl  40771  mapco2g  42707  diophrw  42752  hausgraph  43198  sblpnf  44303  fcoss  45208  limccog  45621  mbfres2cn  45959  volioof  45988  volioofmpt  45995  voliooicof  45997  stoweidlem31  46032  stoweidlem59  46060  subsaliuncllem  46358  sge0resrnlem  46404  hoicvr  46549  ovolval2lem  46644  ovolval2  46645  ovolval3  46648  ovolval4lem1  46650  gricushgr  47921  amgmwlem  49807