Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  hofcl Structured version   Unicode version

Theorem hofcl 14348
 Description: Closure of the Hom functor. Note that the codomain is the category for any universe which contains each Hom-set. This corresponds to the assertion that be locally small (with respect to ). (Contributed by Mario Carneiro, 15-Jan-2017.)
Hypotheses
Ref Expression
hofcl.m HomF
hofcl.o oppCat
hofcl.d
hofcl.c
hofcl.u
hofcl.h f
Assertion
Ref Expression
hofcl c

Proof of Theorem hofcl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hofcl.m . . . 4 HomF
2 hofcl.c . . . 4
3 eqid 2435 . . . 4
4 eqid 2435 . . . 4
5 eqid 2435 . . . 4 comp comp
61, 2, 3, 4, 5hofval 14341 . . 3 f comp comp
7 fvex 5734 . . . . . 6 f
8 fvex 5734 . . . . . . . 8
98, 8xpex 4982 . . . . . . 7
109, 9mpt2ex 6417 . . . . . 6 comp comp
117, 10op2ndd 6350 . . . . 5 f comp comp comp comp
126, 11syl 16 . . . 4 comp comp
1312opeq2d 3983 . . 3 f f comp comp
146, 13eqtr4d 2470 . 2 f
15 eqid 2435 . . . . 5 c c
16 hofcl.o . . . . . 6 oppCat
1716, 3oppcbas 13936 . . . . 5
1815, 17, 3xpcbas 14267 . . . 4 c
19 eqid 2435 . . . 4
20 eqid 2435 . . . 4 c c
21 eqid 2435 . . . 4
22 eqid 2435 . . . 4 c c
23 eqid 2435 . . . 4
24 eqid 2435 . . . 4 comp c comp c
25 eqid 2435 . . . 4 comp comp
2616oppccat 13940 . . . . . 6
272, 26syl 16 . . . . 5
2815, 27, 2xpccat 14279 . . . 4 c
29 hofcl.u . . . . 5
30 hofcl.d . . . . . 6
3130setccat 14232 . . . . 5
3229, 31syl 16 . . . 4
33 eqid 2435 . . . . . . . 8 f f
3433, 3homffn 13911 . . . . . . 7 f
3534a1i 11 . . . . . 6 f
36 hofcl.h . . . . . 6 f
37 df-f 5450 . . . . . 6 f f f
3835, 36, 37sylanbrc 646 . . . . 5 f
3930, 29setcbas 14225 . . . . . 6
40 feq3 5570 . . . . . 6 f f
4139, 40syl 16 . . . . 5 f f
4238, 41mpbid 202 . . . 4 f
43 eqid 2435 . . . . . 6 comp comp comp comp
44 ovex 6098 . . . . . . 7
45 ovex 6098 . . . . . . 7
4644, 45mpt2ex 6417 . . . . . 6 comp comp
4743, 46fnmpt2i 6412 . . . . 5 comp comp
4812fneq1d 5528 . . . . 5 comp comp
4947, 48mpbiri 225 . . . 4
502ad3antrrr 711 . . . . . . . . . . . 12
51 simplrr 738 . . . . . . . . . . . . . 14
52 xp1st 6368 . . . . . . . . . . . . . 14
5351, 52syl 16 . . . . . . . . . . . . 13
5453adantr 452 . . . . . . . . . . . 12
55 simplrl 737 . . . . . . . . . . . . . 14
56 xp1st 6368 . . . . . . . . . . . . . 14
5755, 56syl 16 . . . . . . . . . . . . 13
5857adantr 452 . . . . . . . . . . . 12
59 xp2nd 6369 . . . . . . . . . . . . . 14
6051, 59syl 16 . . . . . . . . . . . . 13
6160adantr 452 . . . . . . . . . . . 12
62 simplrl 737 . . . . . . . . . . . 12
63 1st2nd2 6378 . . . . . . . . . . . . . . . . 17
6455, 63syl 16 . . . . . . . . . . . . . . . 16
6564adantr 452 . . . . . . . . . . . . . . 15
6665oveq1d 6088 . . . . . . . . . . . . . 14 comp comp
6766oveqd 6090 . . . . . . . . . . . . 13 comp comp
68 xp2nd 6369 . . . . . . . . . . . . . . . 16
6955, 68syl 16 . . . . . . . . . . . . . . 15
7069adantr 452 . . . . . . . . . . . . . 14
7164fveq2d 5724 . . . . . . . . . . . . . . . . 17
72 df-ov 6076 . . . . . . . . . . . . . . . . 17
7371, 72syl6eqr 2485 . . . . . . . . . . . . . . . 16
7473eleq2d 2502 . . . . . . . . . . . . . . 15
7574biimpa 471 . . . . . . . . . . . . . 14
76 simplrr 738 . . . . . . . . . . . . . 14
773, 4, 5, 50, 58, 70, 61, 75, 76catcocl 13902 . . . . . . . . . . . . 13 comp
7867, 77eqeltrd 2509 . . . . . . . . . . . 12 comp
793, 4, 5, 50, 54, 58, 61, 62, 78catcocl 13902 . . . . . . . . . . 11 comp comp
80 1st2nd2 6378 . . . . . . . . . . . . . . 15
8151, 80syl 16 . . . . . . . . . . . . . 14
8281fveq2d 5724 . . . . . . . . . . . . 13
83 df-ov 6076 . . . . . . . . . . . . 13
8482, 83syl6eqr 2485 . . . . . . . . . . . 12
8584adantr 452 . . . . . . . . . . 11
8679, 85eleqtrrd 2512 . . . . . . . . . 10 comp comp
87 eqid 2435 . . . . . . . . . 10 comp comp comp comp
8886, 87fmptd 5885 . . . . . . . . 9 comp comp
8929ad2antrr 707 . . . . . . . . . 10
9033, 3, 4, 57, 69homfval 13910 . . . . . . . . . . . 12 f
9164fveq2d 5724 . . . . . . . . . . . . 13 f f
92 df-ov 6076 . . . . . . . . . . . . 13 f f
9391, 92syl6eqr 2485 . . . . . . . . . . . 12 f f
9490, 93, 733eqtr4d 2477 . . . . . . . . . . 11 f
9538ad2antrr 707 . . . . . . . . . . . 12 f
9695, 55ffvelrnd 5863 . . . . . . . . . . 11 f
9794, 96eqeltrrd 2510 . . . . . . . . . 10
9833, 3, 4, 53, 60homfval 13910 . . . . . . . . . . . 12 f
9981fveq2d 5724 . . . . . . . . . . . . 13 f f
100 df-ov 6076 . . . . . . . . . . . . 13 f f
10199, 100syl6eqr 2485 . . . . . . . . . . . 12 f f
10298, 101, 843eqtr4d 2477 . . . . . . . . . . 11 f
10395, 51ffvelrnd 5863 . . . . . . . . . . 11 f
104102, 103eqeltrrd 2510 . . . . . . . . . 10
10530, 89, 21, 97, 104elsetchom 14228 . . . . . . . . 9 comp comp comp comp
10688, 105mpbird 224 . . . . . . . 8 comp comp
10794, 102oveq12d 6091 . . . . . . . 8 f f
108106, 107eleqtrrd 2512 . . . . . . 7 comp comp f f
109108ralrimivva 2790 . . . . . 6 comp comp f f
110 eqid 2435 . . . . . . 7 comp comp comp comp
111110fmpt2 6410 . . . . . 6 comp comp f f comp comp f f
112109, 111sylib 189 . . . . 5 comp comp f f
11312oveqd 6090 . . . . . . 7 comp comp
11443ovmpt4g 6188 . . . . . . . 8 comp comp comp comp comp comp
11546, 114mp3an3 1268 . . . . . . 7 comp comp comp comp
116113, 115sylan9eq 2487 . . . . . 6 comp comp
117 eqid 2435 . . . . . . . 8
118 simprl 733 . . . . . . . 8
119 simprr 734 . . . . . . . 8
12015, 18, 117, 4, 20, 118, 119xpchom 14269 . . . . . . 7 c
1214, 16oppchom 13933 . . . . . . . 8
122121xpeq1i 4890 . . . . . . 7
123120, 122syl6eq 2483 . . . . . 6 c
124116, 123feq12d 5574 . . . . 5 c f f comp comp f f
125112, 124mpbird 224 . . . 4 c f f
126 eqid 2435 . . . . . . . . . 10
1272ad2antrr 707 . . . . . . . . . 10
12856adantl 453 . . . . . . . . . . 11
129128adantr 452 . . . . . . . . . 10
13068adantl 453 . . . . . . . . . . 11
131130adantr 452 . . . . . . . . . 10
132 simpr 448 . . . . . . . . . 10
1333, 4, 126, 127, 129, 5, 131, 132catlid 13900 . . . . . . . . 9 comp
134133oveq1d 6088 . . . . . . . 8 comp comp comp
1353, 4, 126, 127, 129, 5, 131, 132catrid 13901 . . . . . . . 8 comp
136134, 135eqtrd 2467 . . . . . . 7 comp comp
137136mpteq2dva 4287 . . . . . 6 comp comp
138 df-ov 6076 . . . . . . 7
1392adantr 452 . . . . . . . 8
1403, 4, 126, 139, 128catidcl 13899 . . . . . . . 8
1413, 4, 126, 139, 130catidcl 13899 . . . . . . . 8
1421, 139, 3, 4, 128, 130, 128, 130, 5, 140, 141hof2val 14345 . . . . . . 7 comp comp
143138, 142syl5eqr 2481 . . . . . 6 comp comp
14463adantl 453 . . . . . . . . . . 11
145144fveq2d 5724 . . . . . . . . . 10 f f
146145, 92syl6eqr 2485 . . . . . . . . 9 f f
14733, 3, 4, 128, 130homfval 13910 . . . . . . . . 9 f
148146, 147eqtrd 2467 . . . . . . . 8 f
149148reseq2d 5138 . . . . . . 7 f
150 mptresid 5187 . . . . . . 7
151149, 150syl6eqr 2485 . . . . . 6 f
152137, 143, 1513eqtr4d 2477 . . . . 5 f
153144, 144oveq12d 6091 . . . . . 6
154144fveq2d 5724 . . . . . . 7 c c
15527adantr 452 . . . . . . . 8
156 eqid 2435 . . . . . . . 8
15715, 155, 139, 17, 3, 156, 126, 22, 128, 130xpcid 14278 . . . . . . 7 c
15816, 126oppcid 13939 . . . . . . . . . 10
159139, 158syl 16 . . . . . . . . 9
160159fveq1d 5722 . . . . . . . 8
161160opeq1d 3982 . . . . . . 7
162154, 157, 1613eqtrd 2471 . . . . . 6 c
163153, 162fveq12d 5726 . . . . 5 c
16429adantr 452 . . . . . 6
16538ffvelrnda 5862 . . . . . 6 f
16630, 23, 164, 165setcid 14233 . . . . 5 f f
167152, 163, 1663eqtr4d 2477 . . . 4 c f
16823ad2ant1 978 . . . . . 6 c c
169293ad2ant1 978 . . . . . 6 c c
170363ad2ant1 978 . . . . . 6 c c f
171 simp21 990 . . . . . . 7 c c
172171, 56syl 16 . . . . . 6 c c
173171, 68syl 16 . . . . . 6 c c
174 simp22 991 . . . . . . 7 c c
175174, 52syl 16 . . . . . 6 c c
176174, 59syl 16 . . . . . 6 c c
177 simp23 992 . . . . . . 7 c c
178 xp1st 6368 . . . . . . 7
179177, 178syl 16 . . . . . 6 c c
180 xp2nd 6369 . . . . . . 7
181177, 180syl 16 . . . . . 6 c c
182 simp3l 985 . . . . . . . . 9 c c c
18315, 18, 117, 4, 20, 171, 174xpchom 14269 . . . . . . . . 9 c c c
184182, 183eleqtrd 2511 . . . . . . . 8 c c
185 xp1st 6368 . . . . . . . 8
186184, 185syl 16 . . . . . . 7 c c
187186, 121syl6eleq 2525 . . . . . 6 c c
188 xp2nd 6369 . . . . . . 7
189184, 188syl 16 . . . . . 6 c c
190 simp3r 986 . . . . . . . . 9 c c c
19115, 18, 117, 4, 20, 174, 177xpchom 14269 . . . . . . . . 9 c c c
192190, 191eleqtrd 2511 . . . . . . . 8 c c
193 xp1st 6368 . . . . . . . 8
194192, 193syl 16 . . . . . . 7 c c
1954, 16oppchom 13933 . . . . . . 7
196194, 195syl6eleq 2525 . . . . . 6