# Metamath Proof Explorer

## Theorem curfval

Description: Value of the 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}}$
curfval.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
curfval.1
curfval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
curfval.i ${⊢}{I}=\mathrm{Id}\left({D}\right)$
Assertion curfval

### 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 curfval.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
8 curfval.1
9 curfval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
10 curfval.i ${⊢}{I}=\mathrm{Id}\left({D}\right)$
11 df-curf
12 11 a1i
13 fvexd ${⊢}\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\to {1}^{st}\left({e}\right)\in \mathrm{V}$
14 simprl ${⊢}\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\to {e}=⟨{C},{D}⟩$
15 14 fveq2d ${⊢}\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\to {1}^{st}\left({e}\right)={1}^{st}\left(⟨{C},{D}⟩\right)$
16 op1stg ${⊢}\left({C}\in \mathrm{Cat}\wedge {D}\in \mathrm{Cat}\right)\to {1}^{st}\left(⟨{C},{D}⟩\right)={C}$
17 3 4 16 syl2anc ${⊢}{\phi }\to {1}^{st}\left(⟨{C},{D}⟩\right)={C}$
18 17 adantr ${⊢}\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\to {1}^{st}\left(⟨{C},{D}⟩\right)={C}$
19 15 18 eqtrd ${⊢}\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\to {1}^{st}\left({e}\right)={C}$
20 fvexd ${⊢}\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\to {2}^{nd}\left({e}\right)\in \mathrm{V}$
21 14 adantr ${⊢}\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\to {e}=⟨{C},{D}⟩$
22 21 fveq2d ${⊢}\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\to {2}^{nd}\left({e}\right)={2}^{nd}\left(⟨{C},{D}⟩\right)$
23 op2ndg ${⊢}\left({C}\in \mathrm{Cat}\wedge {D}\in \mathrm{Cat}\right)\to {2}^{nd}\left(⟨{C},{D}⟩\right)={D}$
24 3 4 23 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{C},{D}⟩\right)={D}$
25 24 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\to {2}^{nd}\left(⟨{C},{D}⟩\right)={D}$
26 22 25 eqtrd ${⊢}\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\to {2}^{nd}\left({e}\right)={D}$
27 simplr ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {c}={C}$
28 27 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {\mathrm{Base}}_{{c}}={\mathrm{Base}}_{{C}}$
29 28 2 syl6eqr ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {\mathrm{Base}}_{{c}}={A}$
30 simpr ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {d}={D}$
31 30 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {\mathrm{Base}}_{{d}}={\mathrm{Base}}_{{D}}$
32 31 6 syl6eqr ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {\mathrm{Base}}_{{d}}={B}$
33 simprr ${⊢}\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\to {f}={F}$
34 33 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {f}={F}$
35 34 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {1}^{st}\left({f}\right)={1}^{st}\left({F}\right)$
36 35 oveqd ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {x}{1}^{st}\left({f}\right){y}={x}{1}^{st}\left({F}\right){y}$
37 32 36 mpteq12dv ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \left({y}\in {\mathrm{Base}}_{{d}}⟼{x}{1}^{st}\left({f}\right){y}\right)=\left({y}\in {B}⟼{x}{1}^{st}\left({F}\right){y}\right)$
38 30 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \mathrm{Hom}\left({d}\right)=\mathrm{Hom}\left({D}\right)$
39 38 7 syl6eqr ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \mathrm{Hom}\left({d}\right)={J}$
40 39 oveqd ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {y}\mathrm{Hom}\left({d}\right){z}={y}{J}{z}$
41 34 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {2}^{nd}\left({f}\right)={2}^{nd}\left({F}\right)$
42 41 oveqd ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to ⟨{x},{y}⟩{2}^{nd}\left({f}\right)⟨{x},{z}⟩=⟨{x},{y}⟩{2}^{nd}\left({F}\right)⟨{x},{z}⟩$
43 27 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \mathrm{Id}\left({c}\right)=\mathrm{Id}\left({C}\right)$
44 43 8 syl6eqr
45 44 fveq1d
46 eqidd ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {g}={g}$
47 42 45 46 oveq123d
48 40 47 mpteq12dv
49 32 32 48 mpoeq123dv
50 37 49 opeq12d
51 29 50 mpteq12dv
52 27 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \mathrm{Hom}\left({c}\right)=\mathrm{Hom}\left({C}\right)$
53 52 9 syl6eqr ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \mathrm{Hom}\left({c}\right)={H}$
54 53 oveqd ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {x}\mathrm{Hom}\left({c}\right){y}={x}{H}{y}$
55 41 oveqd ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to ⟨{x},{z}⟩{2}^{nd}\left({f}\right)⟨{y},{z}⟩=⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩$
56 30 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \mathrm{Id}\left({d}\right)=\mathrm{Id}\left({D}\right)$
57 56 10 syl6eqr ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \mathrm{Id}\left({d}\right)={I}$
58 57 fveq1d ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \mathrm{Id}\left({d}\right)\left({z}\right)={I}\left({z}\right)$
59 55 46 58 oveq123d ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to {g}\left(⟨{x},{z}⟩{2}^{nd}\left({f}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({d}\right)\left({z}\right)={g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right){I}\left({z}\right)$
60 32 59 mpteq12dv ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \left({z}\in {\mathrm{Base}}_{{d}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({f}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({d}\right)\left({z}\right)\right)=\left({z}\in {B}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right){I}\left({z}\right)\right)$
61 54 60 mpteq12dv ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \left({g}\in \left({x}\mathrm{Hom}\left({c}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{d}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({f}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({d}\right)\left({z}\right)\right)\right)=\left({g}\in \left({x}{H}{y}\right)⟼\left({z}\in {B}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right){I}\left({z}\right)\right)\right)$
62 29 29 61 mpoeq123dv ${⊢}\left(\left(\left({\phi }\wedge \left({e}=⟨{C},{D}⟩\wedge {f}={F}\right)\right)\wedge {c}={C}\right)\wedge {d}={D}\right)\to \left({x}\in {\mathrm{Base}}_{{c}},{y}\in {\mathrm{Base}}_{{c}}⟼\left({g}\in \left({x}\mathrm{Hom}\left({c}\right){y}\right)⟼\left({z}\in {\mathrm{Base}}_{{d}}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({f}\right)⟨{y},{z}⟩\right)\mathrm{Id}\left({d}\right)\left({z}\right)\right)\right)\right)=\left({x}\in {A},{y}\in {A}⟼\left({g}\in \left({x}{H}{y}\right)⟼\left({z}\in {B}⟼{g}\left(⟨{x},{z}⟩{2}^{nd}\left({F}\right)⟨{y},{z}⟩\right){I}\left({z}\right)\right)\right)\right)$
63 51 62 opeq12d
64 20 26 63 csbied2
65 13 19 64 csbied2
66 opex ${⊢}⟨{C},{D}⟩\in \mathrm{V}$
67 66 a1i ${⊢}{\phi }\to ⟨{C},{D}⟩\in \mathrm{V}$
68 5 elexd ${⊢}{\phi }\to {F}\in \mathrm{V}$
69 opex
70 69 a1i
71 12 65 67 68 70 ovmpod
72 1 71 syl5eq