# Metamath Proof Explorer

## Theorem comfffval

Description: Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

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
Assertion comfffval

### 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 fveq2 ${⊢}{c}={C}\to {\mathrm{Base}}_{{c}}={\mathrm{Base}}_{{C}}$
6 5 2 syl6eqr ${⊢}{c}={C}\to {\mathrm{Base}}_{{c}}={B}$
7 6 sqxpeqd ${⊢}{c}={C}\to {\mathrm{Base}}_{{c}}×{\mathrm{Base}}_{{c}}={B}×{B}$
8 fveq2 ${⊢}{c}={C}\to \mathrm{Hom}\left({c}\right)=\mathrm{Hom}\left({C}\right)$
9 8 3 syl6eqr ${⊢}{c}={C}\to \mathrm{Hom}\left({c}\right)={H}$
10 9 oveqd ${⊢}{c}={C}\to {2}^{nd}\left({x}\right)\mathrm{Hom}\left({c}\right){y}={2}^{nd}\left({x}\right){H}{y}$
11 9 fveq1d ${⊢}{c}={C}\to \mathrm{Hom}\left({c}\right)\left({x}\right)={H}\left({x}\right)$
12 fveq2 ${⊢}{c}={C}\to \mathrm{comp}\left({c}\right)=\mathrm{comp}\left({C}\right)$
13 12 4 syl6eqr
14 13 oveqd
15 14 oveqd
16 10 11 15 mpoeq123dv
17 7 6 16 mpoeq123dv
18 df-comf ${⊢}{\mathrm{comp}}_{𝑓}=\left({c}\in \mathrm{V}⟼\left({x}\in \left({\mathrm{Base}}_{{c}}×{\mathrm{Base}}_{{c}}\right),{y}\in {\mathrm{Base}}_{{c}}⟼\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)\right)$
19 2 fvexi ${⊢}{B}\in \mathrm{V}$
20 19 19 xpex ${⊢}{B}×{B}\in \mathrm{V}$
21 20 19 mpoex
22 17 18 21 fvmpt
23 fvprc ${⊢}¬{C}\in \mathrm{V}\to {\mathrm{comp}}_{𝑓}\left({C}\right)=\varnothing$
24 fvprc ${⊢}¬{C}\in \mathrm{V}\to {\mathrm{Base}}_{{C}}=\varnothing$
25 2 24 syl5eq ${⊢}¬{C}\in \mathrm{V}\to {B}=\varnothing$
26 25 olcd ${⊢}¬{C}\in \mathrm{V}\to \left({B}×{B}=\varnothing \vee {B}=\varnothing \right)$
27 0mpo0
28 26 27 syl
29 23 28 eqtr4d
30 22 29 pm2.61i
31 1 30 eqtri