Theorem fco 6729

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ^◡ccnv 5653   “ cima 5657   ∘ ccom 5658  Fun wfun 6524  ⟶wf 6526

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-fun 6532  df-fn 6533  df-f 6534

This theorem is referenced by:  fcod  6730  fco2  6731  mapen  9153  fsuppco2  9413  mapfienlem1  9415  unxpwdom2  9600  wemapwe  9709  cfcoflem  10284  isf34lem7  10391  isf34lem6  10392  inar1  10787  addnqf  10960  mulnqf  10961  axdc4uzlem  13999  seqf1olem2  14058  wrdco  14848  lenco  14849  lo1o1  15546  o1co  15600  caucvgrlem2  15689  fsumcl2lem  15745  fsumadd  15754  fsummulc2  15798  fsumrelem  15821  supcvg  15870  fprodcl2lem  15964  fprodmul  15974  fproddiv  15975  fprodn0  15993  algcvg  16593  cofucl  17899  setccatid  18095  estrccatid  18142  funcestrcsetclem9  18158  funcsetcestrclem9  18173  yonedalem3b  18289  mgmhmco  18690  mhmco  18799  pwsco1mhm  18808  pwsco2mhm  18809  gsumwmhm  18821  efmndcl  18858  f1omvdconj  19425  pmtrfinv  19440  symgtrinv  19451  psgnunilem1  19472  gsumval3lem1  19884  gsumval3  19886  gsumzcl2  19889  gsumzf1o  19891  gsumzaddlem  19900  gsumzmhm  19916  gsumzoppg  19923  gsumzinv  19924  gsumsub  19927  dprdf1o  20013  ablfaclem2  20067  cnfldds  21325  cnflddsOLD  21338  dsmmbas2  21695  f1lindf  21780  lindfmm  21785  psrnegcl  21912  coe1f2  22143  cpmadumatpolylem1  22817  cnco  23202  cnpco  23203  lmcnp  23240  cnmpt11  23599  cnmpt21  23607  qtopcn  23650  fmco  23897  flfcnp  23940  tsmsf1o  24081  tsmsmhm  24082  tsmssub  24085  imasdsf1olem  24310  nrmmetd  24511  isngp2  24534  isngp3  24535  tngngp2  24589  cnmet  24708  cnfldms  24712  cncfco  24849  cnfldcusp  25307  ovolfioo  25418  ovolficc  25419  ovolfsf  25422  ovollb  25430  ovolctb  25441  ovolicc2lem4  25471  ovolicc2  25473  volsup  25507  uniioovol  25530  uniioombllem3a  25535  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  uniioombl  25540  mbfdm  25577  ismbfcn  25580  mbfres  25595  mbfimaopnlem  25606  cncombf  25609  limccnp  25842  dvcobrOLD  25900  dvcof  25902  dvcjbr  25903  dvcj  25904  dvmptco  25926  dvlip2  25950  itgsubstlem  26005  coecj  26234  coecjOLD  26236  pserulm  26381  jensenlem2  26948  jensen  26949  amgmlem  26950  gamf  27003  dchrinv  27222  motcgrg  28469  vsfval  30560  imsdf  30616  lnocoi  30684  hocofi  31693  homco1  31728  homco2  31904  hmopco  31950  kbass2  32044  kbass5  32047  opsqrlem1  32067  opsqrlem6  32072  pjinvari  32118  fmptco1f1o  32557  fcobij  32645  fcobijfs  32646  mbfmco  34242  dstfrvclim1  34456  reprpmtf1o  34604  mrsubco  35489  mclsppslem  35551  circum  35642  mblfinlem2  37628  mbfresfi  37636  ftc1anclem5  37667  ghomco  37861  rngohomco  37944  tendococl  40737  mapco2g  42684  diophrw  42729  hausgraph  43176  sblpnf  44282  fcoss  45182  limccog  45597  mbfres2cn  45935  volioof  45964  volioofmpt  45971  voliooicof  45973  stoweidlem31  46008  stoweidlem59  46036  subsaliuncllem  46334  sge0resrnlem  46380  hoicvr  46525  ovolval2lem  46620  ovolval2  46621  ovolval3  46624  ovolval4lem1  46626  gricushgr  47878  amgmwlem  49561