# Metamath Proof Explorer

## Theorem comfffval2

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

Ref Expression
Hypotheses comfffval2.o ${⊢}{O}={\mathrm{comp}}_{𝑓}\left({C}\right)$
comfffval2.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
comfffval2.h ${⊢}{H}={\mathrm{Hom}}_{𝑓}\left({C}\right)$
comfffval2.x
Assertion comfffval2

### Proof

Step Hyp Ref Expression
1 comfffval2.o ${⊢}{O}={\mathrm{comp}}_{𝑓}\left({C}\right)$
2 comfffval2.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 comfffval2.h ${⊢}{H}={\mathrm{Hom}}_{𝑓}\left({C}\right)$
4 comfffval2.x
5 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
6 1 2 5 4 comfffval
7 xp2nd ${⊢}{x}\in \left({B}×{B}\right)\to {2}^{nd}\left({x}\right)\in {B}$
8 7 adantr ${⊢}\left({x}\in \left({B}×{B}\right)\wedge {y}\in {B}\right)\to {2}^{nd}\left({x}\right)\in {B}$
9 simpr ${⊢}\left({x}\in \left({B}×{B}\right)\wedge {y}\in {B}\right)\to {y}\in {B}$
10 3 2 5 8 9 homfval ${⊢}\left({x}\in \left({B}×{B}\right)\wedge {y}\in {B}\right)\to {2}^{nd}\left({x}\right){H}{y}={2}^{nd}\left({x}\right)\mathrm{Hom}\left({C}\right){y}$
11 xp1st ${⊢}{x}\in \left({B}×{B}\right)\to {1}^{st}\left({x}\right)\in {B}$
12 11 adantr ${⊢}\left({x}\in \left({B}×{B}\right)\wedge {y}\in {B}\right)\to {1}^{st}\left({x}\right)\in {B}$
13 3 2 5 12 8 homfval ${⊢}\left({x}\in \left({B}×{B}\right)\wedge {y}\in {B}\right)\to {1}^{st}\left({x}\right){H}{2}^{nd}\left({x}\right)={1}^{st}\left({x}\right)\mathrm{Hom}\left({C}\right){2}^{nd}\left({x}\right)$
14 df-ov ${⊢}{1}^{st}\left({x}\right){H}{2}^{nd}\left({x}\right)={H}\left(⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩\right)$
15 df-ov ${⊢}{1}^{st}\left({x}\right)\mathrm{Hom}\left({C}\right){2}^{nd}\left({x}\right)=\mathrm{Hom}\left({C}\right)\left(⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩\right)$
16 13 14 15 3eqtr3g ${⊢}\left({x}\in \left({B}×{B}\right)\wedge {y}\in {B}\right)\to {H}\left(⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩\right)=\mathrm{Hom}\left({C}\right)\left(⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩\right)$
17 1st2nd2 ${⊢}{x}\in \left({B}×{B}\right)\to {x}=⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩$
18 17 adantr ${⊢}\left({x}\in \left({B}×{B}\right)\wedge {y}\in {B}\right)\to {x}=⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩$
19 18 fveq2d ${⊢}\left({x}\in \left({B}×{B}\right)\wedge {y}\in {B}\right)\to {H}\left({x}\right)={H}\left(⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩\right)$
20 18 fveq2d ${⊢}\left({x}\in \left({B}×{B}\right)\wedge {y}\in {B}\right)\to \mathrm{Hom}\left({C}\right)\left({x}\right)=\mathrm{Hom}\left({C}\right)\left(⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩\right)$
21 16 19 20 3eqtr4d ${⊢}\left({x}\in \left({B}×{B}\right)\wedge {y}\in {B}\right)\to {H}\left({x}\right)=\mathrm{Hom}\left({C}\right)\left({x}\right)$
22 eqidd
23 10 21 22 mpoeq123dv
24 23 mpoeq3ia
25 6 24 eqtr4i