Theorem fco 6734

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 6712	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6733	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 605	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6732	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2771	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 487	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6693	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 260	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ^◡ccnv 5662   “ cima 5666   ∘ ccom 5667  Fun wfun 6534  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6542  df-fn 6543  df-f 6544

This theorem is used by:  fcod  6735  fco2  6736  mapen  9132  fsuppco2  9366  mapfienlem1  9368  unxpwdom2  9553  wemapwe  9669  cfcoflem  10267  isf34lem7  10374  isf34lem6  10375  inar1  10771  addnqf  10944  mulnqf  10945  axdc4uzlem  14033  seqf1olem2  14092  wrdco  14888  lenco  14889  lo1o1  15603  o1co  15657  caucvgrlem2  15746  fsumcl2lem  15801  fsumadd  15810  fsummulc2  15854  fsumrelem  15878  supcvg  15929  fprodcl2lem  16023  fprodmul  16033  fproddiv  16034  fprodn0  16052  algcvg  16652  cofucl  17963  setccatid  18159  estrccatid  18206  funcestrcsetclem9  18222  funcsetcestrclem9  18237  yonedalem3b  18353  mgmhmco  18794  mhmco  18906  pwsco1mhm  18915  pwsco2mhm  18916  gsumwmhm  18928  efmndcl  18965  f1omvdconj  19540  pmtrfinv  19555  symgtrinv  19566  psgnunilem1  19587  gsumval3lem1  19999  gsumval3  20001  gsumzcl2  20004  gsumzf1o  20006  gsumzaddlem  20015  gsumzmhm  20031  gsumzoppg  20038  gsumzinv  20039  gsumsub  20042  dprdf1o  20128  ablfaclem2  20182  cnfldds  21564  dsmmbas2  21917  f1lindf  22002  lindfmm  22007  psrnegcl  22134  coe1f2  22399  cpmadumatpolylem1  23068  cnco  23453  cnpco  23454  lmcnp  23491  cnmpt11  23851  cnmpt21  23859  qtopcn  23902  fmco  24149  flfcnp  24192  tsmsf1o  24333  tsmsmhm  24334  tsmssub  24337  imasdsf1olem  24561  nrmmetd  24762  isngp2  24785  isngp3  24786  tngngp2  24840  cnmet  24959  cnfldms  24963  cncfco  25097  cnfldcusp  25547  ovolfioo  25657  ovolficc  25658  ovolfsf  25661  ovollb  25669  ovolctb  25680  ovolicc2lem4  25710  ovolicc2  25712  volsup  25746  uniioovol  25769  uniioombllem3a  25774  uniioombllem3  25775  uniioombllem4  25776  uniioombllem5  25777  uniioombl  25779  mbfdm  25816  ismbfcn  25819  mbfres  25834  mbfimaopnlem  25845  cncombf  25848  limccnp  26081  dvcof  26138  dvcjbr  26139  dvcj  26140  dvmptco  26162  dvlip2  26185  itgsubstlem  26238  coecj  26466  coecjOLD  26468  pserulm  26616  jensenlem2  27183  jensen  27184  amgmlem  27185  gamf  27238  dchrinv  27456  motcgrg  28844  vsfval  31032  imsdf  31088  lnocoi  31156  hocofi  32165  homco1  32200  homco2  32376  hmopco  32422  kbass2  32516  kbass5  32519  opsqrlem1  32539  opsqrlem6  32544  pjinvari  32590  fmptco1f1o  33025  fcobij  33111  fcobijfs  33112  fcobijfs2  33113  mbfmco  34695  dstfrvclim1  34909  reprpmtf1o  35054  mrsubco  36026  mclsppslem  36088  circum  36179  mblfinlem2  38342  mbfresfi  38350  ftc1anclem5  38381  ghomco  38575  rngohomco  38658  tendococl  41579  mapco2g  43478  diophrw  43523  hausgraph  43965  sblpnf  45053  fcoss  45959  limccog  46369  mbfres2cn  46705  volioof  46734  volioofmpt  46741  voliooicof  46743  stoweidlem31  46778  stoweidlem59  46806  subsaliuncllem  47104  sge0resrnlem  47150  ovolval2lem  47390  ovolval2  47391  ovolval3  47394  ovolval4lem1  47396  gricushgr  48715  amgmwlem  50683