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

Theorem cantnflem1OLD 8134
 Description: Lemma for cantnfOLD 8137. 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.) Obsolete version of cantnflem1 8111 as of 2-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
cantnfsOLD.1 CNF
cantnfsOLD.2
cantnfsOLD.3
oemapvalOLD.t
oemapvalOLD.3
oemapvalOLD.4
oemapvalOLD.5
oemapvalOLD.6
cantnflem1OLD.o OrdIso
cantnflem1OLD.h seq𝜔
Assertion
Ref Expression
cantnflem1OLD CNF CNF
Distinct variable groups:   ,,,,,,   ,,,,,,   ,,   ,,,,,   ,,,,,   ,,,,,,   ,,   ,,,,,   ,,,,   ,,,,,   ,   ,
Allowed substitution hints:   ()   ()   (,,,)   (,,,)   ()   ()

Proof of Theorem cantnflem1OLD
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 oemapvalOLD.3 . . . . . . . 8
2 cantnfsOLD.1 . . . . . . . . 9 CNF
3 cantnfsOLD.2 . . . . . . . . 9
4 cantnfsOLD.3 . . . . . . . . 9
52, 3, 4cantnfsOLD 8118 . . . . . . . 8
61, 5mpbid 210 . . . . . . 7
76simpld 459 . . . . . 6
87feqmptd 5911 . . . . 5
9 eqeq2 2458 . . . . . . 7
10 eqeq2 2458 . . . . . . 7
11 eqidd 2444 . . . . . . 7
12 onss 6611 . . . . . . . . . . . . 13
134, 12syl 16 . . . . . . . . . . . 12
1413sselda 3489 . . . . . . . . . . 11
15 cnvimass 5347 . . . . . . . . . . . . . . 15
16 oemapvalOLD.4 . . . . . . . . . . . . . . . . . 18
172, 3, 4cantnfsOLD 8118 . . . . . . . . . . . . . . . . . 18
1816, 17mpbid 210 . . . . . . . . . . . . . . . . 17
1918simpld 459 . . . . . . . . . . . . . . . 16
20 fdm 5725 . . . . . . . . . . . . . . . 16
2119, 20syl 16 . . . . . . . . . . . . . . 15
2215, 21syl5sseq 3537 . . . . . . . . . . . . . 14
23 cnvexg 6731 . . . . . . . . . . . . . . . . . . 19
2416, 23syl 16 . . . . . . . . . . . . . . . . . 18
25 imaexg 6722 . . . . . . . . . . . . . . . . . 18
26 cantnflem1OLD.o . . . . . . . . . . . . . . . . . . 19 OrdIso
2726oion 7964 . . . . . . . . . . . . . . . . . 18
2824, 25, 273syl 20 . . . . . . . . . . . . . . . . 17
29 uniexg 6582 . . . . . . . . . . . . . . . . 17
30 sucidg 4946 . . . . . . . . . . . . . . . . 17
3128, 29, 303syl 20 . . . . . . . . . . . . . . . 16
32 oemapvalOLD.t . . . . . . . . . . . . . . . . . . . . . 22
33 oemapvalOLD.5 . . . . . . . . . . . . . . . . . . . . . 22
34 oemapvalOLD.6 . . . . . . . . . . . . . . . . . . . . . 22
352, 3, 4, 32, 1, 16, 33, 34cantnflem1aOLD 8130 . . . . . . . . . . . . . . . . . . . . 21
36 n0i 3775 . . . . . . . . . . . . . . . . . . . . 21
3735, 36syl 16 . . . . . . . . . . . . . . . . . . . 20
384, 22ssexd 4584 . . . . . . . . . . . . . . . . . . . . . 22
392, 3, 4, 26, 16cantnfclOLD 8119 . . . . . . . . . . . . . . . . . . . . . . 23
4039simpld 459 . . . . . . . . . . . . . . . . . . . . . 22
4126oien 7966 . . . . . . . . . . . . . . . . . . . . . 22
4238, 40, 41syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
43 breq1 4440 . . . . . . . . . . . . . . . . . . . . . 22
44 ensymb 7565 . . . . . . . . . . . . . . . . . . . . . . 23
45 en0 7580 . . . . . . . . . . . . . . . . . . . . . . 23
4644, 45bitri 249 . . . . . . . . . . . . . . . . . . . . . 22
4743, 46syl6bb 261 . . . . . . . . . . . . . . . . . . . . 21
4842, 47syl5ibcom 220 . . . . . . . . . . . . . . . . . . . 20
4937, 48mtod 177 . . . . . . . . . . . . . . . . . . 19
5039simprd 463 . . . . . . . . . . . . . . . . . . . 20
51 nnlim 6698 . . . . . . . . . . . . . . . . . . . 20
5250, 51syl 16 . . . . . . . . . . . . . . . . . . 19
53 ioran 490 . . . . . . . . . . . . . . . . . . 19
5449, 52, 53sylanbrc 664 . . . . . . . . . . . . . . . . . 18
5526oicl 7957 . . . . . . . . . . . . . . . . . . 19
56 unizlim 4984 . . . . . . . . . . . . . . . . . . 19
5755, 56mp1i 12 . . . . . . . . . . . . . . . . . 18
5854, 57mtbird 301 . . . . . . . . . . . . . . . . 17
59 orduniorsuc 6650 . . . . . . . . . . . . . . . . . . 19
6055, 59mp1i 12 . . . . . . . . . . . . . . . . . 18
6160ord 377 . . . . . . . . . . . . . . . . 17
6258, 61mpd 15 . . . . . . . . . . . . . . . 16
6331, 62eleqtrrd 2534 . . . . . . . . . . . . . . 15
6426oif 7958 . . . . . . . . . . . . . . . 16
6564ffvelrni 6015 . . . . . . . . . . . . . . 15
6663, 65syl 16 . . . . . . . . . . . . . 14
6722, 66sseldd 3490 . . . . . . . . . . . . 13
68 onelon 4893 . . . . . . . . . . . . 13
694, 67, 68syl2anc 661 . . . . . . . . . . . 12
7069adantr 465 . . . . . . . . . . 11
71 ontri1 4902 . . . . . . . . . . 11
7214, 70, 71syl2anc 661 . . . . . . . . . 10
7372con2bid 329 . . . . . . . . 9
74 simprl 756 . . . . . . . . . . . 12
752, 3, 4, 32, 1, 16, 33, 34oemapvali 8106 . . . . . . . . . . . . . 14
7675simp3d 1011 . . . . . . . . . . . . 13
7776adantr 465 . . . . . . . . . . . 12
7826oiiso 7965 . . . . . . . . . . . . . . . . . . . . . 22
7938, 40, 78syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
80 isof1o 6206 . . . . . . . . . . . . . . . . . . . . 21
8179, 80syl 16 . . . . . . . . . . . . . . . . . . . 20
82 f1ocnv 5818 . . . . . . . . . . . . . . . . . . . 20
83 f1of 5806 . . . . . . . . . . . . . . . . . . . 20
8481, 82, 833syl 20 . . . . . . . . . . . . . . . . . . 19
8584, 35ffvelrnd 6017 . . . . . . . . . . . . . . . . . 18
86 elssuni 4264 . . . . . . . . . . . . . . . . . 18
8785, 86syl 16 . . . . . . . . . . . . . . . . 17
88 ordelon 4892 . . . . . . . . . . . . . . . . . . . 20
8955, 85, 88sylancr 663 . . . . . . . . . . . . . . . . . . 19
90 eloni 4878 . . . . . . . . . . . . . . . . . . 19
9189, 90syl 16 . . . . . . . . . . . . . . . . . 18
92 orduni 6614 . . . . . . . . . . . . . . . . . . 19
9355, 92ax-mp 5 . . . . . . . . . . . . . . . . . 18
94 ordtri1 4901 . . . . . . . . . . . . . . . . . 18
9591, 93, 94sylancl 662 . . . . . . . . . . . . . . . . 17
9687, 95mpbid 210 . . . . . . . . . . . . . . . 16
97 isorel 6207 . . . . . . . . . . . . . . . . . . 19
9879, 63, 85, 97syl12anc 1227 . . . . . . . . . . . . . . . . . 18
99 fvex 5866 . . . . . . . . . . . . . . . . . . 19
10099epelc 4783 . . . . . . . . . . . . . . . . . 18
101 fvex 5866 . . . . . . . . . . . . . . . . . . 19
102101epelc 4783 . . . . . . . . . . . . . . . . . 18
10398, 100, 1023bitr3g 287 . . . . . . . . . . . . . . . . 17
104 f1ocnvfv2 6168 . . . . . . . . . . . . . . . . . . 19
10581, 35, 104syl2anc 661 . . . . . . . . . . . . . . . . . 18
106105eleq2d 2513 . . . . . . . . . . . . . . . . 17
107103, 106bitrd 253 . . . . . . . . . . . . . . . 16
10896, 107mtbid 300 . . . . . . . . . . . . . . 15
10975simp1d 1009 . . . . . . . . . . . . . . . . 17
110 onelon 4893 . . . . . . . . . . . . . . . . 17
1114, 109, 110syl2anc 661 . . . . . . . . . . . . . . . 16
112 ontri1 4902 . . . . . . . . . . . . . . . 16
113111, 69, 112syl2anc 661 . . . . . . . . . . . . . . 15
114108, 113mpbird 232 . . . . . . . . . . . . . 14
115114adantr 465 . . . . . . . . . . . . 13
116 simprr 757 . . . . . . . . . . . . 13
117111adantr 465 . . . . . . . . . . . . . 14
11814adantrr 716 . . . . . . . . . . . . . 14
119 ontr2 4915 . . . . . . . . . . . . . 14
120117, 118, 119syl2anc 661 . . . . . . . . . . . . 13
121115, 116, 120mp2and 679 . . . . . . . . . . . 12
122 eleq2 2516 . . . . . . . . . . . . . 14
123 fveq2 5856 . . . . . . . . . . . . . . 15
124 fveq2 5856 . . . . . . . . . . . . . . 15
125123, 124eqeq12d 2465 . . . . . . . . . . . . . 14
126122, 125imbi12d 320 . . . . . . . . . . . . 13
127126rspcv 3192 . . . . . . . . . . . 12
12874, 77, 121, 127syl3c 61 . . . . . . . . . . 11
129116adantr 465 . . . . . . . . . . . . . . 15
13079ad2antrr 725 . . . . . . . . . . . . . . . . . 18
13163ad2antrr 725 . . . . . . . . . . . . . . . . . 18
13284ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
133 ffvelrn 6014 . . . . . . . . . . . . . . . . . . 19
134132, 133sylancom 667 . . . . . . . . . . . . . . . . . 18
135 isorel 6207 . . . . . . . . . . . . . . . . . 18
136130, 131, 134, 135syl12anc 1227 . . . . . . . . . . . . . . . . 17
137 fvex 5866 . . . . . . . . . . . . . . . . . 18
138137epelc 4783 . . . . . . . . . . . . . . . . 17
139 fvex 5866 . . . . . . . . . . . . . . . . . 18
140139epelc 4783 . . . . . . . . . . . . . . . . 17
141136, 138, 1403bitr3g 287 . . . . . . . . . . . . . . . 16
14281ad2antrr 725 . . . . . . . . . . . . . . . . . 18
143 f1ocnvfv2 6168 . . . . . . . . . . . . . . . . . 18
144142, 143sylancom 667 . . . . . . . . . . . . . . . . 17
145144eleq2d 2513 . . . . . . . . . . . . . . . 16
146141, 145bitrd 253 . . . . . . . . . . . . . . 15
147129, 146mpbird 232 . . . . . . . . . . . . . 14
148 elssuni 4264 . . . . . . . . . . . . . . . 16
149134, 148syl 16 . . . . . . . . . . . . . . 15
150 ordelon 4892 . . . . . . . . . . . . . . . . . 18
15155, 134, 150sylancr 663 . . . . . . . . . . . . . . . . 17
152 eloni 4878 . . . . . . . . . . . . . . . . 17
153151, 152syl 16 . . . . . . . . . . . . . . . 16
154 ordtri1 4901 . . . . . . . . . . . . . . . 16
155153, 93, 154sylancl 662 . . . . . . . . . . . . . . 15
156149, 155mpbid 210 . . . . . . . . . . . . . 14
157147, 156pm2.65da 576 . . . . . . . . . . . . 13
15874, 157eldifd 3472 . . . . . . . . . . . 12
159 df1o2 7144 . . . . . . . . . . . . . . . 16
160159difeq2i 3604 . . . . . . . . . . . . . . 15
161160imaeq2i 5325 . . . . . . . . . . . . . 14
162 eqimss2 3542 . . . . . . . . . . . . . 14
163161, 162mp1i 12 . . . . . . . . . . . . 13
16419, 163suppssrOLD 6006 . . . . . . . . . . . 12
165158, 164syldan 470 . . . . . . . . . . 11
166128, 165eqtrd 2484 . . . . . . . . . 10
167166expr 615 . . . . . . . . 9
16873, 167sylbird 235 . . . . . . . 8
169168imp 429 . . . . . . 7
1709, 10, 11, 169ifbothda 3961 . . . . . 6
171170mpteq2dva 4523 . . . . 5
1728, 171eqtrd 2484 . . . 4
173172fveq2d 5860 . . 3 CNF CNF
17462, 50eqeltrrd 2532 . . . . . 6
175 peano2b 6701 . . . . . 6
176174, 175sylibr 212 . . . . 5
177 eleq1 2515 . . . . . . . . 9
178 sseq2 3511 . . . . . . . . 9
179177, 178anbi12d 710 . . . . . . . 8
180 fveq2 5856 . . . . . . . . . . . . 13
181180sseq2d 3517 . . . . . . . . . . . 12
182181ifbid 3948 . . . . . . . . . . 11
183182mpteq2dv 4524 . . . . . . . . . 10
184183fveq2d 5860 . . . . . . . . 9 CNF CNF
185 suceq 4933 . . . . . . . . . 10
186185fveq2d 5860 . . . . . . . . 9
187184, 186eleq12d 2525 . . . . . . . 8 CNF CNF
188179, 187imbi12d 320 . . . . . . 7 CNF CNF
189188imbi2d 316 . . . . . 6 CNF CNF
190 eleq1 2515 . . . . . . . . 9
191 sseq2 3511 . . . . . . . . 9
192190, 191anbi12d 710 . . . . . . . 8
193 fveq2 5856 . . . . . . . . . . . . 13
194193sseq2d 3517 . . . . . . . . . . . 12
195194ifbid 3948 . . . . . . . . . . 11
196195mpteq2dv 4524 . . . . . . . . . 10
197196fveq2d 5860 . . . . . . . . 9 CNF CNF
198 suceq 4933 . . . . . . . . . 10
199198fveq2d 5860 . . . . . . . . 9
200197, 199eleq12d 2525 . . . . . . . 8 CNF CNF
201192, 200imbi12d 320 . . . . . . 7 CNF CNF
202 eleq1 2515 . . . . . . . . 9
203 sseq2 3511 . . . . . . . . 9
204202, 203anbi12d 710 . . . . . . . 8
205 fveq2 5856 . . . . . . . . . . . . 13
206205sseq2d 3517 . . . . . . . . . . . 12
207206ifbid 3948 . . . . . . . . . . 11
208207mpteq2dv 4524 . . . . . . . . . 10
209208fveq2d 5860 . . . . . . . . 9 CNF CNF
210 suceq 4933 . . . . . . . . . 10
211210fveq2d 5860 . . . . . . . . 9
212209, 211eleq12d 2525 . . . . . . . 8 CNF CNF
213204, 212imbi12d 320 . . . . . . 7 CNF CNF
214 eleq1 2515 . . . . . . . . 9
215 sseq2 3511 . . . . . . . . 9
216214, 215anbi12d 710 . . . . . . . 8
217 fveq2 5856 . . . . . . . . . . . . 13
218217sseq2d 3517 . . . . . . . . . . . 12
219218ifbid 3948 . . . . . . . . . . 11
220219mpteq2dv 4524 . . . . . . . . . 10
221220fveq2d 5860 . . . . . . . . 9 CNF CNF
222 suceq 4933 . . . . . . . . . 10
223222fveq2d 5860 . . . . . . . . 9
224221, 223eleq12d 2525 . . . . . . . 8 CNF CNF
225216, 224imbi12d 320 . . . . . . 7 CNF CNF
226105sseq2d 3517 . . . . . . . . . . . 12
227226ifbid 3948 . . . . . . . . . . 11
228227mpteq2dv 4524 . . . . . . . . . 10
229228fveq2d 5860 . . . . . . . . 9 CNF CNF
230 cantnflem1OLD.h . . . . . . . . . 10 seq𝜔
2312, 3, 4, 32, 1, 16, 33, 34, 26, 230cantnflem1dOLD 8133 . . . . . . . . 9 CNF
232229, 231eqeltrd 2531 . . . . . . . 8 CNF
233 ss0 3802 . . . . . . . . . . . . . . 15
234233fveq2d 5860 . . . . . . . . . . . . . 14
235234sseq2d 3517 . . . . . . . . . . . . 13
236235ifbid 3948 . . . . . . . . . . . 12
237236mpteq2dv 4524 . . . . . . . . . . 11
238237fveq2d 5860 . . . . . . . . . 10 CNF CNF
239 suceq 4933 . . . . . . . . . . . 12
240233, 239syl 16 . . . . . . . . . . 11
241240fveq2d 5860 . . . . . . . . . 10
242238, 241eleq12d 2525 . . . . . . . . 9 CNF CNF
243242adantl 466 . . . . . . . 8 CNF CNF
244232, 243syl5ibcom 220 . . . . . . 7 CNF
24589adantr 465 . . . . . . . . . . . 12
24655a1i 11 . . . . . . . . . . . . 13
247 ordelon 4892 . . . . . . . . . . . . 13
248246, 247sylan 471 . . . . . . . . . . . 12
249 onsseleq 4909 . . . . . . . . . . . 12
250245, 248, 249syl2anc 661 . . . . . . . . . . 11
251 sucelon 6637 . . . . . . . . . . . . . . . 16
252248, 251sylibr 212 . . . . . . . . . . . . . . 15
253 eloni 4878 . . . . . . . . . . . . . . 15
254252, 253syl 16 . . . . . . . . . . . . . 14
255 ordsssuc 4954 . . . . . . . . . . . . . 14
256245, 254, 255syl2anc 661 . . . . . . . . . . . . 13
257 ordtr 4882 . . . . . . . . . . . . . . . . . 18
25855, 257mp1i 12 . . . . . . . . . . . . . . . . 17
259 simprl 756 . . . . . . . . . . . . . . . . 17
260 trsuc 4952 . . . . . . . . . . . . . . . . 17
261258, 259, 260syl2anc 661 . . . . . . . . . . . . . . . 16
262 simprr 757 . . . . . . . . . . . . . . . 16
263261, 262jca 532 . . . . . . . . . . . . . . 15
2643adantr 465 . . . . . . . . . . . . . . . . . . . 20
2654adantr 465 . . . . . . . . . . . . . . . . . . . 20
266 oecl 7189 . . . . . . . . . . . . . . . . . . . 20
267264, 265, 266syl2anc 661 . . . . . . . . . . . . . . . . . . 19
2682, 264, 265cantnff 8096 . . . . . . . . . . . . . . . . . . . 20 CNF
2697ffvelrnda 6016 . . . . . . . . . . . . . . . . . . . . . . . 24
27019, 109ffvelrnd 6017 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
271 ne0i 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
272270, 271syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
273 on0eln0 4923 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2743, 273syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
275272, 274mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . 25
276275adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
277 ifcl 3968 . . . . . . . . . . . . . . . . . . . . . . . 24
278269, 276, 277syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
279 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . 23
280278, 279fmptd 6040 . . . . . . . . . . . . . . . . . . . . . 22
2816simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23
282160imaeq2i 5325 . . . . . . . . . . . . . . . . . . . . . . . 24
283160imaeq2i 5325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
284 eqimss2 3542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
285283, 284mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2867, 285suppssrOLD 6006 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
287286ifeq1d 3944 . . . . . . . . . . . . . . . . . . . . . . . . . 26
288 ifid 3963 . . . . . . . . . . . . . . . . . . . . . . . . . 26
289287, 288syl6eq 2500 . . . . . . . . . . . . . . . . . . . . . . . . 25
290289suppss2OLD 6515 . . . . . . . . . . . . . . . . . . . . . . . 24
291282, 290syl5eqss 3533 . . . . . . . . . . . . . . . . . . . . . . 23
292 ssfi 7742 . . . . . . . . . . . . . . . . . . . . . . 23
293281, 291, 292syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22
2942, 3, 4cantnfsOLD 8118 . . . . . . . . . . . . . . . . . . . . . 22
295280, 293, 294mpbir2and 922 . . . . . . . . . . . . . . . . . . . . 21
296295adantr 465 . . . . . . . . . . . . . . . . . . . 20
297268, 296ffvelrnd 6017 . . . . . . . . . . . . . . . . . . 19 CNF
298 onelon 4893 . . . . . . . . . . . . . . . . . . 19 CNF CNF
299267, 297, 298syl2anc 661 . . . . . . . . . . . . . . . . . 18 CNF
30050adantr 465 . . . . . . . . . . . . . . . . . . . 20
301 elnn 6695 . . . . . . . . . . . . . . . . . . . 20
302259, 300, 301syl2anc 661 . . . . . . . . . . . . . . . . . . 19
303230cantnfvalf 8087 . . . . . . . . . . . . . . . . . . . 20
304303ffvelrni 6015 . . . . . . . . . . . . . . . . . . 19
305302, 304syl 16 . . . . . . . . . . . . . . . . . 18
30622adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
30764ffvelrni 6015 . . . . . . . . . . . . . . . . . . . . . . 23
308259, 307syl 16 . . . . . . . . . . . . . . . . . . . . . 22
309306, 308sseldd 3490 . . . . . . . . . . . . . . . . . . . . 21
310 onelon 4893 . . . . . . . . . . . . . . . . . . . . 21
311265, 309, 310syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
312 oecl 7189 . . . . . . . . . . . . . . . . . . . 20
313264, 311, 312syl2anc 661 . . . . . . . . . . . . . . . . . . 19
3147adantr 465 . . . . . . . . . . . . . . . . . . . . 21
315314, 309ffvelrnd 6017 . . . . . . . . . . . . . . . . . . . 20
316 onelon 4893 . . . . . . . . . . . . . . . . . . . 20
317264, 315, 316syl2anc 661 . . . . . . . . . . . . . . . . . . 19
318 omcl 7188 . . . . . . . . . . . . . . . . . . 19
319313, 317, 318syl2anc 661 . . . . . . . . . . . . . . . . . 18
320 oaord 7198 . . . . . . . . . . . . . . . . . 18 CNF CNF CNF
321299, 305, 319, 320syl3anc 1229 . . . . . . . . . . . . . . . . 17 CNF CNF
322 ifeq1 3930 . . . . . . . . . . . . . . . . . . . . . . . 24
323 ifid 3963 . . . . . . . . . . . . . . . . . . . . . . . 24
324322, 323syl6eq 2500 . . . . . . . . . . . . . . . . . . . . . . 23
325 ifeq1 3930 . . . . . . . . . . . . . . . . . . . . . . . 24
326 ifid 3963 . . . . . . . . . . . . . . . . . . . . . . . 24
327325, 326syl6eq 2500 . . . . . . . . . . . . . . . . . . . . . . 23
328324, 327eqeq12d 2465 . . . . . . . . . . . . . . . . . . . . . 22
32914adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
330311adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
331 onsseleq 4909 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
332329, 330, 331syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26
333332adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
334329adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
33564ffvelrni 6015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
336261, 335syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
337306, 336sseldd 3490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
338 onelon 4893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
339265, 337, 338syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
340339ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
341 onsssuc 4955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
342334, 340, 341syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
343 vex 3098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
344343sucid 4947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
34579adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
346 isorel 6207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
347345, 261, 259, 346syl12anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
348343sucex 6631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
349348epelc 4783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
350 fvex 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
351350epelc 4783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
352347, 349, 3513bitr3g 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
353344, 352mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
354 eloni 4878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
355311, 354syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
356 ordelsuc 6640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
357339, 355, 356syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
358353, 357mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
359358ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
360359sseld 3488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
361342, 360sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
362 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
363345ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
364363, 80syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3652, 3, 4, 32, 1, 16, 33, 34, 26cantnflem1cOLD 8132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
366364, 365, 143syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
367362, 366eleqtrrd 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
368261ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
369364, 82, 833syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
370369, 365ffvelrnd 6017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
371 isorel 6207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
372363, 368, 370, 371syl12anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
373137epelc 4783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
374139epelc 4783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
375372, 373, 3743bitr3g 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
376367, 375mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
37755, 370, 150sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
378377, 152syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
379 ordelsuc 6640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
380376, 378, 379syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
381376, 380mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
382259ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
38355, 382, 247sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384 ontri1 4902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
385383, 377, 384syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
386381, 385mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
387 isorel 6207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
388363, 370, 382, 387syl12anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
389348epelc 4783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
390350epelc 4783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
391388, 389, 3903bitr3g 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
392366eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
393391, 392bitrd 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
394386, 393mtbid 300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
395394expr 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
396395con2d 115 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
397 ontri1 4902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
398334, 340, 397syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
399396, 398sylibrd 234 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
400361, 399impbid 191 . . . . . . . . . . . . . . . . . . . . . . . . . 26
401400orbi1d 702 . . . . . . . . . . . . . . . . . . . . . . . . 25
402333, 401bitr4d 256 . . . . . . . . . . . . . . . . . . . . . . . 24
403 orcom 387 . . . . . . . . . . . . . . . . . . . . . . . 24
404402, 403syl6bb 261 . . . . . . . . . . . . . . . . . . . . . . 23
405404ifbid 3948 . . . . . . . . . . . . . . . . . . . . . 22