Theorem fco 6679

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 6658	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6678	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 599	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6677	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2745	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 482	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6639	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 258	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  ^◡ccnv 5617   “ cima 5621   ∘ ccom 5622  Fun wfun 6479  ⟶wf 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-fun 6487  df-fn 6488  df-f 6489

This theorem is referenced by:  fcod  6680  fco2  6681  mapen  9069  fsuppco2  9306  mapfienlem1  9308  unxpwdom2  9493  wemapwe  9609  cfcoflem  10185  isf34lem7  10292  isf34lem6  10293  inar1  10689  addnqf  10862  mulnqf  10863  axdc4uzlem  13936  seqf1olem2  13995  wrdco  14784  lenco  14785  lo1o1  15485  o1co  15539  caucvgrlem2  15628  fsumcl2lem  15684  fsumadd  15693  fsummulc2  15737  fsumrelem  15761  supcvg  15812  fprodcl2lem  15906  fprodmul  15916  fproddiv  15917  fprodn0  15935  algcvg  16536  cofucl  17846  setccatid  18042  estrccatid  18089  funcestrcsetclem9  18105  funcsetcestrclem9  18120  yonedalem3b  18236  mgmhmco  18673  mhmco  18782  pwsco1mhm  18791  pwsco2mhm  18792  gsumwmhm  18804  efmndcl  18841  f1omvdconj  19412  pmtrfinv  19427  symgtrinv  19438  psgnunilem1  19459  gsumval3lem1  19871  gsumval3  19873  gsumzcl2  19876  gsumzf1o  19878  gsumzaddlem  19887  gsumzmhm  19903  gsumzoppg  19910  gsumzinv  19911  gsumsub  19914  dprdf1o  20000  ablfaclem2  20054  cnfldds  21359  dsmmbas2  21712  f1lindf  21797  lindfmm  21802  psrnegcl  21929  coe1f2  22194  cpmadumatpolylem1  22864  cnco  23249  cnpco  23250  lmcnp  23287  cnmpt11  23646  cnmpt21  23654  qtopcn  23697  fmco  23944  flfcnp  23987  tsmsf1o  24128  tsmsmhm  24129  tsmssub  24132  imasdsf1olem  24356  nrmmetd  24557  isngp2  24580  isngp3  24581  tngngp2  24635  cnmet  24754  cnfldms  24758  cncfco  24892  cnfldcusp  25342  ovolfioo  25452  ovolficc  25453  ovolfsf  25456  ovollb  25464  ovolctb  25475  ovolicc2lem4  25505  ovolicc2  25507  volsup  25541  uniioovol  25564  uniioombllem3a  25569  uniioombllem3  25570  uniioombllem4  25571  uniioombllem5  25572  uniioombl  25574  mbfdm  25611  ismbfcn  25614  mbfres  25629  mbfimaopnlem  25640  cncombf  25643  limccnp  25876  dvcof  25933  dvcjbr  25934  dvcj  25935  dvmptco  25957  dvlip2  25980  itgsubstlem  26033  coecj  26261  coecjOLD  26263  pserulm  26405  jensenlem2  26969  jensen  26970  amgmlem  26971  gamf  27024  dchrinv  27242  motcgrg  28630  vsfval  30722  imsdf  30778  lnocoi  30846  hocofi  31855  homco1  31890  homco2  32066  hmopco  32112  kbass2  32206  kbass5  32209  opsqrlem1  32229  opsqrlem6  32234  pjinvari  32280  fmptco1f1o  32725  fcobij  32812  fcobijfs  32813  fcobijfs2  32814  mbfmco  34448  dstfrvclim1  34662  reprpmtf1o  34810  mrsubco  35749  mclsppslem  35811  circum  35902  mblfinlem2  38025  mbfresfi  38033  ftc1anclem5  38064  ghomco  38258  rngohomco  38341  tendococl  41264  mapco2g  43163  diophrw  43208  hausgraph  43650  sblpnf  44754  fcoss  45655  limccog  46065  mbfres2cn  46401  volioof  46430  volioofmpt  46437  voliooicof  46439  stoweidlem31  46474  stoweidlem59  46502  subsaliuncllem  46800  sge0resrnlem  46846  ovolval2lem  47086  ovolval2  47087  ovolval3  47090  ovolval4lem1  47092  gricushgr  48408  amgmwlem  50292