Theorem fco 6694

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 6673	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6693	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 594	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6692	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2743	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 481	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6654	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 257	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ^◡ccnv 5631   “ cima 5635   ∘ ccom 5636  Fun wfun 6494  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  fcod  6695  fco2  6696  mapen  9081  fsuppco2  9318  mapfienlem1  9320  unxpwdom2  9505  wemapwe  9618  cfcoflem  10194  isf34lem7  10301  isf34lem6  10302  inar1  10698  addnqf  10871  mulnqf  10872  axdc4uzlem  13918  seqf1olem2  13977  wrdco  14766  lenco  14767  lo1o1  15467  o1co  15521  caucvgrlem2  15610  fsumcl2lem  15666  fsumadd  15675  fsummulc2  15719  fsumrelem  15742  supcvg  15791  fprodcl2lem  15885  fprodmul  15895  fproddiv  15896  fprodn0  15914  algcvg  16515  cofucl  17824  setccatid  18020  estrccatid  18067  funcestrcsetclem9  18083  funcsetcestrclem9  18098  yonedalem3b  18214  mgmhmco  18651  mhmco  18760  pwsco1mhm  18769  pwsco2mhm  18770  gsumwmhm  18782  efmndcl  18819  f1omvdconj  19387  pmtrfinv  19402  symgtrinv  19413  psgnunilem1  19434  gsumval3lem1  19846  gsumval3  19848  gsumzcl2  19851  gsumzf1o  19853  gsumzaddlem  19862  gsumzmhm  19878  gsumzoppg  19885  gsumzinv  19886  gsumsub  19889  dprdf1o  19975  ablfaclem2  20029  cnfldds  21333  cnflddsOLD  21346  dsmmbas2  21704  f1lindf  21789  lindfmm  21794  psrnegcl  21922  coe1f2  22162  cpmadumatpolylem1  22837  cnco  23222  cnpco  23223  lmcnp  23260  cnmpt11  23619  cnmpt21  23627  qtopcn  23670  fmco  23917  flfcnp  23960  tsmsf1o  24101  tsmsmhm  24102  tsmssub  24105  imasdsf1olem  24329  nrmmetd  24530  isngp2  24553  isngp3  24554  tngngp2  24608  cnmet  24727  cnfldms  24731  cncfco  24868  cnfldcusp  25325  ovolfioo  25436  ovolficc  25437  ovolfsf  25440  ovollb  25448  ovolctb  25459  ovolicc2lem4  25489  ovolicc2  25491  volsup  25525  uniioovol  25548  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  uniioombl  25558  mbfdm  25595  ismbfcn  25598  mbfres  25613  mbfimaopnlem  25624  cncombf  25627  limccnp  25860  dvcobrOLD  25918  dvcof  25920  dvcjbr  25921  dvcj  25922  dvmptco  25944  dvlip2  25968  itgsubstlem  26023  coecj  26252  coecjOLD  26254  pserulm  26399  jensenlem2  26966  jensen  26967  amgmlem  26968  gamf  27021  dchrinv  27240  motcgrg  28628  vsfval  30721  imsdf  30777  lnocoi  30845  hocofi  31854  homco1  31889  homco2  32065  hmopco  32111  kbass2  32205  kbass5  32208  opsqrlem1  32228  opsqrlem6  32233  pjinvari  32279  fmptco1f1o  32723  fcobij  32810  fcobijfs  32811  fcobijfs2  32812  mbfmco  34442  dstfrvclim1  34656  reprpmtf1o  34804  mrsubco  35737  mclsppslem  35799  circum  35890  mblfinlem2  37909  mbfresfi  37917  ftc1anclem5  37948  ghomco  38142  rngohomco  38225  tendococl  41148  mapco2g  43071  diophrw  43116  hausgraph  43562  sblpnf  44666  fcoss  45568  limccog  45980  mbfres2cn  46316  volioof  46345  volioofmpt  46352  voliooicof  46354  stoweidlem31  46389  stoweidlem59  46417  subsaliuncllem  46715  sge0resrnlem  46761  hoicvr  46906  ovolval2lem  47001  ovolval2  47002  ovolval3  47005  ovolval4lem1  47007  gricushgr  48277  amgmwlem  50161