Metamath Proof Explorer


Theorem curfcl

Description: The curry functor of a functor F : C X. D --> E is a functor curryF ( F ) : C --> ( D --> E ) . (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses curfcl.g G = C D curry F F
curfcl.q Q = D FuncCat E
curfcl.c φ C Cat
curfcl.d φ D Cat
curfcl.f φ F C × c D Func E
Assertion curfcl φ G C Func Q

Proof

Step Hyp Ref Expression
1 curfcl.g G = C D curry F F
2 curfcl.q Q = D FuncCat E
3 curfcl.c φ C Cat
4 curfcl.d φ D Cat
5 curfcl.f φ F C × c D Func E
6 eqid Base C = Base C
7 eqid Base D = Base D
8 eqid Hom D = Hom D
9 eqid Id C = Id C
10 eqid Hom C = Hom C
11 eqid Id D = Id D
12 1 6 3 4 5 7 8 9 10 11 curfval φ G = 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 fvex Base C V
14 13 mptex 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 V
15 13 13 mpoex 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 V
16 14 15 op1std G = 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 1 st G = 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
17 12 16 syl φ 1 st G = 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
18 14 15 op2ndd G = 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 2 nd 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
19 12 18 syl φ 2 nd 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
20 17 19 opeq12d φ 1 st G 2 nd G = 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
21 12 20 eqtr4d φ G = 1 st G 2 nd G
22 2 fucbas D Func E = Base Q
23 eqid D Nat E = D Nat E
24 2 23 fuchom D Nat E = Hom Q
25 eqid Id Q = Id Q
26 eqid comp C = comp C
27 eqid comp Q = comp Q
28 funcrcl F C × c D Func E C × c D Cat E Cat
29 5 28 syl φ C × c D Cat E Cat
30 29 simprd φ E Cat
31 2 4 30 fuccat φ Q Cat
32 opex 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 V
33 32 a1i φ 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 V
34 3 adantr φ x Base C C Cat
35 4 adantr φ x Base C D Cat
36 5 adantr φ x Base C F C × c D Func E
37 simpr φ x Base C x Base C
38 eqid 1 st G x = 1 st G x
39 1 6 34 35 36 7 37 38 curf1cl φ x Base C 1 st G x D Func E
40 33 17 39 fmpt2d φ 1 st G : Base C D Func E
41 eqid 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 Base C , y Base C g x Hom C y z Base D g x z 2 nd F y z Id D z
42 ovex x Hom C y V
43 42 mptex g x Hom C y z Base D g x z 2 nd F y z Id D z V
44 41 43 fnmpoi 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 Fn Base C × Base C
45 19 fneq1d φ 2 nd G Fn Base C × Base C 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 Fn Base C × Base C
46 44 45 mpbiri φ 2 nd G Fn Base C × Base C
47 fvex Base D V
48 47 mptex z Base D g x z 2 nd F y z Id D z V
49 48 a1i φ 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 V
50 19 oveqd φ x 2 nd G y = x 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 y
51 41 ovmpt4g 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 V x 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 y = g x Hom C y z Base D g x z 2 nd F y z Id D z
52 43 51 mp3an3 x Base C y Base C x 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 y = g x Hom C y z Base D g x z 2 nd F y z Id D z
53 50 52 sylan9eq φ x Base C y Base C x 2 nd G y = g x Hom C y z Base D g x z 2 nd F y z Id D z
54 3 ad2antrr φ x Base C y Base C g x Hom C y C Cat
55 4 ad2antrr φ x Base C y Base C g x Hom C y D Cat
56 5 ad2antrr φ x Base C y Base C g x Hom C y F C × c D Func E
57 simplrl φ x Base C y Base C g x Hom C y x Base C
58 simplrr φ x Base C y Base C g x Hom C y y Base C
59 simpr φ x Base C y Base C g x Hom C y g x Hom C y
60 eqid x 2 nd G y g = x 2 nd G y g
61 1 6 54 55 56 7 10 11 57 58 59 60 23 curf2cl φ x Base C y Base C g x Hom C y x 2 nd G y g 1 st G x D Nat E 1 st G y
62 49 53 61 fmpt2d φ x Base C y Base C x 2 nd G y : x Hom C y 1 st G x D Nat E 1 st G y
63 eqid C × c D = C × c D
64 63 6 7 xpcbas Base C × Base D = Base C × c D
65 eqid Id C × c D = Id C × c D
66 eqid Id E = Id E
67 relfunc Rel C × c D Func E
68 1st2ndbr Rel C × c D Func E F C × c D Func E 1 st F C × c D Func E 2 nd F
69 67 5 68 sylancr φ 1 st F C × c D Func E 2 nd F
70 69 ad2antrr φ x Base C y Base D 1 st F C × c D Func E 2 nd F
71 opelxpi x Base C y Base D x y Base C × Base D
72 71 adantll φ x Base C y Base D x y Base C × Base D
73 64 65 66 70 72 funcid φ x Base C y Base D x y 2 nd F x y Id C × c D x y = Id E 1 st F x y
74 3 ad2antrr φ x Base C y Base D C Cat
75 4 ad2antrr φ x Base C y Base D D Cat
76 37 adantr φ x Base C y Base D x Base C
77 simpr φ x Base C y Base D y Base D
78 63 74 75 6 7 9 11 65 76 77 xpcid φ x Base C y Base D Id C × c D x y = Id C x Id D y
79 78 fveq2d φ x Base C y Base D x y 2 nd F x y Id C × c D x y = x y 2 nd F x y Id C x Id D y
80 df-ov Id C x x y 2 nd F x y Id D y = x y 2 nd F x y Id C x Id D y
81 79 80 syl6eqr φ x Base C y Base D x y 2 nd F x y Id C × c D x y = Id C x x y 2 nd F x y Id D y
82 5 ad2antrr φ x Base C y Base D F C × c D Func E
83 1 6 74 75 82 7 76 38 77 curf11 φ x Base C y Base D 1 st 1 st G x y = x 1 st F y
84 df-ov x 1 st F y = 1 st F x y
85 83 84 syl6req φ x Base C y Base D 1 st F x y = 1 st 1 st G x y
86 85 fveq2d φ x Base C y Base D Id E 1 st F x y = Id E 1 st 1 st G x y
87 73 81 86 3eqtr3d φ x Base C y Base D Id C x x y 2 nd F x y Id D y = Id E 1 st 1 st G x y
88 87 mpteq2dva φ x Base C y Base D Id C x x y 2 nd F x y Id D y = y Base D Id E 1 st 1 st G x y
89 30 adantr φ x Base C E Cat
90 eqid Base E = Base E
91 90 66 cidfn E Cat Id E Fn Base E
92 89 91 syl φ x Base C Id E Fn Base E
93 dffn2 Id E Fn Base E Id E : Base E V
94 92 93 sylib φ x Base C Id E : Base E V
95 relfunc Rel D Func E
96 1st2ndbr Rel D Func E 1 st G x D Func E 1 st 1 st G x D Func E 2 nd 1 st G x
97 95 39 96 sylancr φ x Base C 1 st 1 st G x D Func E 2 nd 1 st G x
98 7 90 97 funcf1 φ x Base C 1 st 1 st G x : Base D Base E
99 fcompt Id E : Base E V 1 st 1 st G x : Base D Base E Id E 1 st 1 st G x = y Base D Id E 1 st 1 st G x y
100 94 98 99 syl2anc φ x Base C Id E 1 st 1 st G x = y Base D Id E 1 st 1 st G x y
101 88 100 eqtr4d φ x Base C y Base D Id C x x y 2 nd F x y Id D y = Id E 1 st 1 st G x
102 6 10 9 34 37 catidcl φ x Base C Id C x x Hom C x
103 eqid x 2 nd G x Id C x = x 2 nd G x Id C x
104 1 6 34 35 36 7 10 11 37 37 102 103 curf2 φ x Base C x 2 nd G x Id C x = y Base D Id C x x y 2 nd F x y Id D y
105 2 25 66 39 fucid φ x Base C Id Q 1 st G x = Id E 1 st 1 st G x
106 101 104 105 3eqtr4d φ x Base C x 2 nd G x Id C x = Id Q 1 st G x
107 3 3ad2ant1 φ x Base C y Base C z Base C f x Hom C y g y Hom C z C Cat
108 107 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D C Cat
109 4 3ad2ant1 φ x Base C y Base C z Base C f x Hom C y g y Hom C z D Cat
110 109 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D D Cat
111 5 3ad2ant1 φ x Base C y Base C z Base C f x Hom C y g y Hom C z F C × c D Func E
112 111 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D F C × c D Func E
113 simp21 φ x Base C y Base C z Base C f x Hom C y g y Hom C z x Base C
114 113 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D x Base C
115 simpr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D w Base D
116 1 6 108 110 112 7 114 38 115 curf11 φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D 1 st 1 st G x w = x 1 st F w
117 df-ov x 1 st F w = 1 st F x w
118 116 117 syl6eq φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D 1 st 1 st G x w = 1 st F x w
119 simp22 φ x Base C y Base C z Base C f x Hom C y g y Hom C z y Base C
120 119 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D y Base C
121 eqid 1 st G y = 1 st G y
122 1 6 108 110 112 7 120 121 115 curf11 φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D 1 st 1 st G y w = y 1 st F w
123 df-ov y 1 st F w = 1 st F y w
124 122 123 syl6eq φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D 1 st 1 st G y w = 1 st F y w
125 118 124 opeq12d φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D 1 st 1 st G x w 1 st 1 st G y w = 1 st F x w 1 st F y w
126 simp23 φ x Base C y Base C z Base C f x Hom C y g y Hom C z z Base C
127 126 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D z Base C
128 eqid 1 st G z = 1 st G z
129 1 6 108 110 112 7 127 128 115 curf11 φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D 1 st 1 st G z w = z 1 st F w
130 df-ov z 1 st F w = 1 st F z w
131 129 130 syl6eq φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D 1 st 1 st G z w = 1 st F z w
132 125 131 oveq12d φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D 1 st 1 st G x w 1 st 1 st G y w comp E 1 st 1 st G z w = 1 st F x w 1 st F y w comp E 1 st F z w
133 simp3r φ x Base C y Base C z Base C f x Hom C y g y Hom C z g y Hom C z
134 133 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D g y Hom C z
135 eqid y 2 nd G z g = y 2 nd G z g
136 1 6 108 110 112 7 10 11 120 127 134 135 115 curf2val φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D y 2 nd G z g w = g y w 2 nd F z w Id D w
137 df-ov g y w 2 nd F z w Id D w = y w 2 nd F z w g Id D w
138 136 137 syl6eq φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D y 2 nd G z g w = y w 2 nd F z w g Id D w
139 simp3l φ x Base C y Base C z Base C f x Hom C y g y Hom C z f x Hom C y
140 139 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D f x Hom C y
141 eqid x 2 nd G y f = x 2 nd G y f
142 1 6 108 110 112 7 10 11 114 120 140 141 115 curf2val φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D x 2 nd G y f w = f x w 2 nd F y w Id D w
143 df-ov f x w 2 nd F y w Id D w = x w 2 nd F y w f Id D w
144 142 143 syl6eq φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D x 2 nd G y f w = x w 2 nd F y w f Id D w
145 132 138 144 oveq123d φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D y 2 nd G z g w 1 st 1 st G x w 1 st 1 st G y w comp E 1 st 1 st G z w x 2 nd G y f w = y w 2 nd F z w g Id D w 1 st F x w 1 st F y w comp E 1 st F z w x w 2 nd F y w f Id D w
146 eqid Hom C × c D = Hom C × c D
147 eqid comp C × c D = comp C × c D
148 eqid comp E = comp E
149 67 112 68 sylancr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D 1 st F C × c D Func E 2 nd F
150 opelxpi x Base C w Base D x w Base C × Base D
151 113 150 sylan φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D x w Base C × Base D
152 opelxpi y Base C w Base D y w Base C × Base D
153 119 152 sylan φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D y w Base C × Base D
154 opelxpi z Base C w Base D z w Base C × Base D
155 126 154 sylan φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D z w Base C × Base D
156 7 8 11 110 115 catidcl φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D Id D w w Hom D w
157 140 156 opelxpd φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D f Id D w x Hom C y × w Hom D w
158 63 6 7 10 8 114 115 120 115 146 xpchom2 φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D x w Hom C × c D y w = x Hom C y × w Hom D w
159 157 158 eleqtrrd φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D f Id D w x w Hom C × c D y w
160 134 156 opelxpd φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D g Id D w y Hom C z × w Hom D w
161 63 6 7 10 8 120 115 127 115 146 xpchom2 φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D y w Hom C × c D z w = y Hom C z × w Hom D w
162 160 161 eleqtrrd φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D g Id D w y w Hom C × c D z w
163 64 146 147 148 149 151 153 155 159 162 funcco φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D x w 2 nd F z w g Id D w x w y w comp C × c D z w f Id D w = y w 2 nd F z w g Id D w 1 st F x w 1 st F y w comp E 1 st F z w x w 2 nd F y w f Id D w
164 eqid comp D = comp D
165 63 6 7 10 8 114 115 120 115 26 164 147 127 115 140 156 134 156 xpcco2 φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D g Id D w x w y w comp C × c D z w f Id D w = g x y comp C z f Id D w w w comp D w Id D w
166 7 8 11 110 115 164 115 156 catlid φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D Id D w w w comp D w Id D w = Id D w
167 166 opeq2d φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D g x y comp C z f Id D w w w comp D w Id D w = g x y comp C z f Id D w
168 165 167 eqtrd φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D g Id D w x w y w comp C × c D z w f Id D w = g x y comp C z f Id D w
169 168 fveq2d φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D x w 2 nd F z w g Id D w x w y w comp C × c D z w f Id D w = x w 2 nd F z w g x y comp C z f Id D w
170 df-ov g x y comp C z f x w 2 nd F z w Id D w = x w 2 nd F z w g x y comp C z f Id D w
171 169 170 syl6eqr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D x w 2 nd F z w g Id D w x w y w comp C × c D z w f Id D w = g x y comp C z f x w 2 nd F z w Id D w
172 145 163 171 3eqtr2rd φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D g x y comp C z f x w 2 nd F z w Id D w = y 2 nd G z g w 1 st 1 st G x w 1 st 1 st G y w comp E 1 st 1 st G z w x 2 nd G y f w
173 172 mpteq2dva φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base D g x y comp C z f x w 2 nd F z w Id D w = w Base D y 2 nd G z g w 1 st 1 st G x w 1 st 1 st G y w comp E 1 st 1 st G z w x 2 nd G y f w
174 6 10 26 107 113 119 126 139 133 catcocl φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
175 eqid x 2 nd G z g x y comp C z f = x 2 nd G z g x y comp C z f
176 1 6 107 109 111 7 10 11 113 126 174 175 curf2 φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd G z g x y comp C z f = w Base D g x y comp C z f x w 2 nd F z w Id D w
177 1 6 107 109 111 7 10 11 113 119 139 141 23 curf2cl φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd G y f 1 st G x D Nat E 1 st G y
178 1 6 107 109 111 7 10 11 119 126 133 135 23 curf2cl φ x Base C y Base C z Base C f x Hom C y g y Hom C z y 2 nd G z g 1 st G y D Nat E 1 st G z
179 2 23 7 148 27 177 178 fucco φ x Base C y Base C z Base C f x Hom C y g y Hom C z y 2 nd G z g 1 st G x 1 st G y comp Q 1 st G z x 2 nd G y f = w Base D y 2 nd G z g w 1 st 1 st G x w 1 st 1 st G y w comp E 1 st 1 st G z w x 2 nd G y f w
180 173 176 179 3eqtr4d φ x Base C y Base C z Base C f x Hom C y g y Hom C z x 2 nd G z g x y comp C z f = y 2 nd G z g 1 st G x 1 st G y comp Q 1 st G z x 2 nd G y f
181 6 22 10 24 9 25 26 27 3 31 40 46 62 106 180 isfuncd φ 1 st G C Func Q 2 nd G
182 df-br 1 st G C Func Q 2 nd G 1 st G 2 nd G C Func Q
183 181 182 sylib φ 1 st G 2 nd G C Func Q
184 21 183 eqeltrd φ G C Func Q