Theorem fco 6731

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 6709	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6730	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 604	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6729	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2775	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 486	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6690	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 260	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  ^◡ccnv 5661   “ cima 5665   ∘ ccom 5666  Fun wfun 6531  ⟶wf 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-fun 6539  df-fn 6540  df-f 6541

This theorem is referenced by:  fcod  6732  fco2  6733  mapen  9128  fsuppco2  9362  mapfienlem1  9364  unxpwdom2  9549  wemapwe  9665  cfcoflem  10255  isf34lem7  10362  isf34lem6  10363  inar1  10759  addnqf  10932  mulnqf  10933  axdc4uzlem  14018  seqf1olem2  14077  wrdco  14867  lenco  14868  lo1o1  15582  o1co  15636  caucvgrlem2  15725  fsumcl2lem  15781  fsumadd  15790  fsummulc2  15834  fsumrelem  15858  supcvg  15909  fprodcl2lem  16003  fprodmul  16013  fproddiv  16014  fprodn0  16032  algcvg  16633  cofucl  17944  setccatid  18140  estrccatid  18187  funcestrcsetclem9  18203  funcsetcestrclem9  18218  yonedalem3b  18334  mgmhmco  18771  mhmco  18881  pwsco1mhm  18890  pwsco2mhm  18891  gsumwmhm  18903  efmndcl  18940  f1omvdconj  19515  pmtrfinv  19530  symgtrinv  19541  psgnunilem1  19562  gsumval3lem1  19974  gsumval3  19976  gsumzcl2  19979  gsumzf1o  19981  gsumzaddlem  19990  gsumzmhm  20006  gsumzoppg  20013  gsumzinv  20014  gsumsub  20017  dprdf1o  20103  ablfaclem2  20157  cnfldds  21502  dsmmbas2  21855  f1lindf  21940  lindfmm  21945  psrnegcl  22072  coe1f2  22337  cpmadumatpolylem1  23006  cnco  23391  cnpco  23392  lmcnp  23429  cnmpt11  23788  cnmpt21  23796  qtopcn  23839  fmco  24086  flfcnp  24129  tsmsf1o  24270  tsmsmhm  24271  tsmssub  24274  imasdsf1olem  24498  nrmmetd  24699  isngp2  24722  isngp3  24723  tngngp2  24777  cnmet  24896  cnfldms  24900  cncfco  25034  cnfldcusp  25484  ovolfioo  25594  ovolficc  25595  ovolfsf  25598  ovollb  25606  ovolctb  25617  ovolicc2lem4  25647  ovolicc2  25649  volsup  25683  uniioovol  25706  uniioombllem3a  25711  uniioombllem3  25712  uniioombllem4  25713  uniioombllem5  25714  uniioombl  25716  mbfdm  25753  ismbfcn  25756  mbfres  25771  mbfimaopnlem  25782  cncombf  25785  limccnp  26018  dvcof  26075  dvcjbr  26076  dvcj  26077  dvmptco  26099  dvlip2  26122  itgsubstlem  26175  coecj  26403  coecjOLD  26405  pserulm  26550  jensenlem2  27117  jensen  27118  amgmlem  27119  gamf  27172  dchrinv  27390  motcgrg  28778  vsfval  30925  imsdf  30981  lnocoi  31049  hocofi  32058  homco1  32093  homco2  32269  hmopco  32315  kbass2  32409  kbass5  32412  opsqrlem1  32432  opsqrlem6  32437  pjinvari  32483  fmptco1f1o  32918  fcobij  33005  fcobijfs  33006  fcobijfs2  33007  mbfmco  34598  dstfrvclim1  34812  reprpmtf1o  34957  mrsubco  35911  mclsppslem  35973  circum  36064  mblfinlem2  38196  mbfresfi  38204  ftc1anclem5  38235  ghomco  38429  rngohomco  38512  tendococl  41435  mapco2g  43336  diophrw  43381  hausgraph  43823  sblpnf  44911  fcoss  45817  limccog  46227  mbfres2cn  46563  volioof  46592  volioofmpt  46599  voliooicof  46601  stoweidlem31  46636  stoweidlem59  46664  subsaliuncllem  46962  sge0resrnlem  47008  ovolval2lem  47248  ovolval2  47249  ovolval3  47252  ovolval4lem1  47254  gricushgr  48570  amgmwlem  50475