Theorem fco 6712

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 6691	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6711	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 593	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6710	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2735	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 481	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6672	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 257	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ^◡ccnv 5637   “ cima 5641   ∘ ccom 5642  Fun wfun 6505  ⟶wf 6507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  fcod  6713  fco2  6714  mapen  9105  fsuppco2  9354  mapfienlem1  9356  unxpwdom2  9541  wemapwe  9650  cfcoflem  10225  isf34lem7  10332  isf34lem6  10333  inar1  10728  addnqf  10901  mulnqf  10902  axdc4uzlem  13948  seqf1olem2  14007  wrdco  14797  lenco  14798  lo1o1  15498  o1co  15552  caucvgrlem2  15641  fsumcl2lem  15697  fsumadd  15706  fsummulc2  15750  fsumrelem  15773  supcvg  15822  fprodcl2lem  15916  fprodmul  15926  fproddiv  15927  fprodn0  15945  algcvg  16546  cofucl  17850  setccatid  18046  estrccatid  18093  funcestrcsetclem9  18109  funcsetcestrclem9  18124  yonedalem3b  18240  mgmhmco  18641  mhmco  18750  pwsco1mhm  18759  pwsco2mhm  18760  gsumwmhm  18772  efmndcl  18809  f1omvdconj  19376  pmtrfinv  19391  symgtrinv  19402  psgnunilem1  19423  gsumval3lem1  19835  gsumval3  19837  gsumzcl2  19840  gsumzf1o  19842  gsumzaddlem  19851  gsumzmhm  19867  gsumzoppg  19874  gsumzinv  19875  gsumsub  19878  dprdf1o  19964  ablfaclem2  20018  cnfldds  21276  cnflddsOLD  21289  dsmmbas2  21646  f1lindf  21731  lindfmm  21736  psrnegcl  21863  coe1f2  22094  cpmadumatpolylem1  22768  cnco  23153  cnpco  23154  lmcnp  23191  cnmpt11  23550  cnmpt21  23558  qtopcn  23601  fmco  23848  flfcnp  23891  tsmsf1o  24032  tsmsmhm  24033  tsmssub  24036  imasdsf1olem  24261  nrmmetd  24462  isngp2  24485  isngp3  24486  tngngp2  24540  cnmet  24659  cnfldms  24663  cncfco  24800  cnfldcusp  25257  ovolfioo  25368  ovolficc  25369  ovolfsf  25372  ovollb  25380  ovolctb  25391  ovolicc2lem4  25421  ovolicc2  25423  volsup  25457  uniioovol  25480  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombl  25490  mbfdm  25527  ismbfcn  25530  mbfres  25545  mbfimaopnlem  25556  cncombf  25559  limccnp  25792  dvcobrOLD  25850  dvcof  25852  dvcjbr  25853  dvcj  25854  dvmptco  25876  dvlip2  25900  itgsubstlem  25955  coecj  26184  coecjOLD  26186  pserulm  26331  jensenlem2  26898  jensen  26899  amgmlem  26900  gamf  26953  dchrinv  27172  motcgrg  28471  vsfval  30562  imsdf  30618  lnocoi  30686  hocofi  31695  homco1  31730  homco2  31906  hmopco  31952  kbass2  32046  kbass5  32049  opsqrlem1  32069  opsqrlem6  32074  pjinvari  32120  fmptco1f1o  32557  fcobij  32645  fcobijfs  32646  mbfmco  34255  dstfrvclim1  34469  reprpmtf1o  34617  mrsubco  35508  mclsppslem  35570  circum  35661  mblfinlem2  37652  mbfresfi  37660  ftc1anclem5  37691  ghomco  37885  rngohomco  37968  tendococl  40766  mapco2g  42702  diophrw  42747  hausgraph  43194  sblpnf  44299  fcoss  45204  limccog  45618  mbfres2cn  45956  volioof  45985  volioofmpt  45992  voliooicof  45994  stoweidlem31  46029  stoweidlem59  46057  subsaliuncllem  46355  sge0resrnlem  46401  hoicvr  46546  ovolval2lem  46641  ovolval2  46642  ovolval3  46645  ovolval4lem1  46647  gricushgr  47917  amgmwlem  49791