Theorem fco 6727

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ^◡ccnv 5654   “ cima 5658   ∘ ccom 5659  Fun wfun 6527  ⟶wf 6529

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 2732  ax-sep 5251  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6535  df-fn 6536  df-f 6537

This theorem is used by:  fcod  6728  fco2  6729  mapen  9139  fsuppco2  9373  mapfienlem1  9375  unxpwdom2  9560  wemapwe  9676  cfcoflem  10274  isf34lem7  10381  isf34lem6  10382  inar1  10784  addnqf  10957  mulnqf  10958  axdc4uzlem  14047  seqf1olem2  14106  wrdco  14902  lenco  14903  lo1o1  15619  o1co  15673  caucvgrlem2  15762  fsumcl2lem  15817  fsumadd  15826  fsummulc2  15870  fsumrelem  15894  supcvg  15945  fprodcl2lem  16037  fprodmul  16047  fproddiv  16048  fprodn0  16066  algcvg  16666  cofucl  17977  setccatid  18173  estrccatid  18220  funcestrcsetclem9  18236  funcsetcestrclem9  18251  yonedalem3b  18367  mgmhmco  18816  mhmco  18932  pwsco1mhm  18941  pwsco2mhm  18942  gsumwmhm  18954  efmndcl  18991  f1omvdconj  19573  pmtrfinv  19588  symgtrinv  19599  psgnunilem1  19620  gsumval3lem1  20032  gsumval3  20034  gsumzcl2  20037  gsumzf1o  20039  gsumzaddlem  20048  gsumzmhm  20064  gsumzoppg  20071  gsumzinv  20072  gsumsub  20075  dprdf1o  20161  ablfaclem2  20215  cnfldds  21597  dsmmbas2  21950  f1lindf  22035  lindfmm  22040  psrnegcl  22169  coe1f2  22434  cpmadumatpolylem1  23106  cnco  23491  cnpco  23492  lmcnp  23529  cnmpt11  23889  cnmpt21  23897  qtopcn  23940  fmco  24187  flfcnp  24230  tsmsf1o  24371  tsmsmhm  24372  tsmssub  24375  imasdsf1olem  24599  nrmmetd  24800  isngp2  24823  isngp3  24824  tngngp2  24878  cnmet  24997  cnfldms  25001  cncfco  25135  cnfldcusp  25585  ovolfioo  25695  ovolficc  25696  ovolfsf  25699  ovollb  25707  ovolctb  25718  ovolicc2lem4  25748  ovolicc2  25750  volsup  25784  uniioovol  25807  uniioombllem3a  25812  uniioombllem3  25813  uniioombllem4  25814  uniioombllem5  25815  uniioombl  25817  mbfdm  25854  ismbfcn  25857  mbfres  25872  mbfimaopnlem  25883  cncombf  25886  limccnp  26118  dvcof  26175  dvcjbr  26176  dvcj  26177  dvmptco  26199  dvlip2  26222  itgsubstlem  26275  coecj  26504  coecjOLD  26506  pserulm  26658  jensenlem2  27224  jensen  27225  amgmlem  27226  gamf  27279  dchrinv  27497  motcgrg  28886  vsfval  31114  imsdf  31170  lnocoi  31238  hocofi  32247  homco1  32282  homco2  32458  hmopco  32504  kbass2  32598  kbass5  32601  opsqrlem1  32621  opsqrlem6  32626  pjinvari  32672  fmptco1f1o  33106  fcobij  33191  fcobijfs  33192  fcobijfs2  33193  mbfmco  34775  dstfrvclim1  34989  reprpmtf1o  35134  mrsubco  36100  mclsppslem  36162  circum  36253  mblfinlem2  38407  mbfresfi  38415  ftc1anclem5  38446  ghomco  38641  rngohomco  38724  tendococl  41645  mapco2g  43559  diophrw  43604  hausgraph  44046  sblpnf  45134  fcoss  46040  limccog  46450  mbfres2cn  46786  volioof  46815  volioofmpt  46822  voliooicof  46824  stoweidlem31  46859  stoweidlem59  46887  subsaliuncllem  47185  sge0resrnlem  47231  ovolval2lem  47471  ovolval2  47472  ovolval3  47475  ovolval4lem1  47477  gricushgr  48833  amgmwlem  50820