Theorem fco 6732

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ^◡ccnv 5650   “ cima 5654   ∘ ccom 5655  Fun wfun 6531  ⟶wf 6533

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  fcod  6733  fco2  6734  mapen  9153  fsuppco2  9388  mapfienlem1  9390  unxpwdom2  9575  wemapwe  9691  cfcoflem  10343  isf34lem7  10450  isf34lem6  10451  inar1  10853  addnqf  11026  mulnqf  11027  axdc4uzlem  14119  seqf1olem2  14178  wrdco  14975  lenco  14976  lo1o1  15692  o1co  15746  caucvgrlem2  15835  fsumcl2lem  15890  fsumadd  15899  fsummulc2  15943  fsumrelem  15967  supcvg  16018  fprodcl2lem  16110  fprodmul  16120  fproddiv  16121  fprodn0  16139  algcvg  16744  cofucl  18056  setccatid  18252  estrccatid  18299  funcestrcsetclem9  18315  funcsetcestrclem9  18330  yonedalem3b  18446  mgmhmco  18896  mhmco  19012  pwsco1mhm  19021  pwsco2mhm  19022  gsumwmhm  19034  efmndcl  19071  f1omvdconj  19653  pmtrfinv  19668  symgtrinv  19679  psgnunilem1  19700  gsumval3lem1  20112  gsumval3  20114  gsumzcl2  20117  gsumzf1o  20119  gsumzaddlem  20128  gsumzmhm  20144  gsumzoppg  20151  gsumzinv  20152  gsumsub  20155  dprdf1o  20241  ablfaclem2  20295  cnfldds  21683  dsmmbas2  22036  f1lindf  22121  lindfmm  22126  psrnegcl  22255  coe1f2  22520  cpmadumatpolylem1  23192  cnco  23577  cnpco  23578  lmcnp  23615  cnmpt11  23975  cnmpt21  23983  qtopcn  24026  fmco  24273  flfcnp  24316  tsmsf1o  24457  tsmsmhm  24458  tsmssub  24461  imasdsf1olem  24685  nrmmetd  24886  isngp2  24909  isngp3  24910  tngngp2  24964  cnmet  25083  cnfldms  25087  cncfco  25221  cnfldcusp  25671  ovolfioo  25781  ovolficc  25782  ovolfsf  25785  ovollb  25793  ovolctb  25804  ovolicc2lem4  25834  ovolicc2  25836  volsup  25870  uniioovol  25893  uniioombllem3a  25898  uniioombllem3  25899  uniioombllem4  25900  uniioombllem5  25901  uniioombl  25903  mbfdm  25940  ismbfcn  25943  mbfres  25958  mbfimaopnlem  25969  cncombf  25972  limccnp  26204  dvcof  26261  dvcjbr  26262  dvcj  26263  dvmptco  26285  dvlip2  26308  itgsubstlem  26361  coecj  26590  pserulm  26742  jensenlem2  27308  jensen  27309  amgmlem  27310  gamf  27363  dchrinv  27581  motcgrg  29000  vsfval  31228  imsdf  31284  lnocoi  31352  hocofi  32361  homco1  32396  homco2  32572  hmopco  32618  kbass2  32712  kbass5  32715  opsqrlem1  32735  opsqrlem6  32740  pjinvari  32786  fmptco1f1o  33220  fcobij  33305  fcobijfs  33306  fcobijfs2  33307  mbfmco  34889  dstfrvclim1  35103  reprpmtf1o  35248  mrsubco  36265  mclsppslem  36327  circum  36418  mblfinlem2  38556  mbfresfi  38564  ftc1anclem5  38595  ghomco  38805  rngohomco  38888  tendococl  41809  mapco2g  43704  diophrw  43749  hausgraph  44191  sblpnf  45279  fcoss  46192  limccog  46601  mbfres2cn  46937  volioof  46966  volioofmpt  46973  voliooicof  46975  stoweidlem31  47010  stoweidlem59  47038  subsaliuncllem  47336  sge0resrnlem  47382  ovolval2lem  47622  ovolval2  47623  ovolval3  47626  ovolval4lem1  47628  gricushgr  48984  amgmwlem  50956