# Metamath Proof Explorer

## Theorem curf11

Description: Value of the double evaluated curry functor. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses curfval.g ${⊢}{G}=⟨{C},{D}⟩{curry}_{F}{F}$
curfval.a ${⊢}{A}={\mathrm{Base}}_{{C}}$
curfval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
curfval.d ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
curfval.f ${⊢}{\phi }\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
curfval.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
curf1.x ${⊢}{\phi }\to {X}\in {A}$
curf1.k ${⊢}{K}={1}^{st}\left({G}\right)\left({X}\right)$
curf11.y ${⊢}{\phi }\to {Y}\in {B}$
Assertion curf11 ${⊢}{\phi }\to {1}^{st}\left({K}\right)\left({Y}\right)={X}{1}^{st}\left({F}\right){Y}$

### Proof

Step Hyp Ref Expression
1 curfval.g ${⊢}{G}=⟨{C},{D}⟩{curry}_{F}{F}$
2 curfval.a ${⊢}{A}={\mathrm{Base}}_{{C}}$
3 curfval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
4 curfval.d ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
5 curfval.f ${⊢}{\phi }\to {F}\in \left(\left({C}{×}_{c}{D}\right)\mathrm{Func}{E}\right)$
6 curfval.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
7 curf1.x ${⊢}{\phi }\to {X}\in {A}$
8 curf1.k ${⊢}{K}={1}^{st}\left({G}\right)\left({X}\right)$
9 curf11.y ${⊢}{\phi }\to {Y}\in {B}$
10 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
11 eqid ${⊢}\mathrm{Id}\left({C}\right)=\mathrm{Id}\left({C}\right)$
12 1 2 3 4 5 6 7 8 10 11 curf1 ${⊢}{\phi }\to {K}=⟨\left({y}\in {B}⟼{X}{1}^{st}\left({F}\right){y}\right),\left({y}\in {B},{z}\in {B}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({X}\right)\left(⟨{X},{y}⟩{2}^{nd}\left({F}\right)⟨{X},{z}⟩\right){g}\right)\right)⟩$
13 6 fvexi ${⊢}{B}\in \mathrm{V}$
14 13 mptex ${⊢}\left({y}\in {B}⟼{X}{1}^{st}\left({F}\right){y}\right)\in \mathrm{V}$
15 13 13 mpoex ${⊢}\left({y}\in {B},{z}\in {B}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({X}\right)\left(⟨{X},{y}⟩{2}^{nd}\left({F}\right)⟨{X},{z}⟩\right){g}\right)\right)\in \mathrm{V}$
16 14 15 op1std ${⊢}{K}=⟨\left({y}\in {B}⟼{X}{1}^{st}\left({F}\right){y}\right),\left({y}\in {B},{z}\in {B}⟼\left({g}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)⟼\mathrm{Id}\left({C}\right)\left({X}\right)\left(⟨{X},{y}⟩{2}^{nd}\left({F}\right)⟨{X},{z}⟩\right){g}\right)\right)⟩\to {1}^{st}\left({K}\right)=\left({y}\in {B}⟼{X}{1}^{st}\left({F}\right){y}\right)$
17 12 16 syl ${⊢}{\phi }\to {1}^{st}\left({K}\right)=\left({y}\in {B}⟼{X}{1}^{st}\left({F}\right){y}\right)$
18 simpr ${⊢}\left({\phi }\wedge {y}={Y}\right)\to {y}={Y}$
19 18 oveq2d ${⊢}\left({\phi }\wedge {y}={Y}\right)\to {X}{1}^{st}\left({F}\right){y}={X}{1}^{st}\left({F}\right){Y}$
20 ovexd ${⊢}{\phi }\to {X}{1}^{st}\left({F}\right){Y}\in \mathrm{V}$
21 17 19 9 20 fvmptd ${⊢}{\phi }\to {1}^{st}\left({K}\right)\left({Y}\right)={X}{1}^{st}\left({F}\right){Y}$