Theorem fco 6620

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 6599	. . 3 ⊢ (𝐺:𝐴⟶𝐵 → Fun 𝐺)
2		fcof 6619	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ Fun 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
3	1, 2	sylan2 592	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶)
4		fimacnv 6618	. . . . 5 ⊢ (𝐺:𝐴⟶𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
5	4	eqcomd 2745	. . . 4 ⊢ (𝐺:𝐴⟶𝐵 → 𝐴 = (◡𝐺 “ 𝐵))
6	5	adantl 481	. . 3 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → 𝐴 = (◡𝐺 “ 𝐵))
7	6	feq2d 6582	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐵)⟶𝐶))
8	3, 7	mpbird 256	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ^◡ccnv 5587   “ cima 5591   ∘ ccom 5592  Fun wfun 6424  ⟶wf 6426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-fun 6432  df-fn 6433  df-f 6434

This theorem is referenced by:  fcod  6622  fco2  6623  f1coOLD  6679  mapen  8893  fsuppco2  9123  mapfienlem1  9125  unxpwdom2  9308  wemapwe  9416  cfcoflem  10012  isf34lem7  10119  isf34lem6  10120  inar1  10515  addnqf  10688  mulnqf  10689  axdc4uzlem  13684  seqf1olem2  13744  wrdco  14525  lenco  14526  lo1o1  15222  o1co  15276  caucvgrlem2  15367  fsumcl2lem  15424  fsumadd  15433  fsummulc2  15477  fsumrelem  15500  supcvg  15549  fprodcl2lem  15641  fprodmul  15651  fproddiv  15652  fprodn0  15670  algcvg  16262  cofucl  17584  setccatid  17780  estrccatid  17829  funcestrcsetclem9  17846  funcsetcestrclem9  17861  yonedalem3b  17978  mhmco  18443  pwsco1mhm  18451  pwsco2mhm  18452  gsumwmhm  18465  efmndcl  18502  f1omvdconj  19035  pmtrfinv  19050  symgtrinv  19061  psgnunilem1  19082  gsumval3lem1  19487  gsumval3  19489  gsumzcl2  19492  gsumzf1o  19494  gsumzaddlem  19503  gsumzmhm  19519  gsumzoppg  19526  gsumzinv  19527  gsumsub  19530  dprdf1o  19616  ablfaclem2  19670  cnfldds  20588  dsmmbas2  20925  f1lindf  21010  lindfmm  21015  psrass1lemOLD  21124  psrnegcl  21146  coe1f2  21361  cpmadumatpolylem1  22011  cnco  22398  cnpco  22399  lmcnp  22436  cnmpt11  22795  cnmpt21  22803  qtopcn  22846  fmco  23093  flfcnp  23136  tsmsf1o  23277  tsmsmhm  23278  tsmssub  23281  imasdsf1olem  23507  nrmmetd  23711  isngp2  23734  isngp3  23735  tngngp2  23797  cnmet  23916  cnfldms  23920  cncfco  24051  cnfldcusp  24502  ovolfioo  24612  ovolficc  24613  ovolfsf  24616  ovollb  24624  ovolctb  24635  ovolicc2lem4  24665  ovolicc2  24667  volsup  24701  uniioovol  24724  uniioombllem3a  24729  uniioombllem3  24730  uniioombllem4  24731  uniioombllem5  24732  uniioombl  24734  mbfdm  24771  ismbfcn  24774  mbfres  24789  mbfimaopnlem  24800  cncombf  24803  limccnp  25036  dvcobr  25091  dvcof  25093  dvcjbr  25094  dvcj  25095  dvmptco  25117  dvlip2  25140  itgsubstlem  25193  coecj  25420  pserulm  25562  jensenlem2  26118  jensen  26119  amgmlem  26120  gamf  26173  dchrinv  26390  motcgrg  26886  vsfval  28974  imsdf  29030  lnocoi  29098  hocofi  30107  homco1  30142  homco2  30318  hmopco  30364  kbass2  30458  kbass5  30461  opsqrlem1  30481  opsqrlem6  30486  pjinvari  30532  fmptco1f1o  30947  fcobij  31036  fcobijfs  31037  mbfmco  32210  dstfrvclim1  32423  reprpmtf1o  32585  mrsubco  33462  mclsppslem  33524  circum  33611  mblfinlem2  35794  mbfresfi  35802  ftc1anclem5  35833  ghomco  36028  rngohomco  36111  tendococl  38765  mapco2g  40516  diophrw  40561  hausgraph  41017  sblpnf  41881  fcoss  42703  limccog  43115  mbfres2cn  43453  volioof  43482  volioofmpt  43489  voliooicof  43491  stoweidlem31  43526  stoweidlem59  43554  subsaliuncllem  43850  sge0resrnlem  43895  hoicvr  44040  ovolval2lem  44135  ovolval2  44136  ovolval3  44139  ovolval4lem1  44141  ovolval5lem3  44146  isomushgr  45230  mgmhmco  45307  amgmwlem  46458