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

Theorem yonedalem3b 14414
 Description: Lemma for yoneda 14418. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
yoneda.y Yon
yoneda.b
yoneda.1
yoneda.o oppCat
yoneda.s
yoneda.t
yoneda.q FuncCat
yoneda.h HomF
yoneda.r c FuncCat
yoneda.e evalF
yoneda.z func tpos func F ⟨,⟩F F
yoneda.c
yoneda.w
yoneda.u f
yoneda.v f
yonedalem21.f
yonedalem21.x
yonedalem22.g
yonedalem22.p
yonedalem22.a Nat
yonedalem22.k
yonedalem3.m Nat
Assertion
Ref Expression
yonedalem3b comp comp
Distinct variable groups:   ,,,   ,   ,,,   ,,   ,,,   ,   ,,,   ,,,   ,,,   ,,,   ,,,   ,   ,,,   ,,,   ,,,   ,,,   ,,,
Allowed substitution hints:   (,)   (,,)   (,)   (,,)   ()   (,,)   (,)   (,,)   (,,)   (,,)

Proof of Theorem yonedalem3b
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6125 . . . . . . . 8 comp comp
21oveq1d 6132 . . . . . . 7 comp comp comp comp
32fveq1d 5765 . . . . . 6 comp comp comp comp
43fveq1d 5765 . . . . 5 comp comp comp comp
54cbvmptv 4331 . . . 4 Nat comp comp Nat comp comp
6 yoneda.q . . . . . . . . 9 FuncCat
7 eqid 2443 . . . . . . . . 9 Nat Nat
8 yoneda.o . . . . . . . . . 10 oppCat
9 yoneda.b . . . . . . . . . 10
108, 9oppcbas 13982 . . . . . . . . 9
11 eqid 2443 . . . . . . . . 9 comp comp
12 eqid 2443 . . . . . . . . 9 comp comp
13 eqid 2443 . . . . . . . . . . . 12
146, 7fuchom 14196 . . . . . . . . . . . 12 Nat
15 relfunc 14097 . . . . . . . . . . . . 13
16 yoneda.y . . . . . . . . . . . . . 14 Yon
17 yoneda.c . . . . . . . . . . . . . 14
18 yoneda.s . . . . . . . . . . . . . 14
19 yoneda.w . . . . . . . . . . . . . . 15
20 yoneda.v . . . . . . . . . . . . . . . 16 f
2120unssbd 3514 . . . . . . . . . . . . . . 15
2219, 21ssexd 4385 . . . . . . . . . . . . . 14
23 yoneda.u . . . . . . . . . . . . . 14 f
2416, 17, 8, 18, 6, 22, 23yoncl 14397 . . . . . . . . . . . . 13
25 1st2ndbr 6432 . . . . . . . . . . . . 13
2615, 24, 25sylancr 646 . . . . . . . . . . . 12
27 yonedalem22.p . . . . . . . . . . . 12
28 yonedalem21.x . . . . . . . . . . . 12
299, 13, 14, 26, 27, 28funcf2 14103 . . . . . . . . . . 11 Nat
30 yonedalem22.k . . . . . . . . . . 11
3129, 30ffvelrnd 5907 . . . . . . . . . 10 Nat
3231adantr 453 . . . . . . . . 9 Nat Nat
33 simpr 449 . . . . . . . . . 10 Nat Nat
34 yonedalem22.a . . . . . . . . . . 11 Nat
3534adantr 453 . . . . . . . . . 10 Nat Nat
366, 7, 12, 33, 35fuccocl 14199 . . . . . . . . 9 Nat comp Nat
3727adantr 453 . . . . . . . . 9 Nat
386, 7, 10, 11, 12, 32, 36, 37fuccoval 14198 . . . . . . . 8 Nat comp comp comp comp
396, 7, 10, 11, 12, 33, 35, 37fuccoval 14198 . . . . . . . . . 10 Nat comp comp
4022adantr 453 . . . . . . . . . . 11 Nat
41 eqid 2443 . . . . . . . . . . . . . . 15
42 relfunc 14097 . . . . . . . . . . . . . . . 16
436fucbas 14195 . . . . . . . . . . . . . . . . . 18
449, 43, 26funcf1 14101 . . . . . . . . . . . . . . . . 17
4544, 28ffvelrnd 5907 . . . . . . . . . . . . . . . 16
46 1st2ndbr 6432 . . . . . . . . . . . . . . . 16
4742, 45, 46sylancr 646 . . . . . . . . . . . . . . 15
4810, 41, 47funcf1 14101 . . . . . . . . . . . . . 14
49 eqidd 2444 . . . . . . . . . . . . . . 15
5018, 22setcbas 14271 . . . . . . . . . . . . . . 15
5149, 50feq23d 5623 . . . . . . . . . . . . . 14
5248, 51mpbird 225 . . . . . . . . . . . . 13
5352, 27ffvelrnd 5907 . . . . . . . . . . . 12
5453adantr 453 . . . . . . . . . . 11 Nat
55 yonedalem21.f . . . . . . . . . . . . . . . 16
56 1st2ndbr 6432 . . . . . . . . . . . . . . . 16
5742, 55, 56sylancr 646 . . . . . . . . . . . . . . 15
5810, 41, 57funcf1 14101 . . . . . . . . . . . . . 14
5949, 50feq23d 5623 . . . . . . . . . . . . . 14
6058, 59mpbird 225 . . . . . . . . . . . . 13
6160, 27ffvelrnd 5907 . . . . . . . . . . . 12
6261adantr 453 . . . . . . . . . . 11 Nat
63 yonedalem22.g . . . . . . . . . . . . . . . 16
64 1st2ndbr 6432 . . . . . . . . . . . . . . . 16
6542, 63, 64sylancr 646 . . . . . . . . . . . . . . 15
6610, 41, 65funcf1 14101 . . . . . . . . . . . . . 14
6766, 27ffvelrnd 5907 . . . . . . . . . . . . 13
6867, 50eleqtrrd 2520 . . . . . . . . . . . 12
6968adantr 453 . . . . . . . . . . 11 Nat
707, 33nat1st2nd 14186 . . . . . . . . . . . . 13 Nat Nat
71 eqid 2443 . . . . . . . . . . . . 13
727, 70, 10, 71, 37natcl 14188 . . . . . . . . . . . 12 Nat
7318, 40, 71, 54, 62elsetchom 14274 . . . . . . . . . . . 12 Nat
7472, 73mpbid 203 . . . . . . . . . . 11 Nat
757, 34nat1st2nd 14186 . . . . . . . . . . . . . 14 Nat
767, 75, 10, 71, 27natcl 14188 . . . . . . . . . . . . 13
7718, 22, 71, 61, 68elsetchom 14274 . . . . . . . . . . . . 13
7876, 77mpbid 203 . . . . . . . . . . . 12
7978adantr 453 . . . . . . . . . . 11 Nat
8018, 40, 11, 54, 62, 69, 74, 79setcco 14276 . . . . . . . . . 10 Nat comp
8139, 80eqtrd 2475 . . . . . . . . 9 Nat comp
8281oveq1d 6132 . . . . . . . 8 Nat comp comp comp
8344, 27ffvelrnd 5907 . . . . . . . . . . . . . 14
84 1st2ndbr 6432 . . . . . . . . . . . . . 14
8542, 83, 84sylancr 646 . . . . . . . . . . . . 13
8610, 41, 85funcf1 14101 . . . . . . . . . . . 12
8786, 27ffvelrnd 5907 . . . . . . . . . . 11
8887, 50eleqtrrd 2520 . . . . . . . . . 10
8988adantr 453 . . . . . . . . 9 Nat
907, 31nat1st2nd 14186 . . . . . . . . . . . 12 Nat
917, 90, 10, 71, 27natcl 14188 . . . . . . . . . . 11
9218, 22, 71, 88, 53elsetchom 14274 . . . . . . . . . . 11
9391, 92mpbid 203 . . . . . . . . . 10
9493adantr 453 . . . . . . . . 9 Nat
95 fco 5635 . . . . . . . . . 10
9679, 74, 95syl2anc 644 . . . . . . . . 9 Nat
9718, 40, 11, 89, 54, 69, 94, 96setcco 14276 . . . . . . . 8 Nat comp
9838, 82, 973eqtrd 2479 . . . . . . 7 Nat comp comp
9998fveq1d 5765 . . . . . 6 Nat comp comp
100 yoneda.1 . . . . . . . . . 10
1019, 13, 100, 17, 27catidcl 13945 . . . . . . . . 9
10216, 9, 17, 27, 13, 27yon11 14399 . . . . . . . . 9
103101, 102eleqtrrd 2520 . . . . . . . 8
104103adantr 453 . . . . . . 7 Nat
105 fvco3 5836 . . . . . . 7
10694, 104, 105syl2anc 644 . . . . . 6 Nat
10794, 104ffvelrnd 5907 . . . . . . . 8 Nat
108 fvco3 5836 . . . . . . . 8
10974, 107, 108syl2anc 644 . . . . . . 7 Nat
11017adantr 453 . . . . . . . . . . . 12 Nat
11128adantr 453 . . . . . . . . . . . 12 Nat
112 eqid 2443 . . . . . . . . . . . 12 comp comp
11330adantr 453 . . . . . . . . . . . 12 Nat
114101adantr 453 . . . . . . . . . . . 12 Nat
11516, 9, 110, 37, 13, 111, 112, 37, 113, 114yon2 14401 . . . . . . . . . . 11 Nat comp
1169, 13, 100, 110, 37, 112, 111, 113catrid 13947 . . . . . . . . . . 11 Nat comp
117115, 116eqtrd 2475 . . . . . . . . . 10 Nat
118117fveq2d 5767 . . . . . . . . 9 Nat
119 eqid 2443 . . . . . . . . . . . . . . 15
12010, 119, 71, 47, 28, 27funcf2 14103 . . . . . . . . . . . . . 14
12113, 8oppchom 13979 . . . . . . . . . . . . . . 15
12230, 121syl6eleqr 2534 . . . . . . . . . . . . . 14
123120, 122ffvelrnd 5907 . . . . . . . . . . . . 13
12452, 28ffvelrnd 5907 . . . . . . . . . . . . . 14
12518, 22, 71, 124, 53elsetchom 14274 . . . . . . . . . . . . 13
126123, 125mpbid 203 . . . . . . . . . . . 12
127126adantr 453 . . . . . . . . . . 11 Nat
1289, 13, 100, 17, 28catidcl 13945 . . . . . . . . . . . . 13
12916, 9, 17, 28, 13, 28yon11 14399 . . . . . . . . . . . . 13
130128, 129eleqtrrd 2520 . . . . . . . . . . . 12
131130adantr 453 . . . . . . . . . . 11 Nat
132 fvco3 5836 . . . . . . . . . . 11
133127, 131, 132syl2anc 644 . . . . . . . . . 10 Nat
134122adantr 453 . . . . . . . . . . . . 13 Nat
1357, 70, 10, 119, 11, 111, 37, 134nati 14190 . . . . . . . . . . . 12 Nat comp comp
136124adantr 453 . . . . . . . . . . . . 13 Nat
13718, 40, 11, 136, 54, 62, 127, 74setcco 14276 . . . . . . . . . . . 12 Nat comp
13860, 28ffvelrnd 5907 . . . . . . . . . . . . . 14
139138adantr 453 . . . . . . . . . . . . 13 Nat
1407, 70, 10, 71, 111natcl 14188 . . . . . . . . . . . . . 14 Nat
14118, 40, 71, 136, 139elsetchom 14274 . . . . . . . . . . . . . 14 Nat
142140, 141mpbid 203 . . . . . . . . . . . . 13 Nat
14310, 119, 71, 57, 28, 27funcf2 14103 . . . . . . . . . . . . . . . 16
144143, 122ffvelrnd 5907 . . . . . . . . . . . . . . 15
14518, 22, 71, 138, 61elsetchom 14274 . . . . . . . . . . . . . . 15
146144, 145mpbid 203 . . . . . . . . . . . . . 14
147146adantr 453 . . . . . . . . . . . . 13 Nat
14818, 40, 11, 136, 139, 62, 142, 147setcco 14276 . . . . . . . . . . . 12 Nat comp
149135, 137, 1483eqtr3d 2483 . . . . . . . . . . 11 Nat
150149fveq1d 5765 . . . . . . . . . 10 Nat
151128adantr 453 . . . . . . . . . . . . 13 Nat
15216, 9, 110, 111, 13, 111, 112, 37, 113, 151yon12 14400 . . . . . . . . . . . 12 Nat comp
1539, 13, 100, 110, 37, 112, 111, 113catlid 13946 . . . . . . . . . . . 12 Nat comp
154152, 153eqtrd 2475 . . . . . . . . . . 11 Nat
155154fveq2d 5767 . . . . . . . . . 10 Nat
156133, 150, 1553eqtr3d 2483 . . . . . . . . 9 Nat
157 fvco3 5836 . . . . . . . . . 10
158142, 131, 157syl2anc 644 . . . . . . . . 9 Nat
159118, 156, 1583eqtr2d 2481 . . . . . . . 8 Nat
160159fveq2d 5767 . . . . . . 7 Nat
161109, 160eqtrd 2475 . . . . . 6 Nat
16299, 106, 1613eqtrd 2479 . . . . 5 Nat comp comp
163162mpteq2dva 4326 . . . 4 Nat comp comp Nat
1645, 163syl5eq 2487 . . 3 Nat comp comp Nat
165 eqid 2443 . . . . . . . . . . 11 c c
166165, 43, 10xpcbas 14313 . . . . . . . . . 10 c
167 eqid 2443 . . . . . . . . . 10 c c
168 eqid 2443 . . . . . . . . . 10
169 relfunc 14097 . . . . . . . . . . 11 c
170 yoneda.t . . . . . . . . . . . . 13
171 yoneda.h . . . . . . . . . . . . 13 HomF
172 yoneda.r . . . . . . . . . . . . 13 c FuncCat
173 yoneda.e . . . . . . . . . . . . 13 evalF
174 yoneda.z . . . . . . . . . . . . 13 func tpos func F ⟨,⟩F F
17516, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20yonedalem1 14407 . . . . . . . . . . . 12 c c
176175simpld 447 . . . . . . . . . . 11 c
177 1st2ndbr 6432 . . . . . . . . . . 11 c c c
178169, 176, 177sylancr 646 . . . . . . . . . 10 c
179 opelxpi 4945 . . . . . . . . . . 11
18055, 28, 179syl2anc 644 . . . . . . . . . 10
181 opelxpi 4945 . . . . . . . . . . 11
18263, 27, 181syl2anc 644 . . . . . . . . . 10
183166, 167, 168, 178, 180, 182funcf2 14103 . . . . . . . . 9 c
184165, 43, 10, 14, 119, 55, 28, 63, 27, 167xpchom2 14321 . . . . . . . . . . 11 c Nat
185121xpeq2i 4934 . . . . . . . . . . 11 Nat Nat
186184, 185syl6eq 2491 . . . . . . . . . 10 c Nat
187 df-ov 6120 . . . . . . . . . . . . 13
188 df-ov 6120 . . . . . . . . . . . . 13
189187, 188oveq12i 6129 . . . . . . . . . . . 12
190189eqcomi 2447 . . . . . . . . . . 11
191190a1i 11 . . . . . . . . . 10
192186, 191feq23d 5623 . . . . . . . . 9 c Nat
193183, 192mpbid 203 . . . . . . . 8 Nat
194193, 34, 30fovrnd 6254 . . . . . . 7
195 eqid 2443 . . . . . . . . . . 11
196166, 195, 178funcf1 14101 . . . . . . . . . 10
197196, 55, 28fovrnd 6254 . . . . . . . . 9
198170, 19setcbas 14271 . . . . . . . . 9
199197, 198eleqtrrd 2520 . . . . . . . 8
200196, 63, 27fovrnd 6254 . . . . . . . . 9
201200, 198eleqtrrd 2520 . . . . . . . 8
202170, 19, 168, 199, 201elsetchom 14274 . . . . . . 7
203194, 202mpbid 203 . . . . . 6
20416, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20, 55, 28, 63, 27, 34, 30yonedalem22 14413 . . . . . . . 8
2058oppccat 13986 . . . . . . . . . . 11
20617, 205syl 16 . . . . . . . . . 10
20718setccat 14278 . . . . . . . . . . 11
20822, 207syl 16 . . . . . . . . . 10
2096, 206, 208fuccat 14205 . . . . . . . . 9
210171, 209, 43, 14, 45, 55, 83, 63, 12, 31, 34hof2val 14391 . . . . . . . 8 Nat comp comp
211204, 210eqtrd 2475 . . . . . . 7 Nat comp comp
21216, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20, 55, 28yonedalem21 14408 . . . . . . 7 Nat
21316, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20, 63, 27yonedalem21 14408 . . . . . . 7 Nat
214211, 212, 213feq123d 5618 . . . . . 6 Nat comp comp Nat Nat
215203, 214mpbid 203 . . . . 5 Nat comp comp Nat Nat
216 eqid 2443 . . . . . 6 Nat comp comp Nat comp comp
217216fmpt 5926 . . . . 5 Nat comp comp Nat Nat comp comp Nat Nat
218215, 217sylibr 205 . . . 4 Nat comp comp Nat
219 yonedalem3.m . . . . . 6 Nat
22016, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20, 63, 27, 219yonedalem3a 14409 . . . . 5 Nat
221220simpld 447 . . . 4 Nat
222 fveq1 5762 . . . . 5 comp comp comp comp
223222fveq1d 5765 . . . 4 comp comp comp comp
224218, 211, 221, 223fmptcof 5938 . . 3 Nat comp comp
225 eqid 2443 . . . . . . 7
226173, 206, 208, 10, 119, 11, 7, 55, 63, 28, 27, 225, 34, 122evlf2val 14354 . . . . . 6 comp
22718, 22, 11, 138, 61, 68, 146, 78setcco 14276 . . . . . 6 comp
228226, 227eqtrd 2475 . . . . 5
229228coeq1d 5069 . . . 4
23016, 9, 100, 8, 18, 170, 6, 171, 172, 173, 174, 17, 19, 23, 20, 55, 28, 219yonedalem3a 14409 . . . . . . . 8 Nat
231230simprd 451 . . . . . . 7
232230simpld 447 . . . . . . . 8 Nat
233173, 206, 208, 10, 55, 28evlf1 14355 . . . . . . . 8
234232, 212, 233feq123d 5618 . . . . . . 7 Nat Nat
235231, 234mpbid 203 . . . . . 6 Nat Nat
236 eqid 2443 . . . . . . 7 Nat Nat
237236fmpt 5926 . . . . . 6 Nat Nat Nat
238235, 237sylibr 205 . . . . 5 Nat
239 fcompt 5940 . . . . . 6
24078, 146, 239syl2anc 644 . . . . 5
241 fveq2 5763 . . . . . 6
242241fveq2d 5767 . . . . 5
243238, 232, 240, 242fmptcof 5938 . . . 4 Nat
244229, 243eqtrd 2475 . . 3 Nat
245164, 224, 2443eqtr4d 2485 . 2
246 eqid 2443 . . 3 comp comp
247175simprd 451 . . . . . . 7 c
248 1st2ndbr 6432 . . . . . . 7 c c c
249169, 247, 248sylancr 646 . . . . . 6 c
250166, 195, 249funcf1 14101 . . . . 5
251250, 63, 27fovrnd 6254 . . . 4
252251, 198eleqtrrd 2520 . . 3
253220simprd 451 . . 3
254170, 19, 246, 199, 201, 252, 203, 253setcco 14276 . 2 comp
255250, 55, 28fovrnd 6254 . . . 4
256255, 198eleqtrrd 2520 . . 3
257166, 167, 168, 249, 180, 182funcf2 14103 . . . . . 6 c
258 df-ov 6120 . . . . . . . . . 10
259 df-ov 6120 . . . . . . . . . 10
260258, 259oveq12i 6129 . . . . . . . . 9
261260eqcomi 2447 . . . . . . . 8
262261a1i 11 . . . . . . 7
263186, 262feq23d 5623 . . . . . 6 c Nat
264257, 263mpbid 203 . . . . 5 Nat
265264, 34, 30fovrnd 6254 . . . 4
266170, 19, 168, 256, 252elsetchom 14274 . . . 4
267265, 266mpbid 203 . . 3
268170, 19, 246, 199, 256, 252, 231, 267setcco 14276 . 2 comp
269245, 254, 2683eqtr4d 2485 1 comp comp
 Colors of variables: wff set class Syntax hints:   wi 4   wa 360   wceq 1654   wcel 1728  wral 2712  cvv 2965   cun 3307   wss 3309  cop 3846   class class class wbr 4243   cmpt 4297   cxp 4911   crn 4914   ccom 4917   wrel 4918  wf 5485  cfv 5489  (class class class)co 6117   cmpt2 6119  c1st 6383  c2nd 6384  tpos ctpos 6514  cbs 13507   chom 13578  compcco 13579  ccat 13927  ccid 13928   f chomf 13929  oppCatcoppc 13975   cfunc 14089   func ccofu 14091   Nat cnat 14176   FuncCat cfuc 14177  csetc 14268   c cxpc 14303   F c1stf 14304   F c2ndf 14305   ⟨,⟩F cprf 14306   evalF cevlf 14344  HomFchof 14383  Yoncyon 14384 This theorem is referenced by:  yonedalem3  14415 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-rep 4351  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736  ax-cnex 9084  ax-resscn 9085  ax-1cn 9086  ax-icn 9087  ax-addcl 9088  ax-addrcl 9089  ax-mulcl 9090  ax-mulrcl 9091  ax-mulcom 9092  ax-addass 9093  ax-mulass 9094  ax-distr 9095  ax-i2m1 9096  ax-1ne0 9097  ax-1rid 9098  ax-rnegex 9099  ax-rrecex 9100  ax-cnre 9101  ax-pre-lttri 9102  ax-pre-lttrn 9103  ax-pre-ltadd 9104  ax-pre-mulgt0 9105 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2717  df-rex 2718  df-reu 2719  df-rmo 2720  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-tp 3851  df-op 3852  df-uni 4045  df-int 4080  df-iun 4124  df-br 4244  df-opab 4298  df-mpt 4299  df-tr 4334  df-eprel 4529  df-id 4533  df-po 4538  df-so 4539  df-fr 4576  df-we 4578  df-ord 4619  df-on 4620  df-lim 4621  df-suc 4622  df-om 4881  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497  df-ov 6120  df-oprab 6121  df-mpt2 6122  df-1st 6385  df-2nd 6386  df-tpos 6515  df-riota 6585  df-recs 6669  df-rdg 6704  df-1o 6760  df-oadd 6764  df-er 6941  df-map 7056  df-pm 7057  df-ixp 7100  df-en 7146  df-dom 7147  df-sdom 7148  df-fin 7149  df-pnf 9160  df-mnf 9161  df-xr 9162  df-ltxr 9163  df-le 9164  df-sub 9331  df-neg 9332  df-nn 10039  df-2 10096  df-3 10097  df-4 10098  df-5 10099  df-6 10100  df-7 10101  df-8 10102  df-9 10103  df-10 10104  df-n0 10260  df-z 10321  df-dec 10421  df-uz 10527  df-fz 11082  df-struct 13509  df-ndx 13510  df-slot 13511  df-base 13512  df-sets 13513  df-ress 13514  df-hom 13591  df-cco 13592  df-cat 13931  df-cid 13932  df-homf 13933  df-comf 13934  df-oppc 13976  df-ssc 14048  df-resc 14049  df-subc 14050  df-func 14093  df-cofu 14095  df-nat 14178  df-fuc 14179  df-setc 14269  df-xpc 14307  df-1stf 14308  df-2ndf 14309  df-prf 14310  df-evlf 14348  df-curf 14349  df-hof 14385  df-yon 14386
 Copyright terms: Public domain W3C validator