Theorem fco 6686

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 6665	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6685	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 594	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6684	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2743	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 481	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6646	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 257	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ^◡ccnv 5623   “ cima 5627   ∘ ccom 5628  Fun wfun 6486  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fcod  6687  fco2  6688  mapen  9072  fsuppco2  9309  mapfienlem1  9311  unxpwdom2  9496  wemapwe  9609  cfcoflem  10185  isf34lem7  10292  isf34lem6  10293  inar1  10689  addnqf  10862  mulnqf  10863  axdc4uzlem  13936  seqf1olem2  13995  wrdco  14784  lenco  14785  lo1o1  15485  o1co  15539  caucvgrlem2  15628  fsumcl2lem  15684  fsumadd  15693  fsummulc2  15737  fsumrelem  15761  supcvg  15812  fprodcl2lem  15906  fprodmul  15916  fproddiv  15917  fprodn0  15935  algcvg  16536  cofucl  17846  setccatid  18042  estrccatid  18089  funcestrcsetclem9  18105  funcsetcestrclem9  18120  yonedalem3b  18236  mgmhmco  18673  mhmco  18782  pwsco1mhm  18791  pwsco2mhm  18792  gsumwmhm  18804  efmndcl  18841  f1omvdconj  19412  pmtrfinv  19427  symgtrinv  19438  psgnunilem1  19459  gsumval3lem1  19871  gsumval3  19873  gsumzcl2  19876  gsumzf1o  19878  gsumzaddlem  19887  gsumzmhm  19903  gsumzoppg  19910  gsumzinv  19911  gsumsub  19914  dprdf1o  20000  ablfaclem2  20054  cnfldds  21356  cnflddsOLD  21369  dsmmbas2  21727  f1lindf  21812  lindfmm  21817  psrnegcl  21943  coe1f2  22183  cpmadumatpolylem1  22856  cnco  23241  cnpco  23242  lmcnp  23279  cnmpt11  23638  cnmpt21  23646  qtopcn  23689  fmco  23936  flfcnp  23979  tsmsf1o  24120  tsmsmhm  24121  tsmssub  24124  imasdsf1olem  24348  nrmmetd  24549  isngp2  24572  isngp3  24573  tngngp2  24627  cnmet  24746  cnfldms  24750  cncfco  24884  cnfldcusp  25334  ovolfioo  25444  ovolficc  25445  ovolfsf  25448  ovollb  25456  ovolctb  25467  ovolicc2lem4  25497  ovolicc2  25499  volsup  25533  uniioovol  25556  uniioombllem3a  25561  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  uniioombl  25566  mbfdm  25603  ismbfcn  25606  mbfres  25621  mbfimaopnlem  25632  cncombf  25635  limccnp  25868  dvcof  25925  dvcjbr  25926  dvcj  25927  dvmptco  25949  dvlip2  25972  itgsubstlem  26025  coecj  26253  coecjOLD  26255  pserulm  26400  jensenlem2  26965  jensen  26966  amgmlem  26967  gamf  27020  dchrinv  27238  motcgrg  28626  vsfval  30719  imsdf  30775  lnocoi  30843  hocofi  31852  homco1  31887  homco2  32063  hmopco  32109  kbass2  32203  kbass5  32206  opsqrlem1  32226  opsqrlem6  32231  pjinvari  32277  fmptco1f1o  32721  fcobij  32808  fcobijfs  32809  fcobijfs2  32810  mbfmco  34424  dstfrvclim1  34638  reprpmtf1o  34786  mrsubco  35719  mclsppslem  35781  circum  35872  mblfinlem2  37993  mbfresfi  38001  ftc1anclem5  38032  ghomco  38226  rngohomco  38309  tendococl  41232  mapco2g  43160  diophrw  43205  hausgraph  43651  sblpnf  44755  fcoss  45657  limccog  46068  mbfres2cn  46404  volioof  46433  volioofmpt  46440  voliooicof  46442  stoweidlem31  46477  stoweidlem59  46505  subsaliuncllem  46803  sge0resrnlem  46849  ovolval2lem  47089  ovolval2  47090  ovolval3  47093  ovolval4lem1  47095  gricushgr  48405  amgmwlem  50289