Theorem fco 6683

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ^◡ccnv 5620   “ cima 5624   ∘ ccom 5625  Fun wfun 6483  ⟶wf 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-fun 6491  df-fn 6492  df-f 6493

This theorem is referenced by:  fcod  6684  fco2  6685  mapen  9065  fsuppco2  9298  mapfienlem1  9300  unxpwdom2  9485  wemapwe  9598  cfcoflem  10174  isf34lem7  10281  isf34lem6  10282  inar1  10677  addnqf  10850  mulnqf  10851  axdc4uzlem  13897  seqf1olem2  13956  wrdco  14745  lenco  14746  lo1o1  15446  o1co  15500  caucvgrlem2  15589  fsumcl2lem  15645  fsumadd  15654  fsummulc2  15698  fsumrelem  15721  supcvg  15770  fprodcl2lem  15864  fprodmul  15874  fproddiv  15875  fprodn0  15893  algcvg  16494  cofucl  17803  setccatid  17999  estrccatid  18046  funcestrcsetclem9  18062  funcsetcestrclem9  18077  yonedalem3b  18193  mgmhmco  18630  mhmco  18739  pwsco1mhm  18748  pwsco2mhm  18749  gsumwmhm  18761  efmndcl  18798  f1omvdconj  19366  pmtrfinv  19381  symgtrinv  19392  psgnunilem1  19413  gsumval3lem1  19825  gsumval3  19827  gsumzcl2  19830  gsumzf1o  19832  gsumzaddlem  19841  gsumzmhm  19857  gsumzoppg  19864  gsumzinv  19865  gsumsub  19868  dprdf1o  19954  ablfaclem2  20008  cnfldds  21312  cnflddsOLD  21325  dsmmbas2  21683  f1lindf  21768  lindfmm  21773  psrnegcl  21901  coe1f2  22141  cpmadumatpolylem1  22816  cnco  23201  cnpco  23202  lmcnp  23239  cnmpt11  23598  cnmpt21  23606  qtopcn  23649  fmco  23896  flfcnp  23939  tsmsf1o  24080  tsmsmhm  24081  tsmssub  24084  imasdsf1olem  24308  nrmmetd  24509  isngp2  24532  isngp3  24533  tngngp2  24587  cnmet  24706  cnfldms  24710  cncfco  24847  cnfldcusp  25304  ovolfioo  25415  ovolficc  25416  ovolfsf  25419  ovollb  25427  ovolctb  25438  ovolicc2lem4  25468  ovolicc2  25470  volsup  25504  uniioovol  25527  uniioombllem3a  25532  uniioombllem3  25533  uniioombllem4  25534  uniioombllem5  25535  uniioombl  25537  mbfdm  25574  ismbfcn  25577  mbfres  25592  mbfimaopnlem  25603  cncombf  25606  limccnp  25839  dvcobrOLD  25897  dvcof  25899  dvcjbr  25900  dvcj  25901  dvmptco  25923  dvlip2  25947  itgsubstlem  26002  coecj  26231  coecjOLD  26233  pserulm  26378  jensenlem2  26945  jensen  26946  amgmlem  26947  gamf  27000  dchrinv  27219  motcgrg  28542  vsfval  30634  imsdf  30690  lnocoi  30758  hocofi  31767  homco1  31802  homco2  31978  hmopco  32024  kbass2  32118  kbass5  32121  opsqrlem1  32141  opsqrlem6  32146  pjinvari  32192  fmptco1f1o  32637  fcobij  32727  fcobijfs  32728  fcobijfs2  32729  mbfmco  34349  dstfrvclim1  34563  reprpmtf1o  34711  mrsubco  35637  mclsppslem  35699  circum  35790  mblfinlem2  37771  mbfresfi  37779  ftc1anclem5  37810  ghomco  38004  rngohomco  38087  tendococl  40944  mapco2g  42871  diophrw  42916  hausgraph  43362  sblpnf  44467  fcoss  45370  limccog  45782  mbfres2cn  46118  volioof  46147  volioofmpt  46154  voliooicof  46156  stoweidlem31  46191  stoweidlem59  46219  subsaliuncllem  46517  sge0resrnlem  46563  hoicvr  46708  ovolval2lem  46803  ovolval2  46804  ovolval3  46807  ovolval4lem1  46809  gricushgr  48079  amgmwlem  49963