Theorem fco 6735

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ^◡ccnv 5658   “ cima 5662   ∘ ccom 5663  Fun wfun 6530  ⟶wf 6532

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  fcod  6736  fco2  6737  mapen  9160  fsuppco2  9420  mapfienlem1  9422  unxpwdom2  9607  wemapwe  9716  cfcoflem  10291  isf34lem7  10398  isf34lem6  10399  inar1  10794  addnqf  10967  mulnqf  10968  axdc4uzlem  14006  seqf1olem2  14065  wrdco  14855  lenco  14856  lo1o1  15553  o1co  15607  caucvgrlem2  15696  fsumcl2lem  15752  fsumadd  15761  fsummulc2  15805  fsumrelem  15828  supcvg  15877  fprodcl2lem  15971  fprodmul  15981  fproddiv  15982  fprodn0  16000  algcvg  16600  cofucl  17906  setccatid  18102  estrccatid  18149  funcestrcsetclem9  18165  funcsetcestrclem9  18180  yonedalem3b  18296  mgmhmco  18697  mhmco  18806  pwsco1mhm  18815  pwsco2mhm  18816  gsumwmhm  18828  efmndcl  18865  f1omvdconj  19432  pmtrfinv  19447  symgtrinv  19458  psgnunilem1  19479  gsumval3lem1  19891  gsumval3  19893  gsumzcl2  19896  gsumzf1o  19898  gsumzaddlem  19907  gsumzmhm  19923  gsumzoppg  19930  gsumzinv  19931  gsumsub  19934  dprdf1o  20020  ablfaclem2  20074  cnfldds  21332  cnflddsOLD  21345  dsmmbas2  21702  f1lindf  21787  lindfmm  21792  psrnegcl  21919  coe1f2  22150  cpmadumatpolylem1  22824  cnco  23209  cnpco  23210  lmcnp  23247  cnmpt11  23606  cnmpt21  23614  qtopcn  23657  fmco  23904  flfcnp  23947  tsmsf1o  24088  tsmsmhm  24089  tsmssub  24092  imasdsf1olem  24317  nrmmetd  24518  isngp2  24541  isngp3  24542  tngngp2  24596  cnmet  24715  cnfldms  24719  cncfco  24856  cnfldcusp  25314  ovolfioo  25425  ovolficc  25426  ovolfsf  25429  ovollb  25437  ovolctb  25448  ovolicc2lem4  25478  ovolicc2  25480  volsup  25514  uniioovol  25537  uniioombllem3a  25542  uniioombllem3  25543  uniioombllem4  25544  uniioombllem5  25545  uniioombl  25547  mbfdm  25584  ismbfcn  25587  mbfres  25602  mbfimaopnlem  25613  cncombf  25616  limccnp  25849  dvcobrOLD  25907  dvcof  25909  dvcjbr  25910  dvcj  25911  dvmptco  25933  dvlip2  25957  itgsubstlem  26012  coecj  26241  coecjOLD  26243  pserulm  26388  jensenlem2  26955  jensen  26956  amgmlem  26957  gamf  27010  dchrinv  27229  motcgrg  28528  vsfval  30619  imsdf  30675  lnocoi  30743  hocofi  31752  homco1  31787  homco2  31963  hmopco  32009  kbass2  32103  kbass5  32106  opsqrlem1  32126  opsqrlem6  32131  pjinvari  32177  fmptco1f1o  32616  fcobij  32704  fcobijfs  32705  mbfmco  34301  dstfrvclim1  34515  reprpmtf1o  34663  mrsubco  35548  mclsppslem  35610  circum  35701  mblfinlem2  37687  mbfresfi  37695  ftc1anclem5  37726  ghomco  37920  rngohomco  38003  tendococl  40796  mapco2g  42712  diophrw  42757  hausgraph  43204  sblpnf  44309  fcoss  45214  limccog  45629  mbfres2cn  45967  volioof  45996  volioofmpt  46003  voliooicof  46005  stoweidlem31  46040  stoweidlem59  46068  subsaliuncllem  46366  sge0resrnlem  46412  hoicvr  46557  ovolval2lem  46652  ovolval2  46653  ovolval3  46656  ovolval4lem1  46658  gricushgr  47910  amgmwlem  49646