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

Theorem yonedalem3b 16107
 Description: Lemma for yoneda 16111. (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 6257 . . . . . . . 8 comp comp
21oveq1d 6264 . . . . . . 7 comp comp comp comp
32fveq1d 5827 . . . . . 6 comp comp comp comp
43fveq1d 5827 . . . . 5 comp comp comp comp
54cbvmptv 4459 . . . 4 Nat comp comp Nat comp comp
6 yoneda.q . . . . . . . . 9 FuncCat
7 eqid 2428 . . . . . . . . 9 Nat Nat
8 yoneda.o . . . . . . . . . 10 oppCat
9 yoneda.b . . . . . . . . . 10
108, 9oppcbas 15566 . . . . . . . . 9
11 eqid 2428 . . . . . . . . 9 comp comp
12 eqid 2428 . . . . . . . . 9 comp comp
13 eqid 2428 . . . . . . . . . . . 12
146, 7fuchom 15809 . . . . . . . . . . . 12 Nat
15 relfunc 15710 . . . . . . . . . . . . 13
16 yoneda.y . . . . . . . . . . . . . 14 Yon
17 yoneda.c . . . . . . . . . . . . . 14
18 yoneda.s . . . . . . . . . . . . . 14
19 yoneda.w . . . . . . . . . . . . . . 15
20 yoneda.v . . . . . . . . . . . . . . . 16 f
2120unssbd 3587 . . . . . . . . . . . . . . 15
2219, 21ssexd 4514 . . . . . . . . . . . . . 14
23 yoneda.u . . . . . . . . . . . . . 14 f
2416, 17, 8, 18, 6, 22, 23yoncl 16090 . . . . . . . . . . . . 13
25 1st2ndbr 6800 . . . . . . . . . . . . 13
2615, 24, 25sylancr 667 . . . . . . . . . . . 12
27 yonedalem22.p . . . . . . . . . . . 12
28 yonedalem21.x . . . . . . . . . . . 12
299, 13, 14, 26, 27, 28funcf2 15716 . . . . . . . . . . 11 Nat
30 yonedalem22.k . . . . . . . . . . 11
3129, 30ffvelrnd 5982 . . . . . . . . . 10 Nat
3231adantr 466 . . . . . . . . 9 Nat Nat
33 simpr 462 . . . . . . . . . 10 Nat Nat
34 yonedalem22.a . . . . . . . . . . 11 Nat
3534adantr 466 . . . . . . . . . 10 Nat Nat
366, 7, 12, 33, 35fuccocl 15812 . . . . . . . . 9 Nat comp Nat
3727adantr 466 . . . . . . . . 9 Nat
386, 7, 10, 11, 12, 32, 36, 37fuccoval 15811 . . . . . . . 8 Nat comp comp comp comp
396, 7, 10, 11, 12, 33, 35, 37fuccoval 15811 . . . . . . . . . 10 Nat comp comp
4022adantr 466 . . . . . . . . . . 11 Nat
41 eqid 2428 . . . . . . . . . . . . . . 15
42 relfunc 15710 . . . . . . . . . . . . . . . 16
436fucbas 15808 . . . . . . . . . . . . . . . . . 18
449, 43, 26funcf1 15714 . . . . . . . . . . . . . . . . 17
4544, 28ffvelrnd 5982 . . . . . . . . . . . . . . . 16
46 1st2ndbr 6800 . . . . . . . . . . . . . . . 16
4742, 45, 46sylancr 667 . . . . . . . . . . . . . . 15
4810, 41, 47funcf1 15714 . . . . . . . . . . . . . 14
4918, 22setcbas 15916 . . . . . . . . . . . . . . 15
5049feq3d 5677 . . . . . . . . . . . . . 14
5148, 50mpbird 235 . . . . . . . . . . . . 13
5251, 27ffvelrnd 5982 . . . . . . . . . . . 12
5352adantr 466 . . . . . . . . . . 11 Nat
54 yonedalem21.f . . . . . . . . . . . . . . . 16
55 1st2ndbr 6800 . . . . . . . . . . . . . . . 16
5642, 54, 55sylancr 667 . . . . . . . . . . . . . . 15
5710, 41, 56funcf1 15714 . . . . . . . . . . . . . 14
5849feq3d 5677 . . . . . . . . . . . . . 14
5957, 58mpbird 235 . . . . . . . . . . . . 13
6059, 27ffvelrnd 5982 . . . . . . . . . . . 12
6160adantr 466 . . . . . . . . . . 11 Nat
62 yonedalem22.g . . . . . . . . . . . . . . . 16
63 1st2ndbr 6800 . . . . . . . . . . . . . . . 16
6442, 62, 63sylancr 667 . . . . . . . . . . . . . . 15
6510, 41, 64funcf1 15714 . . . . . . . . . . . . . 14
6665, 27ffvelrnd 5982 . . . . . . . . . . . . 13
6766, 49eleqtrrd 2509 . . . . . . . . . . . 12
6867adantr 466 . . . . . . . . . . 11 Nat
697, 33nat1st2nd 15799 . . . . . . . . . . . . 13 Nat Nat
70 eqid 2428 . . . . . . . . . . . . 13
717, 69, 10, 70, 37natcl 15801 . . . . . . . . . . . 12 Nat
7218, 40, 70, 53, 61elsetchom 15919 . . . . . . . . . . . 12 Nat
7371, 72mpbid 213 . . . . . . . . . . 11 Nat
747, 34nat1st2nd 15799 . . . . . . . . . . . . . 14 Nat
757, 74, 10, 70, 27natcl 15801 . . . . . . . . . . . . 13
7618, 22, 70, 60, 67elsetchom 15919 . . . . . . . . . . . . 13
7775, 76mpbid 213 . . . . . . . . . . . 12
7877adantr 466 . . . . . . . . . . 11 Nat
7918, 40, 11, 53, 61, 68, 73, 78setcco 15921 . . . . . . . . . 10 Nat comp
8039, 79eqtrd 2462 . . . . . . . . 9 Nat comp
8180oveq1d 6264 . . . . . . . 8 Nat comp comp comp
8244, 27ffvelrnd 5982 . . . . . . . . . . . . . 14
83 1st2ndbr 6800 . . . . . . . . . . . . . 14
8442, 82, 83sylancr 667 . . . . . . . . . . . . 13
8510, 41, 84funcf1 15714 . . . . . . . . . . . 12
8685, 27ffvelrnd 5982 . . . . . . . . . . 11
8786, 49eleqtrrd 2509 . . . . . . . . . 10
8887adantr 466 . . . . . . . . 9 Nat
897, 31nat1st2nd 15799 . . . . . . . . . . . 12 Nat
907, 89, 10, 70, 27natcl 15801 . . . . . . . . . . 11
9118, 22, 70, 87, 52elsetchom 15919 . . . . . . . . . . 11
9290, 91mpbid 213 . . . . . . . . . 10
9392adantr 466 . . . . . . . . 9 Nat
94 fco 5699 . . . . . . . . . 10
9578, 73, 94syl2anc 665 . . . . . . . . 9 Nat
9618, 40, 11, 88, 53, 68, 93, 95setcco 15921 . . . . . . . 8 Nat comp
9738, 81, 963eqtrd 2466 . . . . . . 7 Nat comp comp
9897fveq1d 5827 . . . . . 6 Nat comp comp
99 yoneda.1 . . . . . . . . . 10
1009, 13, 99, 17, 27catidcl 15531 . . . . . . . . 9
10116, 9, 17, 27, 13, 27yon11 16092 . . . . . . . . 9
102100, 101eleqtrrd 2509 . . . . . . . 8
103102adantr 466 . . . . . . 7 Nat
104 fvco3 5902 . . . . . . 7
10593, 103, 104syl2anc 665 . . . . . 6 Nat
10693, 103ffvelrnd 5982 . . . . . . . 8 Nat
107 fvco3 5902 . . . . . . . 8
10873, 106, 107syl2anc 665 . . . . . . 7 Nat
10917adantr 466 . . . . . . . . . . . 12 Nat
11028adantr 466 . . . . . . . . . . . 12 Nat
111 eqid 2428 . . . . . . . . . . . 12 comp comp
11230adantr 466 . . . . . . . . . . . 12 Nat
113100adantr 466 . . . . . . . . . . . 12 Nat
11416, 9, 109, 37, 13, 110, 111, 37, 112, 113yon2 16094 . . . . . . . . . . 11 Nat comp
1159, 13, 99, 109, 37, 111, 110, 112catrid 15533 . . . . . . . . . . 11 Nat comp
116114, 115eqtrd 2462 . . . . . . . . . 10 Nat
117116fveq2d 5829 . . . . . . . . 9 Nat
118 eqid 2428 . . . . . . . . . . . . . . 15
11910, 118, 70, 47, 28, 27funcf2 15716 . . . . . . . . . . . . . 14
12013, 8oppchom 15563 . . . . . . . . . . . . . . 15
12130, 120syl6eleqr 2517 . . . . . . . . . . . . . 14
122119, 121ffvelrnd 5982 . . . . . . . . . . . . 13
12351, 28ffvelrnd 5982 . . . . . . . . . . . . . 14
12418, 22, 70, 123, 52elsetchom 15919 . . . . . . . . . . . . 13
125122, 124mpbid 213 . . . . . . . . . . . 12
126125adantr 466 . . . . . . . . . . 11 Nat
1279, 13, 99, 17, 28catidcl 15531 . . . . . . . . . . . . 13
12816, 9, 17, 28, 13, 28yon11 16092 . . . . . . . . . . . . 13
129127, 128eleqtrrd 2509 . . . . . . . . . . . 12
130129adantr 466 . . . . . . . . . . 11 Nat
131 fvco3 5902 . . . . . . . . . . 11
132126, 130, 131syl2anc 665 . . . . . . . . . 10 Nat
133121adantr 466 . . . . . . . . . . . . 13 Nat
1347, 69, 10, 118, 11, 110, 37, 133nati 15803 . . . . . . . . . . . 12 Nat comp comp
135123adantr 466 . . . . . . . . . . . . 13 Nat
13618, 40, 11, 135, 53, 61, 126, 73setcco 15921 . . . . . . . . . . . 12 Nat comp
13759, 28ffvelrnd 5982 . . . . . . . . . . . . . 14
138137adantr 466 . . . . . . . . . . . . 13 Nat
1397, 69, 10, 70, 110natcl 15801 . . . . . . . . . . . . . 14 Nat
14018, 40, 70, 135, 138elsetchom 15919 . . . . . . . . . . . . . 14 Nat
141139, 140mpbid 213 . . . . . . . . . . . . 13 Nat
14210, 118, 70, 56, 28, 27funcf2 15716 . . . . . . . . . . . . . . . 16
143142, 121ffvelrnd 5982 . . . . . . . . . . . . . . 15
14418, 22, 70, 137, 60elsetchom 15919 . . . . . . . . . . . . . . 15
145143, 144mpbid 213 . . . . . . . . . . . . . 14
146145adantr 466 . . . . . . . . . . . . 13 Nat
14718, 40, 11, 135, 138, 61, 141, 146setcco 15921 . . . . . . . . . . . 12 Nat comp
148134, 136, 1473eqtr3d 2470 . . . . . . . . . . 11 Nat
149148fveq1d 5827 . . . . . . . . . 10 Nat
150127adantr 466 . . . . . . . . . . . . 13 Nat
15116, 9, 109, 110, 13, 110, 111, 37, 112, 150yon12 16093 . . . . . . . . . . . 12 Nat comp
1529, 13, 99, 109, 37, 111, 110, 112catlid 15532 . . . . . . . . . . . 12 Nat comp
153151, 152eqtrd 2462 . . . . . . . . . . 11 Nat
154153fveq2d 5829 . . . . . . . . . 10 Nat
155132, 149, 1543eqtr3d 2470 . . . . . . . . 9 Nat
156 fvco3 5902 . . . . . . . . . 10
157141, 130, 156syl2anc 665 . . . . . . . . 9 Nat
158117, 155, 1573eqtr2d 2468 . . . . . . . 8 Nat
159158fveq2d 5829 . . . . . . 7 Nat
160108, 159eqtrd 2462 . . . . . 6 Nat
16198, 105, 1603eqtrd 2466 . . . . 5 Nat comp comp
162161mpteq2dva 4453 . . . 4 Nat comp comp Nat
1635, 162syl5eq 2474 . . 3 Nat comp comp Nat
164 eqid 2428 . . . . . . . . . . 11 c c
165164, 43, 10xpcbas 16006 . . . . . . . . . 10 c
166 eqid 2428 . . . . . . . . . 10 c c
167 eqid 2428 . . . . . . . . . 10
168 relfunc 15710 . . . . . . . . . . 11 c
169 yoneda.t . . . . . . . . . . . . 13
170 yoneda.h . . . . . . . . . . . . 13 HomF
171 yoneda.r . . . . . . . . . . . . 13 c FuncCat
172 yoneda.e . . . . . . . . . . . . 13 evalF
173 yoneda.z . . . . . . . . . . . . 13 func tpos func F ⟨,⟩F F
17416, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20yonedalem1 16100 . . . . . . . . . . . 12 c c
175174simpld 460 . . . . . . . . . . 11 c
176 1st2ndbr 6800 . . . . . . . . . . 11 c c c
177168, 175, 176sylancr 667 . . . . . . . . . 10 c
178 opelxpi 4828 . . . . . . . . . . 11
17954, 28, 178syl2anc 665 . . . . . . . . . 10
180 opelxpi 4828 . . . . . . . . . . 11
18162, 27, 180syl2anc 665 . . . . . . . . . 10
182165, 166, 167, 177, 179, 181funcf2 15716 . . . . . . . . 9 c
183164, 43, 10, 14, 118, 54, 28, 62, 27, 166xpchom2 16014 . . . . . . . . . . 11 c Nat
184120xpeq2i 4817 . . . . . . . . . . 11 Nat Nat
185183, 184syl6eq 2478 . . . . . . . . . 10 c Nat
186 df-ov 6252 . . . . . . . . . . . . 13
187 df-ov 6252 . . . . . . . . . . . . 13
188186, 187oveq12i 6261 . . . . . . . . . . . 12
189188eqcomi 2437 . . . . . . . . . . 11
190189a1i 11 . . . . . . . . . 10
191185, 190feq23d 5684 . . . . . . . . 9 c Nat
192182, 191mpbid 213 . . . . . . . 8 Nat
193192, 34, 30fovrnd 6399 . . . . . . 7
194 eqid 2428 . . . . . . . . . . 11
195165, 194, 177funcf1 15714 . . . . . . . . . 10
196195, 54, 28fovrnd 6399 . . . . . . . . 9
197169, 19setcbas 15916 . . . . . . . . 9
198196, 197eleqtrrd 2509 . . . . . . . 8
199195, 62, 27fovrnd 6399 . . . . . . . . 9
200199, 197eleqtrrd 2509 . . . . . . . 8
201169, 19, 167, 198, 200elsetchom 15919 . . . . . . 7
202193, 201mpbid 213 . . . . . 6
20316, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 62, 27, 34, 30yonedalem22 16106 . . . . . . . 8
2048oppccat 15570 . . . . . . . . . . 11
20517, 204syl 17 . . . . . . . . . 10
20618setccat 15923 . . . . . . . . . . 11
20722, 206syl 17 . . . . . . . . . 10
2086, 205, 207fuccat 15818 . . . . . . . . 9
209170, 208, 43, 14, 45, 54, 82, 62, 12, 31, 34hof2val 16084 . . . . . . . 8 Nat comp comp
210203, 209eqtrd 2462 . . . . . . 7 Nat comp comp
21116, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28yonedalem21 16101 . . . . . . 7 Nat
21216, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27yonedalem21 16101 . . . . . . 7 Nat
213210, 211, 212feq123d 5679 . . . . . 6 Nat comp comp Nat Nat
214202, 213mpbid 213 . . . . 5 Nat comp comp Nat Nat
215 eqid 2428 . . . . . 6 Nat comp comp Nat comp comp
216215fmpt 6002 . . . . 5 Nat comp comp Nat Nat comp comp Nat Nat
217214, 216sylibr 215 . . . 4 Nat comp comp Nat
218 yonedalem3.m . . . . . 6 Nat
21916, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27, 218yonedalem3a 16102 . . . . 5 Nat
220219simpld 460 . . . 4 Nat
221 fveq1 5824 . . . . 5 comp comp comp comp
222221fveq1d 5827 . . . 4 comp comp comp comp
223217, 210, 220, 222fmptcof 6016 . . 3 Nat comp comp
224 eqid 2428 . . . . . . 7
225172, 205, 207, 10, 118, 11, 7, 54, 62, 28, 27, 224, 34, 121evlf2val 16047 . . . . . 6 comp
22618, 22, 11, 137, 60, 67, 145, 77setcco 15921 . . . . . 6 comp
227225, 226eqtrd 2462 . . . . 5
228227coeq1d 4958 . . . 4
22916, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 218yonedalem3a 16102 . . . . . . . 8 Nat
230229simprd 464 . . . . . . 7
231229simpld 460 . . . . . . . 8 Nat
232172, 205, 207, 10, 54, 28evlf1 16048 . . . . . . . 8
233231, 211, 232feq123d 5679 . . . . . . 7 Nat Nat
234230, 233mpbid 213 . . . . . 6 Nat Nat
235 eqid 2428 . . . . . . 7 Nat Nat
236235fmpt 6002 . . . . . 6 Nat Nat Nat
237234, 236sylibr 215 . . . . 5 Nat
238 fcompt 6018 . . . . . 6
23977, 145, 238syl2anc 665 . . . . 5
240 fveq2 5825 . . . . . 6
241240fveq2d 5829 . . . . 5
242237, 231, 239, 241fmptcof 6016 . . . 4 Nat
243228, 242eqtrd 2462 . . 3 Nat
244163, 223, 2433eqtr4d 2472 . 2
245 eqid 2428 . . 3 comp comp
246174simprd 464 . . . . . . 7 c
247 1st2ndbr 6800 . . . . . . 7 c c c
248168, 246, 247sylancr 667 . . . . . 6 c
249165, 194, 248funcf1 15714 . . . . 5
250249, 62, 27fovrnd 6399 . . . 4
251250, 197eleqtrrd 2509 . . 3
252219simprd 464 . . 3
253169, 19, 245, 198, 200, 251, 202, 252setcco 15921 . 2 comp
254249, 54, 28fovrnd 6399 . . . 4
255254, 197eleqtrrd 2509 . . 3
256165, 166, 167, 248, 179, 181funcf2 15716 . . . . . 6 c
257 df-ov 6252 . . . . . . . . . 10
258 df-ov 6252 . . . . . . . . . 10
259257, 258oveq12i 6261 . . . . . . . . 9
260259eqcomi 2437 . . . . . . . 8
261260a1i 11 . . . . . . 7
262185, 261feq23d 5684 . . . . . 6 c Nat
263256, 262mpbid 213 . . . . 5 Nat
264263, 34, 30fovrnd 6399 . . . 4
265169, 19, 167, 255, 251elsetchom 15919 . . . 4
266264, 265mpbid 213 . . 3
267169, 19, 245, 198, 255, 251, 230, 266setcco 15921 . 2 comp
268244, 253, 2673eqtr4d 2472 1 comp comp
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   wceq 1437   wcel 1872  wral 2714  cvv 3022   cun 3377   wss 3379  cop 3947   class class class wbr 4366   cmpt 4425   cxp 4794   crn 4797   ccom 4800   wrel 4801  wf 5540  cfv 5544  (class class class)co 6249   cmpt2 6251  c1st 6749  c2nd 6750  tpos ctpos 6927  cbs 15064   chom 15144  compcco 15145  ccat 15513  ccid 15514   f chomf 15515  oppCatcoppc 15559   cfunc 15702   func ccofu 15704   Nat cnat 15789   FuncCat cfuc 15790  csetc 15913   c cxpc 15996   F c1stf 15997   F c2ndf 15998   ⟨,⟩F cprf 15999   evalF cevlf 16037  HomFchof 16076  Yoncyon 16077 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-tpos 6928  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-oadd 7141  df-er 7318  df-map 7429  df-pm 7430  df-ixp 7478  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-nn 10561  df-2 10619  df-3 10620  df-4 10621  df-5 10622  df-6 10623  df-7 10624  df-8 10625  df-9 10626  df-10 10627  df-n0 10821  df-z 10889  df-dec 11003  df-uz 11111  df-fz 11736  df-struct 15066  df-ndx 15067  df-slot 15068  df-base 15069  df-sets 15070  df-ress 15071  df-hom 15157  df-cco 15158  df-cat 15517  df-cid 15518  df-homf 15519  df-comf 15520  df-oppc 15560  df-ssc 15658  df-resc 15659  df-subc 15660  df-func 15706  df-cofu 15708  df-nat 15791  df-fuc 15792  df-setc 15914  df-xpc 16000  df-1stf 16001  df-2ndf 16002  df-prf 16003  df-evlf 16041  df-curf 16042  df-hof 16078  df-yon 16079 This theorem is referenced by:  yonedalem3  16108
 Copyright terms: Public domain W3C validator