Theorem fco 6730

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  ^◡ccnv 5660   “ cima 5664   ∘ ccom 5665  Fun wfun 6530  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  fcod  6731  fco2  6732  mapen  9125  fsuppco2  9359  mapfienlem1  9361  unxpwdom2  9546  wemapwe  9662  cfcoflem  10251  isf34lem7  10358  isf34lem6  10359  inar1  10755  addnqf  10928  mulnqf  10929  axdc4uzlem  14015  seqf1olem2  14074  wrdco  14864  lenco  14865  lo1o1  15579  o1co  15633  caucvgrlem2  15722  fsumcl2lem  15778  fsumadd  15787  fsummulc2  15831  fsumrelem  15855  supcvg  15906  fprodcl2lem  16000  fprodmul  16010  fproddiv  16011  fprodn0  16029  algcvg  16629  cofucl  17940  setccatid  18136  estrccatid  18183  funcestrcsetclem9  18199  funcsetcestrclem9  18214  yonedalem3b  18330  mgmhmco  18767  mhmco  18877  pwsco1mhm  18886  pwsco2mhm  18887  gsumwmhm  18899  efmndcl  18936  f1omvdconj  19511  pmtrfinv  19526  symgtrinv  19537  psgnunilem1  19558  gsumval3lem1  19970  gsumval3  19972  gsumzcl2  19975  gsumzf1o  19977  gsumzaddlem  19986  gsumzmhm  20002  gsumzoppg  20009  gsumzinv  20010  gsumsub  20013  dprdf1o  20099  ablfaclem2  20153  cnfldds  21534  dsmmbas2  21887  f1lindf  21972  lindfmm  21977  psrnegcl  22104  coe1f2  22369  cpmadumatpolylem1  23038  cnco  23423  cnpco  23424  lmcnp  23461  cnmpt11  23820  cnmpt21  23828  qtopcn  23871  fmco  24118  flfcnp  24161  tsmsf1o  24302  tsmsmhm  24303  tsmssub  24306  imasdsf1olem  24530  nrmmetd  24731  isngp2  24754  isngp3  24755  tngngp2  24809  cnmet  24928  cnfldms  24932  cncfco  25066  cnfldcusp  25516  ovolfioo  25626  ovolficc  25627  ovolfsf  25630  ovollb  25638  ovolctb  25649  ovolicc2lem4  25679  ovolicc2  25681  volsup  25715  uniioovol  25738  uniioombllem3a  25743  uniioombllem3  25744  uniioombllem4  25745  uniioombllem5  25746  uniioombl  25748  mbfdm  25785  ismbfcn  25788  mbfres  25803  mbfimaopnlem  25814  cncombf  25817  limccnp  26050  dvcof  26107  dvcjbr  26108  dvcj  26109  dvmptco  26131  dvlip2  26154  itgsubstlem  26207  coecj  26435  coecjOLD  26437  pserulm  26585  jensenlem2  27152  jensen  27153  amgmlem  27154  gamf  27207  dchrinv  27425  motcgrg  28813  vsfval  30985  imsdf  31041  lnocoi  31109  hocofi  32118  homco1  32153  homco2  32329  hmopco  32375  kbass2  32469  kbass5  32472  opsqrlem1  32492  opsqrlem6  32497  pjinvari  32543  fmptco1f1o  32978  fcobij  33065  fcobijfs  33066  fcobijfs2  33067  mbfmco  34654  dstfrvclim1  34868  reprpmtf1o  35013  mrsubco  36013  mclsppslem  36075  circum  36166  mblfinlem2  38309  mbfresfi  38317  ftc1anclem5  38348  ghomco  38542  rngohomco  38625  tendococl  41546  mapco2g  43445  diophrw  43490  hausgraph  43932  sblpnf  45020  fcoss  45926  limccog  46336  mbfres2cn  46672  volioof  46701  volioofmpt  46708  voliooicof  46710  stoweidlem31  46745  stoweidlem59  46773  subsaliuncllem  47071  sge0resrnlem  47117  ovolval2lem  47357  ovolval2  47358  ovolval3  47361  ovolval4lem1  47363  gricushgr  48682  amgmwlem  50622