Theorem fco 6728

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  ^◡ccnv 5658   “ cima 5662   ∘ ccom 5663  Fun wfun 6527  ⟶wf 6529

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 5258  ax-pr 5402

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 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5175  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6535  df-fn 6536  df-f 6537

This theorem is referenced by:  fcod  6729  fco2  6730  mapen  9125  fsuppco2  9359  mapfienlem1  9361  unxpwdom2  9546  wemapwe  9662  cfcoflem  10252  isf34lem7  10359  isf34lem6  10360  inar1  10756  addnqf  10929  mulnqf  10930  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  16630  cofucl  17941  setccatid  18137  estrccatid  18184  funcestrcsetclem9  18200  funcsetcestrclem9  18215  yonedalem3b  18331  mgmhmco  18768  mhmco  18878  pwsco1mhm  18887  pwsco2mhm  18888  gsumwmhm  18900  efmndcl  18937  f1omvdconj  19512  pmtrfinv  19527  symgtrinv  19538  psgnunilem1  19559  gsumval3lem1  19971  gsumval3  19973  gsumzcl2  19976  gsumzf1o  19978  gsumzaddlem  19987  gsumzmhm  20003  gsumzoppg  20010  gsumzinv  20011  gsumsub  20014  dprdf1o  20100  ablfaclem2  20154  cnfldds  21499  dsmmbas2  21852  f1lindf  21937  lindfmm  21942  psrnegcl  22069  coe1f2  22334  cpmadumatpolylem1  23003  cnco  23388  cnpco  23389  lmcnp  23426  cnmpt11  23785  cnmpt21  23793  qtopcn  23836  fmco  24083  flfcnp  24126  tsmsf1o  24267  tsmsmhm  24268  tsmssub  24271  imasdsf1olem  24495  nrmmetd  24696  isngp2  24719  isngp3  24720  tngngp2  24774  cnmet  24893  cnfldms  24897  cncfco  25031  cnfldcusp  25481  ovolfioo  25591  ovolficc  25592  ovolfsf  25595  ovollb  25603  ovolctb  25614  ovolicc2lem4  25644  ovolicc2  25646  volsup  25680  uniioovol  25703  uniioombllem3a  25708  uniioombllem3  25709  uniioombllem4  25710  uniioombllem5  25711  uniioombl  25713  mbfdm  25750  ismbfcn  25753  mbfres  25768  mbfimaopnlem  25779  cncombf  25782  limccnp  26015  dvcof  26072  dvcjbr  26073  dvcj  26074  dvmptco  26096  dvlip2  26119  itgsubstlem  26172  coecj  26400  coecjOLD  26402  pserulm  26547  jensenlem2  27114  jensen  27115  amgmlem  27116  gamf  27169  dchrinv  27387  motcgrg  28775  vsfval  30922  imsdf  30978  lnocoi  31046  hocofi  32055  homco1  32090  homco2  32266  hmopco  32312  kbass2  32406  kbass5  32409  opsqrlem1  32429  opsqrlem6  32434  pjinvari  32480  fmptco1f1o  32915  fcobij  33002  fcobijfs  33003  fcobijfs2  33004  mbfmco  34595  dstfrvclim1  34809  reprpmtf1o  34954  mrsubco  35908  mclsppslem  35970  circum  36061  mblfinlem2  38192  mbfresfi  38200  ftc1anclem5  38231  ghomco  38425  rngohomco  38508  tendococl  41431  mapco2g  43330  diophrw  43375  hausgraph  43817  sblpnf  44905  fcoss  45811  limccog  46221  mbfres2cn  46557  volioof  46586  volioofmpt  46593  voliooicof  46595  stoweidlem31  46630  stoweidlem59  46658  subsaliuncllem  46956  sge0resrnlem  47002  ovolval2lem  47242  ovolval2  47243  ovolval3  47246  ovolval4lem1  47248  gricushgr  48564  amgmwlem  50458