Metamath Proof Explorer


Theorem curf2cl

Description: The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses curf2.g G = C D curry F F
curf2.a A = Base C
curf2.c φ C Cat
curf2.d φ D Cat
curf2.f φ F C × c D Func E
curf2.b B = Base D
curf2.h H = Hom C
curf2.i I = Id D
curf2.x φ X A
curf2.y φ Y A
curf2.k φ K X H Y
curf2.l L = X 2 nd G Y K
curf2.n N = D Nat E
Assertion curf2cl φ L 1 st G X N 1 st G Y

Proof

Step Hyp Ref Expression
1 curf2.g G = C D curry F F
2 curf2.a A = Base C
3 curf2.c φ C Cat
4 curf2.d φ D Cat
5 curf2.f φ F C × c D Func E
6 curf2.b B = Base D
7 curf2.h H = Hom C
8 curf2.i I = Id D
9 curf2.x φ X A
10 curf2.y φ Y A
11 curf2.k φ K X H Y
12 curf2.l L = X 2 nd G Y K
13 curf2.n N = D Nat E
14 1 2 3 4 5 6 7 8 9 10 11 12 curf2 φ L = z B K X z 2 nd F Y z I z
15 eqid C × c D = C × c D
16 15 2 6 xpcbas A × B = Base C × c D
17 eqid Hom C × c D = Hom C × c D
18 eqid Hom E = Hom E
19 relfunc Rel C × c D Func E
20 1st2ndbr Rel C × c D Func E F C × c D Func E 1 st F C × c D Func E 2 nd F
21 19 5 20 sylancr φ 1 st F C × c D Func E 2 nd F
22 21 adantr φ z B 1 st F C × c D Func E 2 nd F
23 opelxpi X A z B X z A × B
24 9 23 sylan φ z B X z A × B
25 opelxpi Y A z B Y z A × B
26 10 25 sylan φ z B Y z A × B
27 16 17 18 22 24 26 funcf2 φ z B X z 2 nd F Y z : X z Hom C × c D Y z 1 st F X z Hom E 1 st F Y z
28 eqid Hom D = Hom D
29 9 adantr φ z B X A
30 simpr φ z B z B
31 10 adantr φ z B Y A
32 15 2 6 7 28 29 30 31 30 17 xpchom2 φ z B X z Hom C × c D Y z = X H Y × z Hom D z
33 32 feq2d φ z B X z 2 nd F Y z : X z Hom C × c D Y z 1 st F X z Hom E 1 st F Y z X z 2 nd F Y z : X H Y × z Hom D z 1 st F X z Hom E 1 st F Y z
34 27 33 mpbid φ z B X z 2 nd F Y z : X H Y × z Hom D z 1 st F X z Hom E 1 st F Y z
35 11 adantr φ z B K X H Y
36 4 adantr φ z B D Cat
37 6 28 8 36 30 catidcl φ z B I z z Hom D z
38 34 35 37 fovrnd φ z B K X z 2 nd F Y z I z 1 st F X z Hom E 1 st F Y z
39 3 adantr φ z B C Cat
40 5 adantr φ z B F C × c D Func E
41 eqid 1 st G X = 1 st G X
42 1 2 39 36 40 6 29 41 30 curf11 φ z B 1 st 1 st G X z = X 1 st F z
43 df-ov X 1 st F z = 1 st F X z
44 42 43 eqtrdi φ z B 1 st 1 st G X z = 1 st F X z
45 eqid 1 st G Y = 1 st G Y
46 1 2 39 36 40 6 31 45 30 curf11 φ z B 1 st 1 st G Y z = Y 1 st F z
47 df-ov Y 1 st F z = 1 st F Y z
48 46 47 eqtrdi φ z B 1 st 1 st G Y z = 1 st F Y z
49 44 48 oveq12d φ z B 1 st 1 st G X z Hom E 1 st 1 st G Y z = 1 st F X z Hom E 1 st F Y z
50 38 49 eleqtrrd φ z B K X z 2 nd F Y z I z 1 st 1 st G X z Hom E 1 st 1 st G Y z
51 50 ralrimiva φ z B K X z 2 nd F Y z I z 1 st 1 st G X z Hom E 1 st 1 st G Y z
52 6 fvexi B V
53 mptelixpg B V z B K X z 2 nd F Y z I z z B 1 st 1 st G X z Hom E 1 st 1 st G Y z z B K X z 2 nd F Y z I z 1 st 1 st G X z Hom E 1 st 1 st G Y z
54 52 53 ax-mp z B K X z 2 nd F Y z I z z B 1 st 1 st G X z Hom E 1 st 1 st G Y z z B K X z 2 nd F Y z I z 1 st 1 st G X z Hom E 1 st 1 st G Y z
55 51 54 sylibr φ z B K X z 2 nd F Y z I z z B 1 st 1 st G X z Hom E 1 st 1 st G Y z
56 14 55 eqeltrd φ L z B 1 st 1 st G X z Hom E 1 st 1 st G Y z
57 eqid Id C = Id C
58 3 adantr φ z B w B f z Hom D w C Cat
59 9 adantr φ z B w B f z Hom D w X A
60 eqid comp C = comp C
61 10 adantr φ z B w B f z Hom D w Y A
62 11 adantr φ z B w B f z Hom D w K X H Y
63 2 7 57 58 59 60 61 62 catrid φ z B w B f z Hom D w K X X comp C Y Id C X = K
64 2 7 57 58 59 60 61 62 catlid φ z B w B f z Hom D w Id C Y X Y comp C Y K = K
65 63 64 eqtr4d φ z B w B f z Hom D w K X X comp C Y Id C X = Id C Y X Y comp C Y K
66 4 adantr φ z B w B f z Hom D w D Cat
67 simpr1 φ z B w B f z Hom D w z B
68 eqid comp D = comp D
69 simpr2 φ z B w B f z Hom D w w B
70 simpr3 φ z B w B f z Hom D w f z Hom D w
71 6 28 8 66 67 68 69 70 catlid φ z B w B f z Hom D w I w z w comp D w f = f
72 6 28 8 66 67 68 69 70 catrid φ z B w B f z Hom D w f z z comp D w I z = f
73 71 72 eqtr4d φ z B w B f z Hom D w I w z w comp D w f = f z z comp D w I z
74 65 73 opeq12d φ z B w B f z Hom D w K X X comp C Y Id C X I w z w comp D w f = Id C Y X Y comp C Y K f z z comp D w I z
75 eqid comp C × c D = comp C × c D
76 2 7 57 58 59 catidcl φ z B w B f z Hom D w Id C X X H X
77 6 28 8 66 69 catidcl φ z B w B f z Hom D w I w w Hom D w
78 15 2 6 7 28 59 67 59 69 60 68 75 61 69 76 70 62 77 xpcco2 φ z B w B f z Hom D w K I w X z X w comp C × c D Y w Id C X f = K X X comp C Y Id C X I w z w comp D w f
79 37 3ad2antr1 φ z B w B f z Hom D w I z z Hom D z
80 2 7 57 58 61 catidcl φ z B w B f z Hom D w Id C Y Y H Y
81 15 2 6 7 28 59 67 61 67 60 68 75 61 69 62 79 80 70 xpcco2 φ z B w B f z Hom D w Id C Y f X z Y z comp C × c D Y w K I z = Id C Y X Y comp C Y K f z z comp D w I z
82 74 78 81 3eqtr4d φ z B w B f z Hom D w K I w X z X w comp C × c D Y w Id C X f = Id C Y f X z Y z comp C × c D Y w K I z
83 82 fveq2d φ z B w B f z Hom D w X z 2 nd F Y w K I w X z X w comp C × c D Y w Id C X f = X z 2 nd F Y w Id C Y f X z Y z comp C × c D Y w K I z
84 eqid comp E = comp E
85 21 adantr φ z B w B f z Hom D w 1 st F C × c D Func E 2 nd F
86 24 3ad2antr1 φ z B w B f z Hom D w X z A × B
87 59 69 opelxpd φ z B w B f z Hom D w X w A × B
88 61 69 opelxpd φ z B w B f z Hom D w Y w A × B
89 76 70 opelxpd φ z B w B f z Hom D w Id C X f X H X × z Hom D w
90 15 2 6 7 28 59 67 59 69 17 xpchom2 φ z B w B f z Hom D w X z Hom C × c D X w = X H X × z Hom D w
91 89 90 eleqtrrd φ z B w B f z Hom D w Id C X f X z Hom C × c D X w
92 62 77 opelxpd φ z B w B f z Hom D w K I w X H Y × w Hom D w
93 15 2 6 7 28 59 69 61 69 17 xpchom2 φ z B w B f z Hom D w X w Hom C × c D Y w = X H Y × w Hom D w
94 92 93 eleqtrrd φ z B w B f z Hom D w K I w X w Hom C × c D Y w
95 16 17 75 84 85 86 87 88 91 94 funcco φ z B w B f z Hom D w X z 2 nd F Y w K I w X z X w comp C × c D Y w Id C X f = X w 2 nd F Y w K I w 1 st F X z 1 st F X w comp E 1 st F Y w X z 2 nd F X w Id C X f
96 26 3ad2antr1 φ z B w B f z Hom D w Y z A × B
97 62 79 opelxpd φ z B w B f z Hom D w K I z X H Y × z Hom D z
98 15 2 6 7 28 59 67 61 67 17 xpchom2 φ z B w B f z Hom D w X z Hom C × c D Y z = X H Y × z Hom D z
99 97 98 eleqtrrd φ z B w B f z Hom D w K I z X z Hom C × c D Y z
100 80 70 opelxpd φ z B w B f z Hom D w Id C Y f Y H Y × z Hom D w
101 15 2 6 7 28 61 67 61 69 17 xpchom2 φ z B w B f z Hom D w Y z Hom C × c D Y w = Y H Y × z Hom D w
102 100 101 eleqtrrd φ z B w B f z Hom D w Id C Y f Y z Hom C × c D Y w
103 16 17 75 84 85 86 96 88 99 102 funcco φ z B w B f z Hom D w X z 2 nd F Y w Id C Y f X z Y z comp C × c D Y w K I z = Y z 2 nd F Y w Id C Y f 1 st F X z 1 st F Y z comp E 1 st F Y w X z 2 nd F Y z K I z
104 83 95 103 3eqtr3d φ z B w B f z Hom D w X w 2 nd F Y w K I w 1 st F X z 1 st F X w comp E 1 st F Y w X z 2 nd F X w Id C X f = Y z 2 nd F Y w Id C Y f 1 st F X z 1 st F Y z comp E 1 st F Y w X z 2 nd F Y z K I z
105 5 adantr φ z B w B f z Hom D w F C × c D Func E
106 1 2 58 66 105 6 59 41 67 curf11 φ z B w B f z Hom D w 1 st 1 st G X z = X 1 st F z
107 106 43 eqtrdi φ z B w B f z Hom D w 1 st 1 st G X z = 1 st F X z
108 1 2 58 66 105 6 59 41 69 curf11 φ z B w B f z Hom D w 1 st 1 st G X w = X 1 st F w
109 df-ov X 1 st F w = 1 st F X w
110 108 109 eqtrdi φ z B w B f z Hom D w 1 st 1 st G X w = 1 st F X w
111 107 110 opeq12d φ z B w B f z Hom D w 1 st 1 st G X z 1 st 1 st G X w = 1 st F X z 1 st F X w
112 1 2 58 66 105 6 61 45 69 curf11 φ z B w B f z Hom D w 1 st 1 st G Y w = Y 1 st F w
113 df-ov Y 1 st F w = 1 st F Y w
114 112 113 eqtrdi φ z B w B f z Hom D w 1 st 1 st G Y w = 1 st F Y w
115 111 114 oveq12d φ z B w B f z Hom D w 1 st 1 st G X z 1 st 1 st G X w comp E 1 st 1 st G Y w = 1 st F X z 1 st F X w comp E 1 st F Y w
116 1 2 58 66 105 6 7 8 59 61 62 12 69 curf2val φ z B w B f z Hom D w L w = K X w 2 nd F Y w I w
117 df-ov K X w 2 nd F Y w I w = X w 2 nd F Y w K I w
118 116 117 eqtrdi φ z B w B f z Hom D w L w = X w 2 nd F Y w K I w
119 1 2 58 66 105 6 59 41 67 28 57 69 70 curf12 φ z B w B f z Hom D w z 2 nd 1 st G X w f = Id C X X z 2 nd F X w f
120 df-ov Id C X X z 2 nd F X w f = X z 2 nd F X w Id C X f
121 119 120 eqtrdi φ z B w B f z Hom D w z 2 nd 1 st G X w f = X z 2 nd F X w Id C X f
122 115 118 121 oveq123d φ z B w B f z Hom D w L w 1 st 1 st G X z 1 st 1 st G X w comp E 1 st 1 st G Y w z 2 nd 1 st G X w f = X w 2 nd F Y w K I w 1 st F X z 1 st F X w comp E 1 st F Y w X z 2 nd F X w Id C X f
123 1 2 58 66 105 6 61 45 67 curf11 φ z B w B f z Hom D w 1 st 1 st G Y z = Y 1 st F z
124 123 47 eqtrdi φ z B w B f z Hom D w 1 st 1 st G Y z = 1 st F Y z
125 107 124 opeq12d φ z B w B f z Hom D w 1 st 1 st G X z 1 st 1 st G Y z = 1 st F X z 1 st F Y z
126 125 114 oveq12d φ z B w B f z Hom D w 1 st 1 st G X z 1 st 1 st G Y z comp E 1 st 1 st G Y w = 1 st F X z 1 st F Y z comp E 1 st F Y w
127 1 2 58 66 105 6 61 45 67 28 57 69 70 curf12 φ z B w B f z Hom D w z 2 nd 1 st G Y w f = Id C Y Y z 2 nd F Y w f
128 df-ov Id C Y Y z 2 nd F Y w f = Y z 2 nd F Y w Id C Y f
129 127 128 eqtrdi φ z B w B f z Hom D w z 2 nd 1 st G Y w f = Y z 2 nd F Y w Id C Y f
130 1 2 58 66 105 6 7 8 59 61 62 12 67 curf2val φ z B w B f z Hom D w L z = K X z 2 nd F Y z I z
131 df-ov K X z 2 nd F Y z I z = X z 2 nd F Y z K I z
132 130 131 eqtrdi φ z B w B f z Hom D w L z = X z 2 nd F Y z K I z
133 126 129 132 oveq123d φ z B w B f z Hom D w z 2 nd 1 st G Y w f 1 st 1 st G X z 1 st 1 st G Y z comp E 1 st 1 st G Y w L z = Y z 2 nd F Y w Id C Y f 1 st F X z 1 st F Y z comp E 1 st F Y w X z 2 nd F Y z K I z
134 104 122 133 3eqtr4d φ z B w B f z Hom D w L w 1 st 1 st G X z 1 st 1 st G X w comp E 1 st 1 st G Y w z 2 nd 1 st G X w f = z 2 nd 1 st G Y w f 1 st 1 st G X z 1 st 1 st G Y z comp E 1 st 1 st G Y w L z
135 134 ralrimivvva φ z B w B f z Hom D w L w 1 st 1 st G X z 1 st 1 st G X w comp E 1 st 1 st G Y w z 2 nd 1 st G X w f = z 2 nd 1 st G Y w f 1 st 1 st G X z 1 st 1 st G Y z comp E 1 st 1 st G Y w L z
136 1 2 3 4 5 6 9 41 curf1cl φ 1 st G X D Func E
137 1 2 3 4 5 6 10 45 curf1cl φ 1 st G Y D Func E
138 13 6 28 18 84 136 137 isnat2 φ L 1 st G X N 1 st G Y L z B 1 st 1 st G X z Hom E 1 st 1 st G Y z z B w B f z Hom D w L w 1 st 1 st G X z 1 st 1 st G X w comp E 1 st 1 st G Y w z 2 nd 1 st G X w f = z 2 nd 1 st G Y w f 1 st 1 st G X z 1 st 1 st G Y z comp E 1 st 1 st G Y w L z
139 56 135 138 mpbir2and φ L 1 st G X N 1 st G Y