Metamath Proof Explorer


Theorem curf2val

Description: Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses curf2.g G=CDcurryFF
curf2.a A=BaseC
curf2.c φCCat
curf2.d φDCat
curf2.f φFC×cDFuncE
curf2.b B=BaseD
curf2.h H=HomC
curf2.i I=IdD
curf2.x φXA
curf2.y φYA
curf2.k φKXHY
curf2.l L=X2ndGYK
curf2.z φZB
Assertion curf2val φLZ=KXZ2ndFYZIZ

Proof

Step Hyp Ref Expression
1 curf2.g G=CDcurryFF
2 curf2.a A=BaseC
3 curf2.c φCCat
4 curf2.d φDCat
5 curf2.f φFC×cDFuncE
6 curf2.b B=BaseD
7 curf2.h H=HomC
8 curf2.i I=IdD
9 curf2.x φXA
10 curf2.y φYA
11 curf2.k φKXHY
12 curf2.l L=X2ndGYK
13 curf2.z φZB
14 1 2 3 4 5 6 7 8 9 10 11 12 curf2 φL=zBKXz2ndFYzIz
15 simpr φz=Zz=Z
16 15 opeq2d φz=ZXz=XZ
17 15 opeq2d φz=ZYz=YZ
18 16 17 oveq12d φz=ZXz2ndFYz=XZ2ndFYZ
19 eqidd φz=ZK=K
20 15 fveq2d φz=ZIz=IZ
21 18 19 20 oveq123d φz=ZKXz2ndFYzIz=KXZ2ndFYZIZ
22 ovexd φKXZ2ndFYZIZV
23 14 21 13 22 fvmptd φLZ=KXZ2ndFYZIZ