Theorem fco 6741

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ^◡ccnv 5666   “ cima 5670   ∘ ccom 5671  Fun wfun 6536  ⟶wf 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pr 5414

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-br 5126  df-opab 5188  df-id 5560  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-fun 6544  df-fn 6545  df-f 6546

This theorem is referenced by:  fcod  6742  fco2  6743  mapen  9164  fsuppco2  9426  mapfienlem1  9428  unxpwdom2  9611  wemapwe  9720  cfcoflem  10295  isf34lem7  10402  isf34lem6  10403  inar1  10798  addnqf  10971  mulnqf  10972  axdc4uzlem  14007  seqf1olem2  14066  wrdco  14853  lenco  14854  lo1o1  15551  o1co  15605  caucvgrlem2  15694  fsumcl2lem  15750  fsumadd  15759  fsummulc2  15803  fsumrelem  15826  supcvg  15875  fprodcl2lem  15969  fprodmul  15979  fproddiv  15980  fprodn0  15998  algcvg  16596  cofucl  17909  setccatid  18105  estrccatid  18152  funcestrcsetclem9  18168  funcsetcestrclem9  18183  yonedalem3b  18299  mgmhmco  18701  mhmco  18810  pwsco1mhm  18819  pwsco2mhm  18820  gsumwmhm  18832  efmndcl  18869  f1omvdconj  19437  pmtrfinv  19452  symgtrinv  19463  psgnunilem1  19484  gsumval3lem1  19896  gsumval3  19898  gsumzcl2  19901  gsumzf1o  19903  gsumzaddlem  19912  gsumzmhm  19928  gsumzoppg  19935  gsumzinv  19936  gsumsub  19939  dprdf1o  20025  ablfaclem2  20079  cnfldds  21343  cnflddsOLD  21356  dsmmbas2  21724  f1lindf  21809  lindfmm  21814  psrnegcl  21941  coe1f2  22178  cpmadumatpolylem1  22854  cnco  23239  cnpco  23240  lmcnp  23277  cnmpt11  23636  cnmpt21  23644  qtopcn  23687  fmco  23934  flfcnp  23977  tsmsf1o  24118  tsmsmhm  24119  tsmssub  24122  imasdsf1olem  24347  nrmmetd  24550  isngp2  24573  isngp3  24574  tngngp2  24628  cnmet  24747  cnfldms  24751  cncfco  24888  cnfldcusp  25346  ovolfioo  25457  ovolficc  25458  ovolfsf  25461  ovollb  25469  ovolctb  25480  ovolicc2lem4  25510  ovolicc2  25512  volsup  25546  uniioovol  25569  uniioombllem3a  25574  uniioombllem3  25575  uniioombllem4  25576  uniioombllem5  25577  uniioombl  25579  mbfdm  25616  ismbfcn  25619  mbfres  25634  mbfimaopnlem  25645  cncombf  25648  limccnp  25881  dvcobrOLD  25939  dvcof  25941  dvcjbr  25942  dvcj  25943  dvmptco  25965  dvlip2  25989  itgsubstlem  26044  coecj  26273  coecjOLD  26275  pserulm  26420  jensenlem2  26986  jensen  26987  amgmlem  26988  gamf  27041  dchrinv  27260  motcgrg  28507  vsfval  30599  imsdf  30655  lnocoi  30723  hocofi  31732  homco1  31767  homco2  31943  hmopco  31989  kbass2  32083  kbass5  32086  opsqrlem1  32106  opsqrlem6  32111  pjinvari  32157  fmptco1f1o  32590  fcobij  32680  fcobijfs  32681  mbfmco  34207  dstfrvclim1  34421  reprpmtf1o  34582  mrsubco  35467  mclsppslem  35529  circum  35620  mblfinlem2  37606  mbfresfi  37614  ftc1anclem5  37645  ghomco  37839  rngohomco  37922  tendococl  40715  mapco2g  42670  diophrw  42715  hausgraph  43162  sblpnf  44274  fcoss  45160  limccog  45580  mbfres2cn  45918  volioof  45947  volioofmpt  45954  voliooicof  45956  stoweidlem31  45991  stoweidlem59  46019  subsaliuncllem  46317  sge0resrnlem  46363  hoicvr  46508  ovolval2lem  46603  ovolval2  46604  ovolval3  46607  ovolval4lem1  46609  gricushgr  47832  amgmwlem  49317