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

Theorem cantnflem1OLD 8152
Description: Lemma for cantnfOLD 8155. 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 respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015.) Obsolete version of cantnflem1 8129 as of 2-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
cantnfsOLD.1
cantnfsOLD.2
cantnfsOLD.3
oemapvalOLD.t
oemapvalOLD.3
oemapvalOLD.4
oemapvalOLD.5
oemapvalOLD.6
cantnflem1OLD.o
cantnflem1OLD.h
Assertion
Ref Expression
cantnflem1OLD
Distinct variable groups:   , , , , , ,   , , , , , ,   , ,   , , , , ,   S, , , , ,   , , , , , ,   , ,   ,O, , , ,   , , , ,   , , , , ,   ,   ,

Proof of Theorem cantnflem1OLD
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 oemapvalOLD.3 . . . . . . . 8
2 cantnfsOLD.1 . . . . . . . . 9
3 cantnfsOLD.2 . . . . . . . . 9
4 cantnfsOLD.3 . . . . . . . . 9
52, 3, 4cantnfsOLD 8136 . . . . . . . 8
61, 5mpbid 210 . . . . . . 7
76simpld 459 . . . . . 6
87feqmptd 5926 . . . . 5
9 eqeq2 2472 . . . . . . 7
10 eqeq2 2472 . . . . . . 7
11 eqidd 2458 . . . . . . 7
12 onss 6626 . . . . . . . . . . . . 13
134, 12syl 16 . . . . . . . . . . . 12
1413sselda 3503 . . . . . . . . . . 11
15 cnvimass 5362 . . . . . . . . . . . . . . 15
16 oemapvalOLD.4 . . . . . . . . . . . . . . . . . 18
172, 3, 4cantnfsOLD 8136 . . . . . . . . . . . . . . . . . 18
1816, 17mpbid 210 . . . . . . . . . . . . . . . . 17
1918simpld 459 . . . . . . . . . . . . . . . 16
20 fdm 5740 . . . . . . . . . . . . . . . 16
2119, 20syl 16 . . . . . . . . . . . . . . 15
2215, 21syl5sseq 3551 . . . . . . . . . . . . . 14
23 cnvexg 6746 . . . . . . . . . . . . . . . . . . 19
2416, 23syl 16 . . . . . . . . . . . . . . . . . 18
25 imaexg 6737 . . . . . . . . . . . . . . . . . 18
26 cantnflem1OLD.o . . . . . . . . . . . . . . . . . . 19
2726oion 7982 . . . . . . . . . . . . . . . . . 18
2824, 25, 273syl 20 . . . . . . . . . . . . . . . . 17
29 uniexg 6597 . . . . . . . . . . . . . . . . 17
30 sucidg 4961 . . . . . . . . . . . . . . . . 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 8148 . . . . . . . . . . . . . . . . . . . . 21
36 n0i 3789 . . . . . . . . . . . . . . . . . . . . 21
3735, 36syl 16 . . . . . . . . . . . . . . . . . . . 20
384, 22ssexd 4599 . . . . . . . . . . . . . . . . . . . . . 22
392, 3, 4, 26, 16cantnfclOLD 8137 . . . . . . . . . . . . . . . . . . . . . . 23
4039simpld 459 . . . . . . . . . . . . . . . . . . . . . 22
4126oien 7984 . . . . . . . . . . . . . . . . . . . . . 22
4238, 40, 41syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
43 breq1 4455 . . . . . . . . . . . . . . . . . . . . . 22
44 ensymb 7583 . . . . . . . . . . . . . . . . . . . . . . 23
45 en0 7598 . . . . . . . . . . . . . . . . . . . . . . 23
4644, 45bitri 249 . . . . . . . . . . . . . . . . . . . . . 22
4743, 46syl6bb 261 . . . . . . . . . . . . . . . . . . . . 21
4842, 47syl5ibcom 220 . . . . . . . . . . . . . . . . . . . 20
4937, 48mtod 177 . . . . . . . . . . . . . . . . . . 19
5039simprd 463 . . . . . . . . . . . . . . . . . . . 20
51 nnlim 6713 . . . . . . . . . . . . . . . . . . . 20
5250, 51syl 16 . . . . . . . . . . . . . . . . . . 19
53 ioran 490 . . . . . . . . . . . . . . . . . . 19
5449, 52, 53sylanbrc 664 . . . . . . . . . . . . . . . . . 18
5526oicl 7975 . . . . . . . . . . . . . . . . . . 19
56 unizlim 4999 . . . . . . . . . . . . . . . . . . 19
5755, 56mp1i 12 . . . . . . . . . . . . . . . . . 18
5854, 57mtbird 301 . . . . . . . . . . . . . . . . 17
59 orduniorsuc 6665 . . . . . . . . . . . . . . . . . . 19
6055, 59mp1i 12 . . . . . . . . . . . . . . . . . 18
6160ord 377 . . . . . . . . . . . . . . . . 17
6258, 61mpd 15 . . . . . . . . . . . . . . . 16
6331, 62eleqtrrd 2548 . . . . . . . . . . . . . . 15
6426oif 7976 . . . . . . . . . . . . . . . 16
6564ffvelrni 6030 . . . . . . . . . . . . . . 15
6663, 65syl 16 . . . . . . . . . . . . . 14
6722, 66sseldd 3504 . . . . . . . . . . . . 13
68 onelon 4908 . . . . . . . . . . . . 13
694, 67, 68syl2anc 661 . . . . . . . . . . . 12
7069adantr 465 . . . . . . . . . . 11
71 ontri1 4917 . . . . . . . . . . 11
7214, 70, 71syl2anc 661 . . . . . . . . . 10
7372con2bid 329 . . . . . . . . 9
74 simprl 756 . . . . . . . . . . . 12
752, 3, 4, 32, 1, 16, 33, 34oemapvali 8124 . . . . . . . . . . . . . 14
7675simp3d 1010 . . . . . . . . . . . . 13
7776adantr 465 . . . . . . . . . . . 12
7826oiiso 7983 . . . . . . . . . . . . . . . . . . . . . 22
7938, 40, 78syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
80 isof1o 6221 . . . . . . . . . . . . . . . . . . . . 21
8179, 80syl 16 . . . . . . . . . . . . . . . . . . . 20
82 f1ocnv 5833 . . . . . . . . . . . . . . . . . . . 20
83 f1of 5821 . . . . . . . . . . . . . . . . . . . 20
8481, 82, 833syl 20 . . . . . . . . . . . . . . . . . . 19
8584, 35ffvelrnd 6032 . . . . . . . . . . . . . . . . . 18
86 elssuni 4279 . . . . . . . . . . . . . . . . . 18
8785, 86syl 16 . . . . . . . . . . . . . . . . 17
88 ordelon 4907 . . . . . . . . . . . . . . . . . . . 20
8955, 85, 88sylancr 663 . . . . . . . . . . . . . . . . . . 19
90 eloni 4893 . . . . . . . . . . . . . . . . . . 19
9189, 90syl 16 . . . . . . . . . . . . . . . . . 18
92 orduni 6629 . . . . . . . . . . . . . . . . . . 19
9355, 92ax-mp 5 . . . . . . . . . . . . . . . . . 18
94 ordtri1 4916 . . . . . . . . . . . . . . . . . 18
9591, 93, 94sylancl 662 . . . . . . . . . . . . . . . . 17
9687, 95mpbid 210 . . . . . . . . . . . . . . . 16
97 isorel 6222 . . . . . . . . . . . . . . . . . . 19
9879, 63, 85, 97syl12anc 1226 . . . . . . . . . . . . . . . . . 18
99 fvex 5881 . . . . . . . . . . . . . . . . . . 19
10099epelc 4798 . . . . . . . . . . . . . . . . . 18
101 fvex 5881 . . . . . . . . . . . . . . . . . . 19
102101epelc 4798 . . . . . . . . . . . . . . . . . 18
10398, 100, 1023bitr3g 287 . . . . . . . . . . . . . . . . 17
104 f1ocnvfv2 6183 . . . . . . . . . . . . . . . . . . 19
10581, 35, 104syl2anc 661 . . . . . . . . . . . . . . . . . 18
106105eleq2d 2527 . . . . . . . . . . . . . . . . 17
107103, 106bitrd 253 . . . . . . . . . . . . . . . 16
10896, 107mtbid 300 . . . . . . . . . . . . . . 15
10975simp1d 1008 . . . . . . . . . . . . . . . . 17
110 onelon 4908 . . . . . . . . . . . . . . . . 17
1114, 109, 110syl2anc 661 . . . . . . . . . . . . . . . 16
112 ontri1 4917 . . . . . . . . . . . . . . . 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 4930 . . . . . . . . . . . . . 14
120117, 118, 119syl2anc 661 . . . . . . . . . . . . 13
121115, 116, 120mp2and 679 . . . . . . . . . . . 12
122 eleq2 2530 . . . . . . . . . . . . . 14
123 fveq2 5871 . . . . . . . . . . . . . . 15
124 fveq2 5871 . . . . . . . . . . . . . . 15
125123, 124eqeq12d 2479 . . . . . . . . . . . . . 14
126122, 125imbi12d 320 . . . . . . . . . . . . 13
127126rspcv 3206 . . . . . . . . . . . 12
12874, 77, 121, 127syl3c 61 . . . . . . . . . . 11
129116adantr 465 . . . . . . . . . . . . . . 15
13079ad2antrr 725 . . . . . . . . . . . . . . . . . 18
13163ad2antrr 725 . . . . . . . . . . . . . . . . . 18
13284ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
133 ffvelrn 6029 . . . . . . . . . . . . . . . . . . 19
134132, 133sylancom 667 . . . . . . . . . . . . . . . . . 18
135 isorel 6222 . . . . . . . . . . . . . . . . . 18
136130, 131, 134, 135syl12anc 1226 . . . . . . . . . . . . . . . . 17
137 fvex 5881 . . . . . . . . . . . . . . . . . 18
138137epelc 4798 . . . . . . . . . . . . . . . . 17
139 fvex 5881 . . . . . . . . . . . . . . . . . 18
140139epelc 4798 . . . . . . . . . . . . . . . . 17
141136, 138, 1403bitr3g 287 . . . . . . . . . . . . . . . 16
14281ad2antrr 725 . . . . . . . . . . . . . . . . . 18
143 f1ocnvfv2 6183 . . . . . . . . . . . . . . . . . 18
144142, 143sylancom 667 . . . . . . . . . . . . . . . . 17
145144eleq2d 2527 . . . . . . . . . . . . . . . 16
146141, 145bitrd 253 . . . . . . . . . . . . . . 15
147129, 146mpbird 232 . . . . . . . . . . . . . 14
148 elssuni 4279 . . . . . . . . . . . . . . . 16
149134, 148syl 16 . . . . . . . . . . . . . . 15
150 ordelon 4907 . . . . . . . . . . . . . . . . . 18
15155, 134, 150sylancr 663 . . . . . . . . . . . . . . . . 17
152 eloni 4893 . . . . . . . . . . . . . . . . 17
153151, 152syl 16 . . . . . . . . . . . . . . . 16
154 ordtri1 4916 . . . . . . . . . . . . . . . 16
155153, 93, 154sylancl 662 . . . . . . . . . . . . . . 15
156149, 155mpbid 210 . . . . . . . . . . . . . 14
157147, 156pm2.65da 576 . . . . . . . . . . . . 13
15874, 157eldifd 3486 . . . . . . . . . . . 12
159 df1o2 7161 . . . . . . . . . . . . . . . 16
160159difeq2i 3618 . . . . . . . . . . . . . . 15
161160imaeq2i 5340 . . . . . . . . . . . . . 14
162 eqimss2 3556 . . . . . . . . . . . . . 14
163161, 162mp1i 12 . . . . . . . . . . . . 13
16419, 163suppssrOLD 6021 . . . . . . . . . . . 12
165158, 164syldan 470 . . . . . . . . . . 11
166128, 165eqtrd 2498 . . . . . . . . . 10
167166expr 615 . . . . . . . . 9
16873, 167sylbird 235 . . . . . . . 8
169168imp 429 . . . . . . 7
1709, 10, 11, 169ifbothda 3976 . . . . . 6
171170mpteq2dva 4538 . . . . 5
1728, 171eqtrd 2498 . . . 4
173172fveq2d 5875 . . 3
17462, 50eqeltrrd 2546 . . . . . 6
175 peano2b 6716 . . . . . 6
176174, 175sylibr 212 . . . . 5
177 eleq1 2529 . . . . . . . . 9
178 sseq2 3525 . . . . . . . . 9
179177, 178anbi12d 710 . . . . . . . 8
180 fveq2 5871 . . . . . . . . . . . . 13
181180sseq2d 3531 . . . . . . . . . . . 12
182181ifbid 3963 . . . . . . . . . . 11
183182mpteq2dv 4539 . . . . . . . . . 10
184183fveq2d 5875 . . . . . . . . 9
185 suceq 4948 . . . . . . . . . 10
186185fveq2d 5875 . . . . . . . . 9
187184, 186eleq12d 2539 . . . . . . . 8
188179, 187imbi12d 320 . . . . . . 7
189188imbi2d 316 . . . . . 6
190 eleq1 2529 . . . . . . . . 9
191 sseq2 3525 . . . . . . . . 9
192190, 191anbi12d 710 . . . . . . . 8
193 fveq2 5871 . . . . . . . . . . . . 13
194193sseq2d 3531 . . . . . . . . . . . 12
195194ifbid 3963 . . . . . . . . . . 11
196195mpteq2dv 4539 . . . . . . . . . 10
197196fveq2d 5875 . . . . . . . . 9
198 suceq 4948 . . . . . . . . . 10
199198fveq2d 5875 . . . . . . . . 9
200197, 199eleq12d 2539 . . . . . . . 8
201192, 200imbi12d 320 . . . . . . 7
202 eleq1 2529 . . . . . . . . 9
203 sseq2 3525 . . . . . . . . 9