# Metamath Proof Explorer

## Theorem comfval

Description: Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfffval.o ${⊢}{O}={\mathrm{comp}}_{𝑓}\left({C}\right)$
comfffval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
comfffval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
comfffval.x
comffval.x ${⊢}{\phi }\to {X}\in {B}$
comffval.y ${⊢}{\phi }\to {Y}\in {B}$
comffval.z ${⊢}{\phi }\to {Z}\in {B}$
comfval.f ${⊢}{\phi }\to {F}\in \left({X}{H}{Y}\right)$
comfval.g ${⊢}{\phi }\to {G}\in \left({Y}{H}{Z}\right)$
Assertion comfval

### Proof

Step Hyp Ref Expression
1 comfffval.o ${⊢}{O}={\mathrm{comp}}_{𝑓}\left({C}\right)$
2 comfffval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 comfffval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
4 comfffval.x
5 comffval.x ${⊢}{\phi }\to {X}\in {B}$
6 comffval.y ${⊢}{\phi }\to {Y}\in {B}$
7 comffval.z ${⊢}{\phi }\to {Z}\in {B}$
8 comfval.f ${⊢}{\phi }\to {F}\in \left({X}{H}{Y}\right)$
9 comfval.g ${⊢}{\phi }\to {G}\in \left({Y}{H}{Z}\right)$
10 1 2 3 4 5 6 7 comffval
11 oveq12
12 11 adantl
13 ovexd
14 10 12 9 8 13 ovmpod