Theorem fco 6741

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 6720	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6740	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 592	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6739	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2737	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 481	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6703	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 257	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ^◡ccnv 5675   “ cima 5679   ∘ ccom 5680  Fun wfun 6537  ⟶wf 6539

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-fun 6545  df-fn 6546  df-f 6547

This theorem is referenced by:  fcod  6743  fco2  6744  f1coOLD  6800  mapen  9147  fsuppco2  9404  mapfienlem1  9406  unxpwdom2  9589  wemapwe  9698  cfcoflem  10273  isf34lem7  10380  isf34lem6  10381  inar1  10776  addnqf  10949  mulnqf  10950  axdc4uzlem  13955  seqf1olem2  14015  wrdco  14789  lenco  14790  lo1o1  15483  o1co  15537  caucvgrlem2  15628  fsumcl2lem  15684  fsumadd  15693  fsummulc2  15737  fsumrelem  15760  supcvg  15809  fprodcl2lem  15901  fprodmul  15911  fproddiv  15912  fprodn0  15930  algcvg  16520  cofucl  17845  setccatid  18044  estrccatid  18093  funcestrcsetclem9  18110  funcsetcestrclem9  18125  yonedalem3b  18242  mgmhmco  18645  mhmco  18746  pwsco1mhm  18755  pwsco2mhm  18756  gsumwmhm  18768  efmndcl  18805  f1omvdconj  19362  pmtrfinv  19377  symgtrinv  19388  psgnunilem1  19409  gsumval3lem1  19821  gsumval3  19823  gsumzcl2  19826  gsumzf1o  19828  gsumzaddlem  19837  gsumzmhm  19853  gsumzoppg  19860  gsumzinv  19861  gsumsub  19864  dprdf1o  19950  ablfaclem2  20004  cnfldds  21242  dsmmbas2  21601  f1lindf  21686  lindfmm  21691  psrass1lemOLD  21802  psrnegcl  21825  coe1f2  22051  cpmadumatpolylem1  22702  cnco  23089  cnpco  23090  lmcnp  23127  cnmpt11  23486  cnmpt21  23494  qtopcn  23537  fmco  23784  flfcnp  23827  tsmsf1o  23968  tsmsmhm  23969  tsmssub  23972  imasdsf1olem  24198  nrmmetd  24402  isngp2  24425  isngp3  24426  tngngp2  24488  cnmet  24607  cnfldms  24611  cncfco  24746  cnfldcusp  25204  ovolfioo  25315  ovolficc  25316  ovolfsf  25319  ovollb  25327  ovolctb  25338  ovolicc2lem4  25368  ovolicc2  25370  volsup  25404  uniioovol  25427  uniioombllem3a  25432  uniioombllem3  25433  uniioombllem4  25434  uniioombllem5  25435  uniioombl  25437  mbfdm  25474  ismbfcn  25477  mbfres  25492  mbfimaopnlem  25503  cncombf  25506  limccnp  25739  dvcobrOLD  25797  dvcof  25799  dvcjbr  25800  dvcj  25801  dvmptco  25823  dvlip2  25847  itgsubstlem  25902  coecj  26130  pserulm  26272  jensenlem2  26832  jensen  26833  amgmlem  26834  gamf  26887  dchrinv  27106  motcgrg  28227  vsfval  30318  imsdf  30374  lnocoi  30442  hocofi  31451  homco1  31486  homco2  31662  hmopco  31708  kbass2  31802  kbass5  31805  opsqrlem1  31825  opsqrlem6  31830  pjinvari  31876  fmptco1f1o  32289  fcobij  32379  fcobijfs  32380  mbfmco  33726  dstfrvclim1  33939  reprpmtf1o  34101  mrsubco  34975  mclsppslem  35037  circum  35122  gg-cnfldds  35641  mblfinlem2  36989  mbfresfi  36997  ftc1anclem5  37028  ghomco  37222  rngohomco  37305  tendococl  40106  mapco2g  41914  diophrw  41959  hausgraph  42416  sblpnf  43531  fcoss  44367  limccog  44794  mbfres2cn  45132  volioof  45161  volioofmpt  45168  voliooicof  45170  stoweidlem31  45205  stoweidlem59  45233  subsaliuncllem  45531  sge0resrnlem  45577  hoicvr  45722  ovolval2lem  45817  ovolval2  45818  ovolval3  45821  ovolval4lem1  45823  isomushgr  46952  amgmwlem  48010