# Metamath Proof Explorer

## Theorem comfffn

Description: The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfffn.o ${⊢}{O}={\mathrm{comp}}_{𝑓}\left({C}\right)$
comfffn.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
Assertion comfffn ${⊢}{O}Fn\left(\left({B}×{B}\right)×{B}\right)$

### Proof

Step Hyp Ref Expression
1 comfffn.o ${⊢}{O}={\mathrm{comp}}_{𝑓}\left({C}\right)$
2 comfffn.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
4 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
5 1 2 3 4 comfffval ${⊢}{O}=\left({x}\in \left({B}×{B}\right),{y}\in {B}⟼\left({g}\in \left({2}^{nd}\left({x}\right)\mathrm{Hom}\left({C}\right){y}\right),{f}\in \mathrm{Hom}\left({C}\right)\left({x}\right)⟼{g}\left({x}\mathrm{comp}\left({C}\right){y}\right){f}\right)\right)$
6 ovex ${⊢}{2}^{nd}\left({x}\right)\mathrm{Hom}\left({C}\right){y}\in \mathrm{V}$
7 fvex ${⊢}\mathrm{Hom}\left({C}\right)\left({x}\right)\in \mathrm{V}$
8 6 7 mpoex ${⊢}\left({g}\in \left({2}^{nd}\left({x}\right)\mathrm{Hom}\left({C}\right){y}\right),{f}\in \mathrm{Hom}\left({C}\right)\left({x}\right)⟼{g}\left({x}\mathrm{comp}\left({C}\right){y}\right){f}\right)\in \mathrm{V}$
9 5 8 fnmpoi ${⊢}{O}Fn\left(\left({B}×{B}\right)×{B}\right)$