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

Theorem cantnflem1 7601
 Description: Lemma for cantnf 7605. This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct are -related as or , and WLOG assuming that , we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015.)
Hypotheses
Ref Expression
cantnfs.1 CNF
cantnfs.2
cantnfs.3
oemapval.t
oemapval.3
oemapval.4
oemapvali.5
oemapvali.6
cantnflem1.o OrdIso
cantnflem1.h seq𝜔
Assertion
Ref Expression
cantnflem1 CNF CNF
Distinct variable groups:   ,,,,,,   ,,,,,,   ,,   ,,,,,   ,,,,,   ,,,,,,   ,,   ,,,,,   ,,,,   ,,,,,   ,   ,
Allowed substitution hints:   ()   ()   (,,,)   (,,,)   ()   ()

Proof of Theorem cantnflem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 oemapval.3 . . . . . . . 8
2 cantnfs.1 . . . . . . . . 9 CNF
3 cantnfs.2 . . . . . . . . 9
4 cantnfs.3 . . . . . . . . 9
52, 3, 4cantnfs 7577 . . . . . . . 8
61, 5mpbid 202 . . . . . . 7
76simpld 446 . . . . . 6
87feqmptd 5738 . . . . 5
9 eqeq2 2413 . . . . . . 7
10 eqeq2 2413 . . . . . . 7
11 eqidd 2405 . . . . . . 7
12 onss 4730 . . . . . . . . . . . . 13
134, 12syl 16 . . . . . . . . . . . 12
1413sselda 3308 . . . . . . . . . . 11
15 cnvimass 5183 . . . . . . . . . . . . . . 15
16 oemapval.4 . . . . . . . . . . . . . . . . . 18
172, 3, 4cantnfs 7577 . . . . . . . . . . . . . . . . . 18
1816, 17mpbid 202 . . . . . . . . . . . . . . . . 17
1918simpld 446 . . . . . . . . . . . . . . . 16
20 fdm 5554 . . . . . . . . . . . . . . . 16
2119, 20syl 16 . . . . . . . . . . . . . . 15
2215, 21syl5sseq 3356 . . . . . . . . . . . . . 14
23 cnvexg 5364 . . . . . . . . . . . . . . . . . . 19
2416, 23syl 16 . . . . . . . . . . . . . . . . . 18
25 imaexg 5176 . . . . . . . . . . . . . . . . . 18
26 cantnflem1.o . . . . . . . . . . . . . . . . . . 19 OrdIso
2726oion 7461 . . . . . . . . . . . . . . . . . 18
2824, 25, 273syl 19 . . . . . . . . . . . . . . . . 17
29 uniexg 4665 . . . . . . . . . . . . . . . . 17
30 sucidg 4619 . . . . . . . . . . . . . . . . 17
3128, 29, 303syl 19 . . . . . . . . . . . . . . . 16
32 oemapval.t . . . . . . . . . . . . . . . . . . . . . 22
33 oemapvali.5 . . . . . . . . . . . . . . . . . . . . . 22
34 oemapvali.6 . . . . . . . . . . . . . . . . . . . . . 22
352, 3, 4, 32, 1, 16, 33, 34cantnflem1a 7597 . . . . . . . . . . . . . . . . . . . . 21
36 n0i 3593 . . . . . . . . . . . . . . . . . . . . 21
3735, 36syl 16 . . . . . . . . . . . . . . . . . . . 20
384, 22ssexd 4310 . . . . . . . . . . . . . . . . . . . . . 22
392, 3, 4, 26, 16cantnfcl 7578 . . . . . . . . . . . . . . . . . . . . . . 23
4039simpld 446 . . . . . . . . . . . . . . . . . . . . . 22
4126oien 7463 . . . . . . . . . . . . . . . . . . . . . 22
4238, 40, 41syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
43 breq1 4175 . . . . . . . . . . . . . . . . . . . . . 22
44 ensymb 7114 . . . . . . . . . . . . . . . . . . . . . . 23
45 en0 7129 . . . . . . . . . . . . . . . . . . . . . . 23
4644, 45bitri 241 . . . . . . . . . . . . . . . . . . . . . 22
4743, 46syl6bb 253 . . . . . . . . . . . . . . . . . . . . 21
4842, 47syl5ibcom 212 . . . . . . . . . . . . . . . . . . . 20
4937, 48mtod 170 . . . . . . . . . . . . . . . . . . 19
5039simprd 450 . . . . . . . . . . . . . . . . . . . 20
51 nnlim 4817 . . . . . . . . . . . . . . . . . . . 20
5250, 51syl 16 . . . . . . . . . . . . . . . . . . 19
53 ioran 477 . . . . . . . . . . . . . . . . . . 19
5449, 52, 53sylanbrc 646 . . . . . . . . . . . . . . . . . 18
5526oicl 7454 . . . . . . . . . . . . . . . . . . 19
56 unizlim 4657 . . . . . . . . . . . . . . . . . . 19
5755, 56mp1i 12 . . . . . . . . . . . . . . . . . 18
5854, 57mtbird 293 . . . . . . . . . . . . . . . . 17
59 orduniorsuc 4769 . . . . . . . . . . . . . . . . . . 19
6055, 59mp1i 12 . . . . . . . . . . . . . . . . . 18
6160ord 367 . . . . . . . . . . . . . . . . 17
6258, 61mpd 15 . . . . . . . . . . . . . . . 16
6331, 62eleqtrrd 2481 . . . . . . . . . . . . . . 15
6426oif 7455 . . . . . . . . . . . . . . . 16
6564ffvelrni 5828 . . . . . . . . . . . . . . 15
6663, 65syl 16 . . . . . . . . . . . . . 14
6722, 66sseldd 3309 . . . . . . . . . . . . 13
68 onelon 4566 . . . . . . . . . . . . 13
694, 67, 68syl2anc 643 . . . . . . . . . . . 12
7069adantr 452 . . . . . . . . . . 11
71 ontri1 4575 . . . . . . . . . . 11
7214, 70, 71syl2anc 643 . . . . . . . . . 10
7372con2bid 320 . . . . . . . . 9
74 simprl 733 . . . . . . . . . . . 12
752, 3, 4, 32, 1, 16, 33, 34oemapvali 7596 . . . . . . . . . . . . . 14
7675simp3d 971 . . . . . . . . . . . . 13
7776adantr 452 . . . . . . . . . . . 12
7826oiiso 7462 . . . . . . . . . . . . . . . . . . . . . 22
7938, 40, 78syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
80 isof1o 6004 . . . . . . . . . . . . . . . . . . . . 21
8179, 80syl 16 . . . . . . . . . . . . . . . . . . . 20
82 f1ocnv 5646 . . . . . . . . . . . . . . . . . . . 20
83 f1of 5633 . . . . . . . . . . . . . . . . . . . 20
8481, 82, 833syl 19 . . . . . . . . . . . . . . . . . . 19
8584, 35ffvelrnd 5830 . . . . . . . . . . . . . . . . . 18
86 elssuni 4003 . . . . . . . . . . . . . . . . . 18
8785, 86syl 16 . . . . . . . . . . . . . . . . 17
88 ordelon 4565 . . . . . . . . . . . . . . . . . . . 20
8955, 85, 88sylancr 645 . . . . . . . . . . . . . . . . . . 19
90 eloni 4551 . . . . . . . . . . . . . . . . . . 19
9189, 90syl 16 . . . . . . . . . . . . . . . . . 18
92 orduni 4733 . . . . . . . . . . . . . . . . . . 19
9355, 92ax-mp 8 . . . . . . . . . . . . . . . . . 18
94 ordtri1 4574 . . . . . . . . . . . . . . . . . 18
9591, 93, 94sylancl 644 . . . . . . . . . . . . . . . . 17
9687, 95mpbid 202 . . . . . . . . . . . . . . . 16
97 isorel 6005 . . . . . . . . . . . . . . . . . . 19
9879, 63, 85, 97syl12anc 1182 . . . . . . . . . . . . . . . . . 18
99 fvex 5701 . . . . . . . . . . . . . . . . . . 19
10099epelc 4456 . . . . . . . . . . . . . . . . . 18
101 fvex 5701 . . . . . . . . . . . . . . . . . . 19
102101epelc 4456 . . . . . . . . . . . . . . . . . 18
10398, 100, 1023bitr3g 279 . . . . . . . . . . . . . . . . 17
104 f1ocnvfv2 5974 . . . . . . . . . . . . . . . . . . 19
10581, 35, 104syl2anc 643 . . . . . . . . . . . . . . . . . 18
106105eleq2d 2471 . . . . . . . . . . . . . . . . 17
107103, 106bitrd 245 . . . . . . . . . . . . . . . 16
10896, 107mtbid 292 . . . . . . . . . . . . . . 15
10975simp1d 969 . . . . . . . . . . . . . . . . 17
110 onelon 4566 . . . . . . . . . . . . . . . . 17
1114, 109, 110syl2anc 643 . . . . . . . . . . . . . . . 16
112 ontri1 4575 . . . . . . . . . . . . . . . 16
113111, 69, 112syl2anc 643 . . . . . . . . . . . . . . 15
114108, 113mpbird 224 . . . . . . . . . . . . . 14
115114adantr 452 . . . . . . . . . . . . 13
116 simprr 734 . . . . . . . . . . . . 13
117111adantr 452 . . . . . . . . . . . . . 14
11814adantrr 698 . . . . . . . . . . . . . 14
119 ontr2 4588 . . . . . . . . . . . . . 14
120117, 118, 119syl2anc 643 . . . . . . . . . . . . 13
121115, 116, 120mp2and 661 . . . . . . . . . . . 12
122 eleq2 2465 . . . . . . . . . . . . . 14
123 fveq2 5687 . . . . . . . . . . . . . . 15
124 fveq2 5687 . . . . . . . . . . . . . . 15
125123, 124eqeq12d 2418 . . . . . . . . . . . . . 14
126122, 125imbi12d 312 . . . . . . . . . . . . 13
127126rspcv 3008 . . . . . . . . . . . 12
12874, 77, 121, 127syl3c 59 . . . . . . . . . . 11
129116adantr 452 . . . . . . . . . . . . . . 15
13079ad2antrr 707 . . . . . . . . . . . . . . . . . 18
13163ad2antrr 707 . . . . . . . . . . . . . . . . . 18
13284ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
133 ffvelrn 5827 . . . . . . . . . . . . . . . . . . 19
134132, 133sylancom 649 . . . . . . . . . . . . . . . . . 18
135 isorel 6005 . . . . . . . . . . . . . . . . . 18
136130, 131, 134, 135syl12anc 1182 . . . . . . . . . . . . . . . . 17
137 fvex 5701 . . . . . . . . . . . . . . . . . 18
138137epelc 4456 . . . . . . . . . . . . . . . . 17
139 fvex 5701 . . . . . . . . . . . . . . . . . 18
140139epelc 4456 . . . . . . . . . . . . . . . . 17
141136, 138, 1403bitr3g 279 . . . . . . . . . . . . . . . 16
14281ad2antrr 707 . . . . . . . . . . . . . . . . . 18
143 f1ocnvfv2 5974 . . . . . . . . . . . . . . . . . 18
144142, 143sylancom 649 . . . . . . . . . . . . . . . . 17
145144eleq2d 2471 . . . . . . . . . . . . . . . 16
146141, 145bitrd 245 . . . . . . . . . . . . . . 15
147129, 146mpbird 224 . . . . . . . . . . . . . 14
148 elssuni 4003 . . . . . . . . . . . . . . . 16
149134, 148syl 16 . . . . . . . . . . . . . . 15
150 ordelon 4565 . . . . . . . . . . . . . . . . . 18
15155, 134, 150sylancr 645 . . . . . . . . . . . . . . . . 17
152 eloni 4551 . . . . . . . . . . . . . . . . 17
153151, 152syl 16 . . . . . . . . . . . . . . . 16
154 ordtri1 4574 . . . . . . . . . . . . . . . 16
155153, 93, 154sylancl 644 . . . . . . . . . . . . . . 15
156149, 155mpbid 202 . . . . . . . . . . . . . 14
157147, 156pm2.65da 560 . . . . . . . . . . . . 13
15874, 157eldifd 3291 . . . . . . . . . . . 12
159 df1o2 6695 . . . . . . . . . . . . . . . 16
160159difeq2i 3422 . . . . . . . . . . . . . . 15
161160imaeq2i 5160 . . . . . . . . . . . . . 14
162 eqimss2 3361 . . . . . . . . . . . . . 14
163161, 162mp1i 12 . . . . . . . . . . . . 13
16419, 163suppssr 5823 . . . . . . . . . . . 12
165158, 164syldan 457 . . . . . . . . . . 11
166128, 165eqtrd 2436 . . . . . . . . . 10
167166expr 599 . . . . . . . . 9
16873, 167sylbird 227 . . . . . . . 8
169168imp 419 . . . . . . 7
1709, 10, 11, 169ifbothda 3729 . . . . . 6
171170mpteq2dva 4255 . . . . 5
1728, 171eqtrd 2436 . . . 4
173172fveq2d 5691 . . 3 CNF CNF
17462, 50eqeltrrd 2479 . . . . . 6
175 peano2b 4820 . . . . . 6
176174, 175sylibr 204 . . . . 5
177 eleq1 2464 . . . . . . . . 9
178 sseq2 3330 . . . . . . . . 9
179177, 178anbi12d 692 . . . . . . . 8
180 fveq2 5687 . . . . . . . . . . . . 13
181180sseq2d 3336 . . . . . . . . . . . 12
182181ifbid 3717 . . . . . . . . . . 11
183182mpteq2dv 4256 . . . . . . . . . 10
184183fveq2d 5691 . . . . . . . . 9 CNF CNF
185 suceq 4606 . . . . . . . . . 10
186185fveq2d 5691 . . . . . . . . 9
187184, 186eleq12d 2472 . . . . . . . 8 CNF CNF
188179, 187imbi12d 312 . . . . . . 7 CNF CNF
189188imbi2d 308 . . . . . 6 CNF CNF
190 eleq1 2464 . . . . . . . . 9
191 sseq2 3330 . . . . . . . . 9
192190, 191anbi12d 692 . . . . . . . 8
193 fveq2 5687 . . . . . . . . . . . . 13
194193sseq2d 3336 . . . . . . . . . . . 12
195194ifbid 3717 . . . . . . . . . . 11
196195mpteq2dv 4256 . . . . . . . . . 10
197196fveq2d 5691 . . . . . . . . 9 CNF CNF
198 suceq 4606 . . . . . . . . . 10
199198fveq2d 5691 . . . . . . . . 9
200197, 199eleq12d 2472 . . . . . . . 8 CNF CNF
201192, 200imbi12d 312 . . . . . . 7 CNF CNF
202 eleq1 2464 . . . . . . . . 9
203 sseq2 3330 . . . . . . . . 9
204202, 203anbi12d 692 . . . . . . . 8
205 fveq2 5687 . . . . . . . . . . . . 13
206205sseq2d 3336 . . . . . . . . . . . 12
207206ifbid 3717 . . . . . . . . . . 11
208207mpteq2dv 4256 . . . . . . . . . 10
209208fveq2d 5691 . . . . . . . . 9 CNF CNF
210 suceq 4606 . . . . . . . . . 10
211210fveq2d 5691 . . . . . . . . 9
212209, 211eleq12d 2472 . . . . . . . 8 CNF CNF
213204, 212imbi12d 312 . . . . . . 7 CNF CNF
214 eleq1 2464 . . . . . . . . 9
215 sseq2 3330 . . . . . . . . 9
216214, 215anbi12d 692 . . . . . . . 8
217 fveq2 5687 . . . . . . . . . . . . 13
218217sseq2d 3336 . . . . . . . . . . . 12
219218ifbid 3717 . . . . . . . . . . 11
220219mpteq2dv 4256 . . . . . . . . . 10
221220fveq2d 5691 . . . . . . . . 9 CNF CNF
222 suceq 4606 . . . . . . . . . 10
223222fveq2d 5691 . . . . . . . . 9
224221, 223eleq12d 2472 . . . . . . . 8 CNF CNF
225216, 224imbi12d 312 . . . . . . 7 CNF CNF
226105sseq2d 3336 . . . . . . . . . . . 12
227226ifbid 3717 . . . . . . . . . . 11
228227mpteq2dv 4256 . . . . . . . . . 10
229228fveq2d 5691 . . . . . . . . 9 CNF CNF
230 cantnflem1.h . . . . . . . . . 10 seq𝜔
2312, 3, 4, 32, 1, 16, 33, 34, 26, 230cantnflem1d 7600 . . . . . . . . 9 CNF
232229, 231eqeltrd 2478 . . . . . . . 8 CNF
233 ss0 3618 . . . . . . . . . . . . . . 15
234233fveq2d 5691 . . . . . . . . . . . . . 14
235234sseq2d 3336 . . . . . . . . . . . . 13
236235ifbid 3717 . . . . . . . . . . . 12
237236mpteq2dv 4256 . . . . . . . . . . 11
238237fveq2d 5691 . . . . . . . . . 10 CNF CNF
239 suceq 4606 . . . . . . . . . . . 12
240233, 239syl 16 . . . . . . . . . . 11
241240fveq2d 5691 . . . . . . . . . 10
242238, 241eleq12d 2472 . . . . . . . . 9 CNF CNF
243242adantl 453 . . . . . . . 8 CNF CNF
244232, 243syl5ibcom 212 . . . . . . 7 CNF
24589adantr 452 . . . . . . . . . . . 12
24655a1i 11 . . . . . . . . . . . . 13
247 ordelon 4565 . . . . . . . . . . . . 13
248246, 247sylan 458 . . . . . . . . . . . 12
249 onsseleq 4582 . . . . . . . . . . . 12
250245, 248, 249syl2anc 643 . . . . . . . . . . 11
251 sucelon 4756 . . . . . . . . . . . . . . . 16
252248, 251sylibr 204 . . . . . . . . . . . . . . 15
253 eloni 4551 . . . . . . . . . . . . . . 15
254252, 253syl 16 . . . . . . . . . . . . . 14
255 ordsssuc 4627 . . . . . . . . . . . . . 14
256245, 254, 255syl2anc 643 . . . . . . . . . . . . 13
257 ordtr 4555 . . . . . . . . . . . . . . . . . 18
25855, 257mp1i 12 . . . . . . . . . . . . . . . . 17
259 simprl 733 . . . . . . . . . . . . . . . . 17
260 trsuc 4625 . . . . . . . . . . . . . . . . 17
261258, 259, 260syl2anc 643 . . . . . . . . . . . . . . . 16
262 simprr 734 . . . . . . . . . . . . . . . 16
263261, 262jca 519 . . . . . . . . . . . . . . 15
2643adantr 452 . . . . . . . . . . . . . . . . . . . 20
2654adantr 452 . . . . . . . . . . . . . . . . . . . 20
266 oecl 6740 . . . . . . . . . . . . . . . . . . . 20
267264, 265, 266syl2anc 643 . . . . . . . . . . . . . . . . . . 19
2682, 264, 265cantnff 7585 . . . . . . . . . . . . . . . . . . . 20 CNF
2697ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . . . . . 24
27019, 109ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
271 ne0i 3594 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
272270, 271syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
273 on0eln0 4596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2743, 273syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
275272, 274mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . 25
276275adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24
277 ifcl 3735 . . . . . . . . . . . . . . . . . . . . . . . 24
278269, 276, 277syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
279 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . 23
280278, 279fmptd 5852 . . . . . . . . . . . . . . . . . . . . . 22
2816simprd 450 . . . . . . . . . . . . . . . . . . . . . . 23
282160imaeq2i 5160 . . . . . . . . . . . . . . . . . . . . . . . 24
283160imaeq2i 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
284 eqimss2 3361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
285283, 284mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2867, 285suppssr 5823 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
287286ifeq1d 3713 . . . . . . . . . . . . . . . . . . . . . . . . . 26
288 ifid 3731 . . . . . . . . . . . . . . . . . . . . . . . . . 26
289287, 288syl6eq 2452 . . . . . . . . . . . . . . . . . . . . . . . . 25
290289suppss2 6259 . . . . . . . . . . . . . . . . . . . . . . . 24
291282, 290syl5eqss 3352 . . . . . . . . . . . . . . . . . . . . . . 23
292 ssfi 7288 . . . . . . . . . . . . . . . . . . . . . . 23
293281, 291, 292syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
2942, 3, 4cantnfs 7577 . . . . . . . . . . . . . . . . . . . . . 22
295280, 293, 294mpbir2and 889 . . . . . . . . . . . . . . . . . . . . 21
296295adantr 452 . . . . . . . . . . . . . . . . . . . 20
297268, 296ffvelrnd 5830 . . . . . . . . . . . . . . . . . . 19 CNF
298 onelon 4566 . . . . . . . . . . . . . . . . . . 19 CNF CNF
299267, 297, 298syl2anc 643 . . . . . . . . . . . . . . . . . 18 CNF
30050adantr 452 . . . . . . . . . . . . . . . . . . . 20
301 elnn 4814 . . . . . . . . . . . . . . . . . . . 20
302259, 300, 301syl2anc 643 . . . . . . . . . . . . . . . . . . 19
303230cantnfvalf 7576 . . . . . . . . . . . . . . . . . . . 20
304303ffvelrni 5828 . . . . . . . . . . . . . . . . . . 19
305302, 304syl 16 . . . . . . . . . . . . . . . . . 18
30622adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
30764ffvelrni 5828 . . . . . . . . . . . . . . . . . . . . . . 23
308259, 307syl 16 . . . . . . . . . . . . . . . . . . . . . 22
309306, 308sseldd 3309 . . . . . . . . . . . . . . . . . . . . 21
310 onelon 4566 . . . . . . . . . . . . . . . . . . . . 21
311265, 309, 310syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
312 oecl 6740 . . . . . . . . . . . . . . . . . . . 20
313264, 311, 312syl2anc 643 . . . . . . . . . . . . . . . . . . 19
3147adantr 452 . . . . . . . . . . . . . . . . . . . . 21
315314, 309ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . 20
316 onelon 4566 . . . . . . . . . . . . . . . . . . . 20
317264, 315, 316syl2anc 643 . . . . . . . . . . . . . . . . . . 19
318 omcl 6739 . . . . . . . . . . . . . . . . . . 19
319313, 317, 318syl2anc 643 . . . . . . . . . . . . . . . . . 18
320 oaord 6749 . . . . . . . . . . . . . . . . . 18 CNF CNF CNF
321299, 305, 319, 320syl3anc 1184 . . . . . . . . . . . . . . . . 17 CNF CNF
322 ifeq1 3703 . . . . . . . . . . . . . . . . . . . . . . . 24
323 ifid 3731 . . . . . . . . . . . . . . . . . . . . . . . 24
324322, 323syl6eq 2452 . . . . . . . . . . . . . . . . . . . . . . 23
325 ifeq1 3703 . . . . . . . . . . . . . . . . . . . . . . . 24
326 ifid 3731 . . . . . . . . . . . . . . . . . . . . . . . 24
327325, 326syl6eq 2452 . . . . . . . . . . . . . . . . . . . . . . 23
328324, 327eqeq12d 2418 . . . . . . . . . . . . . . . . . . . . . 22
32914adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
330311adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
331 onsseleq 4582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
332329, 330, 331syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26
333332adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
334329adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
33564ffvelrni 5828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
336261, 335syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
337306, 336sseldd 3309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
338 onelon 4566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
339265, 337, 338syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
340339ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
341 onsssuc 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
342334, 340, 341syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
343 vex 2919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
344343sucid 4620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
34579adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
346 isorel 6005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
347345, 261, 259, 346syl12anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
348343sucex 4750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
349348epelc 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
350 fvex 5701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
351350epelc 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
352347, 349, 3513bitr3g 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
353344, 352mpbii 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
354 eloni 4551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
355311, 354syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
356 ordelsuc 4759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
357339, 355, 356syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
358353, 357mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
359358ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
360359sseld 3307 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
361342, 360sylbid 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
362 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
363345ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
364363, 80syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3652, 3, 4, 32, 1, 16, 33, 34, 26cantnflem1c 7599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
366364, 365, 143syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
367362, 366eleqtrrd 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
368261ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
369364, 82, 833syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
370369, 365ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
371 isorel 6005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
372363, 368, 370, 371syl12anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
373137epelc 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
374139epelc 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
375372, 373, 3743bitr3g 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
376367, 375mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
37755, 370, 150sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
378377, 152syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
379 ordelsuc 4759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
380376, 378, 379syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
381376, 380mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
382259ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
38355, 382, 247sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384 ontri1 4575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
385383, 377, 384syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
386381, 385mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
387 isorel 6005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
388363, 370, 382, 387syl12anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
389348epelc 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
390350epelc 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
391388, 389, 3903bitr3g 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
392366eleq1d 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
393391, 392bitrd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
394386, 393mtbid 292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
395394expr 599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
396395con2d 109 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
397 ontri1 4575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
398334, 340, 397syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
399396, 398sylibrd 226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
400361, 399impbid 184 . . . . . . . . . . . . . . . . . . . . . . . . . 26
401400orbi1d 684 . . . . . . . . . . . . . . . . . . . . . . . . 25
402333, 401bitr4d 248 . . . . . . . . . . . . . . . . . . . . . . . 24
403 orcom 377 . . . . . . . . . . . . . . . . . . . . . . . 24
404402, 403syl6bb 253 . . . . . . . . . . . . . . . . . . . . . . 23
405404ifbid 3717 . . . . . . . . . . . . . . . . . . . . . 22