Theorem fco 6692

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

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

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 2708  ax-sep 5231  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  fcod  6693  fco2  6694  mapen  9079  fsuppco2  9316  mapfienlem1  9318  unxpwdom2  9503  wemapwe  9618  cfcoflem  10194  isf34lem7  10301  isf34lem6  10302  inar1  10698  addnqf  10871  mulnqf  10872  axdc4uzlem  13945  seqf1olem2  14004  wrdco  14793  lenco  14794  lo1o1  15494  o1co  15548  caucvgrlem2  15637  fsumcl2lem  15693  fsumadd  15702  fsummulc2  15746  fsumrelem  15770  supcvg  15821  fprodcl2lem  15915  fprodmul  15925  fproddiv  15926  fprodn0  15944  algcvg  16545  cofucl  17855  setccatid  18051  estrccatid  18098  funcestrcsetclem9  18114  funcsetcestrclem9  18129  yonedalem3b  18245  mgmhmco  18682  mhmco  18791  pwsco1mhm  18800  pwsco2mhm  18801  gsumwmhm  18813  efmndcl  18850  f1omvdconj  19421  pmtrfinv  19436  symgtrinv  19447  psgnunilem1  19468  gsumval3lem1  19880  gsumval3  19882  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumzmhm  19912  gsumzoppg  19919  gsumzinv  19920  gsumsub  19923  dprdf1o  20009  ablfaclem2  20063  cnfldds  21364  dsmmbas2  21717  f1lindf  21802  lindfmm  21807  psrnegcl  21933  coe1f2  22173  cpmadumatpolylem1  22846  cnco  23231  cnpco  23232  lmcnp  23269  cnmpt11  23628  cnmpt21  23636  qtopcn  23679  fmco  23926  flfcnp  23969  tsmsf1o  24110  tsmsmhm  24111  tsmssub  24114  imasdsf1olem  24338  nrmmetd  24539  isngp2  24562  isngp3  24563  tngngp2  24617  cnmet  24736  cnfldms  24740  cncfco  24874  cnfldcusp  25324  ovolfioo  25434  ovolficc  25435  ovolfsf  25438  ovollb  25446  ovolctb  25457  ovolicc2lem4  25487  ovolicc2  25489  volsup  25523  uniioovol  25546  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  uniioombl  25556  mbfdm  25593  ismbfcn  25596  mbfres  25611  mbfimaopnlem  25622  cncombf  25625  limccnp  25858  dvcof  25915  dvcjbr  25916  dvcj  25917  dvmptco  25939  dvlip2  25962  itgsubstlem  26015  coecj  26243  coecjOLD  26245  pserulm  26387  jensenlem2  26951  jensen  26952  amgmlem  26953  gamf  27006  dchrinv  27224  motcgrg  28612  vsfval  30704  imsdf  30760  lnocoi  30828  hocofi  31837  homco1  31872  homco2  32048  hmopco  32094  kbass2  32188  kbass5  32191  opsqrlem1  32211  opsqrlem6  32216  pjinvari  32262  fmptco1f1o  32706  fcobij  32793  fcobijfs  32794  fcobijfs2  32795  mbfmco  34408  dstfrvclim1  34622  reprpmtf1o  34770  mrsubco  35703  mclsppslem  35765  circum  35856  mblfinlem2  37979  mbfresfi  37987  ftc1anclem5  38018  ghomco  38212  rngohomco  38295  tendococl  41218  mapco2g  43146  diophrw  43191  hausgraph  43633  sblpnf  44737  fcoss  45639  limccog  46050  mbfres2cn  46386  volioof  46415  volioofmpt  46422  voliooicof  46424  stoweidlem31  46459  stoweidlem59  46487  subsaliuncllem  46785  sge0resrnlem  46831  ovolval2lem  47071  ovolval2  47072  ovolval3  47075  ovolval4lem1  47077  gricushgr  48393  amgmwlem  50277