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 = Base C
curfval.c φ C Cat
curfval.d φ D Cat
curfval.f φ F C × c D Func E
curfval.b B = Base D
curfval.j J = Hom D
curfval.1 1 ˙ = Id C
curfval.h H = Hom C
curfval.i I = Id D
Assertion curfval φ G = x A y B x 1 st F y y B , z B g y J z 1 ˙ x x y 2 nd F x z g x A , y A g x H y z B g x z 2 nd F y z I z

Proof

Step Hyp Ref Expression
1 curfval.g G = C D curry F F
2 curfval.a A = Base C
3 curfval.c φ C Cat
4 curfval.d φ D Cat
5 curfval.f φ F C × c D Func E
6 curfval.b B = Base D
7 curfval.j J = Hom D
8 curfval.1 1 ˙ = Id C
9 curfval.h H = Hom C
10 curfval.i I = Id D
11 df-curf curry F = e V , f V 1 st e / c 2 nd e / d x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z
12 11 a1i φ curry F = e V , f V 1 st e / c 2 nd e / d x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z
13 fvexd φ e = C D f = F 1 st e V
14 simprl φ e = C D f = F e = C D
15 14 fveq2d φ e = C D f = F 1 st e = 1 st C D
16 op1stg C Cat D Cat 1 st C D = C
17 3 4 16 syl2anc φ 1 st C D = C
18 17 adantr φ e = C D f = F 1 st C D = C
19 15 18 eqtrd φ e = C D f = F 1 st e = C
20 fvexd φ e = C D f = F c = C 2 nd e V
21 14 adantr φ e = C D f = F c = C e = C D
22 21 fveq2d φ e = C D f = F c = C 2 nd e = 2 nd C D
23 op2ndg C Cat D Cat 2 nd C D = D
24 3 4 23 syl2anc φ 2 nd C D = D
25 24 ad2antrr φ e = C D f = F c = C 2 nd C D = D
26 22 25 eqtrd φ e = C D f = F c = C 2 nd e = D
27 simplr φ e = C D f = F c = C d = D c = C
28 27 fveq2d φ e = C D f = F c = C d = D Base c = Base C
29 28 2 syl6eqr φ e = C D f = F c = C d = D Base c = A
30 simpr φ e = C D f = F c = C d = D d = D
31 30 fveq2d φ e = C D f = F c = C d = D Base d = Base D
32 31 6 syl6eqr φ e = C D f = F c = C d = D Base d = B
33 simprr φ e = C D f = F f = F
34 33 ad2antrr φ e = C D f = F c = C d = D f = F
35 34 fveq2d φ e = C D f = F c = C d = D 1 st f = 1 st F
36 35 oveqd φ e = C D f = F c = C d = D x 1 st f y = x 1 st F y
37 32 36 mpteq12dv φ e = C D f = F c = C d = D y Base d x 1 st f y = y B x 1 st F y
38 30 fveq2d φ e = C D f = F c = C d = D Hom d = Hom D
39 38 7 syl6eqr φ e = C D f = F c = C d = D Hom d = J
40 39 oveqd φ e = C D f = F c = C d = D y Hom d z = y J z
41 34 fveq2d φ e = C D f = F c = C d = D 2 nd f = 2 nd F
42 41 oveqd φ e = C D f = F c = C d = D x y 2 nd f x z = x y 2 nd F x z
43 27 fveq2d φ e = C D f = F c = C d = D Id c = Id C
44 43 8 syl6eqr φ e = C D f = F c = C d = D Id c = 1 ˙
45 44 fveq1d φ e = C D f = F c = C d = D Id c x = 1 ˙ x
46 eqidd φ e = C D f = F c = C d = D g = g
47 42 45 46 oveq123d φ e = C D f = F c = C d = D Id c x x y 2 nd f x z g = 1 ˙ x x y 2 nd F x z g
48 40 47 mpteq12dv φ e = C D f = F c = C d = D g y Hom d z Id c x x y 2 nd f x z g = g y J z 1 ˙ x x y 2 nd F x z g
49 32 32 48 mpoeq123dv φ e = C D f = F c = C d = D y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g = y B , z B g y J z 1 ˙ x x y 2 nd F x z g
50 37 49 opeq12d φ e = C D f = F c = C d = D y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g = y B x 1 st F y y B , z B g y J z 1 ˙ x x y 2 nd F x z g
51 29 50 mpteq12dv φ e = C D f = F c = C d = D x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g = x A y B x 1 st F y y B , z B g y J z 1 ˙ x x y 2 nd F x z g
52 27 fveq2d φ e = C D f = F c = C d = D Hom c = Hom C
53 52 9 syl6eqr φ e = C D f = F c = C d = D Hom c = H
54 53 oveqd φ e = C D f = F c = C d = D x Hom c y = x H y
55 41 oveqd φ e = C D f = F c = C d = D x z 2 nd f y z = x z 2 nd F y z
56 30 fveq2d φ e = C D f = F c = C d = D Id d = Id D
57 56 10 syl6eqr φ e = C D f = F c = C d = D Id d = I
58 57 fveq1d φ e = C D f = F c = C d = D Id d z = I z
59 55 46 58 oveq123d φ e = C D f = F c = C d = D g x z 2 nd f y z Id d z = g x z 2 nd F y z I z
60 32 59 mpteq12dv φ e = C D f = F c = C d = D z Base d g x z 2 nd f y z Id d z = z B g x z 2 nd F y z I z
61 54 60 mpteq12dv φ e = C D f = F c = C d = D g x Hom c y z Base d g x z 2 nd f y z Id d z = g x H y z B g x z 2 nd F y z I z
62 29 29 61 mpoeq123dv φ e = C D f = F c = C d = D x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z = x A , y A g x H y z B g x z 2 nd F y z I z
63 51 62 opeq12d φ e = C D f = F c = C d = D x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z = x A y B x 1 st F y y B , z B g y J z 1 ˙ x x y 2 nd F x z g x A , y A g x H y z B g x z 2 nd F y z I z
64 20 26 63 csbied2 φ e = C D f = F c = C 2 nd e / d x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z = x A y B x 1 st F y y B , z B g y J z 1 ˙ x x y 2 nd F x z g x A , y A g x H y z B g x z 2 nd F y z I z
65 13 19 64 csbied2 φ e = C D f = F 1 st e / c 2 nd e / d x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z = x A y B x 1 st F y y B , z B g y J z 1 ˙ x x y 2 nd F x z g x A , y A g x H y z B g x z 2 nd F y z I z
66 opex C D V
67 66 a1i φ C D V
68 5 elexd φ F V
69 opex x A y B x 1 st F y y B , z B g y J z 1 ˙ x x y 2 nd F x z g x A , y A g x H y z B g x z 2 nd F y z I z V
70 69 a1i φ x A y B x 1 st F y y B , z B g y J z 1 ˙ x x y 2 nd F x z g x A , y A g x H y z B g x z 2 nd F y z I z V
71 12 65 67 68 70 ovmpod φ C D curry F F = x A y B x 1 st F y y B , z B g y J z 1 ˙ x x y 2 nd F x z g x A , y A g x H y z B g x z 2 nd F y z I z
72 1 71 syl5eq φ G = x A y B x 1 st F y y B , z B g y J z 1 ˙ x x y 2 nd F x z g x A , y A g x H y z B g x z 2 nd F y z I z