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

Theorem cantnflem1 8129
 Description: Lemma for cantnf 8133. 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.) (Revised by AV, 2-Jul-2019.)
Hypotheses
Ref Expression
cantnfs.s
cantnfs.a
cantnfs.b
oemapval.t
oemapval.f
oemapval.g
oemapvali.r
oemapvali.x
cantnflem1.o
cantnflem1.h
Assertion
Ref Expression
cantnflem1
Distinct variable groups:   ,,,,,,   ,,,,,,   ,,   ,,,,,   S,,,,,   ,,,,,,   ,,   ,O,,,,   ,,,,   ,,,,,   ,   ,

Proof of Theorem cantnflem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ovex 6324 . . . . . 6
2 cantnflem1.o . . . . . . 7
32oion 7982 . . . . . 6
41, 3mp1i 12 . . . . 5
5 uniexg 6597 . . . . 5
6 sucidg 4961 . . . . 5
74, 5, 63syl 20 . . . 4
8 cantnfs.s . . . . . . . . . 10
9 cantnfs.a . . . . . . . . . 10
10 cantnfs.b . . . . . . . . . 10
11 oemapval.t . . . . . . . . . 10
12 oemapval.f . . . . . . . . . 10
13 oemapval.g . . . . . . . . . 10
14 oemapvali.r . . . . . . . . . 10
15 oemapvali.x . . . . . . . . . 10
168, 9, 10, 11, 12, 13, 14, 15cantnflem1a 8125 . . . . . . . . 9
17 n0i 3789 . . . . . . . . 9
1816, 17syl 16 . . . . . . . 8
19 suppssdm 6931 . . . . . . . . . . . 12
208, 9, 10cantnfs 8106 . . . . . . . . . . . . . . 15
2113, 20mpbid 210 . . . . . . . . . . . . . 14
2221simpld 459 . . . . . . . . . . . . 13
23 fdm 5740 . . . . . . . . . . . . 13
2422, 23syl 16 . . . . . . . . . . . 12
2519, 24syl5sseq 3551 . . . . . . . . . . 11
2610, 25ssexd 4599 . . . . . . . . . 10
278, 9, 10, 2, 13cantnfcl 8107 . . . . . . . . . . 11
2827simpld 459 . . . . . . . . . 10
292oien 7984 . . . . . . . . . 10
3026, 28, 29syl2anc 661 . . . . . . . . 9
31 breq1 4455 . . . . . . . . . 10
32 ensymb 7583 . . . . . . . . . . 11
33 en0 7598 . . . . . . . . . . 11
3432, 33bitri 249 . . . . . . . . . 10
3531, 34syl6bb 261 . . . . . . . . 9
3630, 35syl5ibcom 220 . . . . . . . 8
3718, 36mtod 177 . . . . . . 7
3827simprd 463 . . . . . . . 8
39 nnlim 6713 . . . . . . . 8
4038, 39syl 16 . . . . . . 7
41 ioran 490 . . . . . . 7
4237, 40, 41sylanbrc 664 . . . . . 6
432oicl 7975 . . . . . . 7
44 unizlim 4999 . . . . . . 7
4543, 44mp1i 12 . . . . . 6
4642, 45mtbird 301 . . . . 5
47 orduniorsuc 6665 . . . . . . 7
4843, 47mp1i 12 . . . . . 6
4948ord 377 . . . . 5
5046, 49mpd 15 . . . 4
517, 50eleqtrrd 2548 . . 3
522oiiso 7983 . . . . . . . 8
5326, 28, 52syl2anc 661 . . . . . . 7
54 isof1o 6221 . . . . . . 7
5553, 54syl 16 . . . . . 6
56 f1ocnv 5833 . . . . . 6
57 f1of 5821 . . . . . 6
5855, 56, 573syl 20 . . . . 5
5958, 16ffvelrnd 6032 . . . 4
60 elssuni 4279 . . . 4
6159, 60syl 16 . . 3
6250, 38eqeltrrd 2546 . . . . 5
63 peano2b 6716 . . . . 5
6462, 63sylibr 212 . . . 4
65 eleq1 2529 . . . . . . . 8
66 sseq2 3525 . . . . . . . 8
6765, 66anbi12d 710 . . . . . . 7
68 fveq2 5871 . . . . . . . . . . . 12
6968sseq2d 3531 . . . . . . . . . . 11
7069ifbid 3963 . . . . . . . . . 10
7170mpteq2dv 4539 . . . . . . . . 9
7271fveq2d 5875 . . . . . . . 8
73 suceq 4948 . . . . . . . . 9
7473fveq2d 5875 . . . . . . . 8
7572, 74eleq12d 2539 . . . . . . 7
7667, 75imbi12d 320 . . . . . 6
7776imbi2d 316 . . . . 5
78 eleq1 2529 . . . . . . . 8
79 sseq2 3525 . . . . . . . 8
8078, 79anbi12d 710 . . . . . . 7
81 fveq2 5871 . . . . . . . . . . . 12
8281sseq2d 3531 . . . . . . . . . . 11
8382ifbid 3963 . . . . . . . . . 10
8483mpteq2dv 4539 . . . . . . . . 9
8584fveq2d 5875 . . . . . . . 8
86 suceq 4948 . . . . . . . . 9
8786fveq2d 5875 . . . . . . . 8
8885, 87eleq12d 2539 . . . . . . 7
8980, 88imbi12d 320 . . . . . 6
90 eleq1 2529 . . . . . . . 8
91 sseq2 3525 . . . . . . . 8
9290, 91anbi12d 710 . . . . . . 7
93 fveq2 5871 . . . . . . . . . . . 12
9493sseq2d 3531 . . . . . . . . . . 11
9594ifbid 3963 . . . . . . . . . 10
9695mpteq2dv 4539 . . . . . . . . 9
9796fveq2d 5875 . . . . . . . 8
98 suceq 4948 . . . . . . . . 9
9998fveq2d 5875 . . . . . . . 8
10097, 99eleq12d 2539 . . . . . . 7
10192, 100imbi12d 320 . . . . . 6
102 eleq1 2529 . . . . . . . 8
103 sseq2 3525 . . . . . . . 8
104102, 103anbi12d 710 . . . . . . 7
105 fveq2 5871 . . . . . . . . . . . 12
106105sseq2d 3531 . . . . . . . . . . 11
107106ifbid 3963 . . . . . . . . . 10
108107mpteq2dv 4539 . . . . . . . . 9
109108fveq2d 5875 . . . . . . . 8
110 suceq 4948 . . . . . . . . 9
111110fveq2d 5875 . . . . . . . 8
112109, 111eleq12d 2539 . . . . . . 7
113104, 112imbi12d 320 . . . . . 6
114 f1ocnvfv2 6183 . . . . . . . . . . . . 13
11555, 16, 114syl2anc 661 . . . . . . . . . . . 12
116115sseq2d 3531 . . . . . . . . . . 11
117116ifbid 3963 . . . . . . . . . 10
118117mpteq2dv 4539 . . . . . . . . 9
119118fveq2d 5875 . . . . . . . 8
120 cantnflem1.h . . . . . . . . 9
1218, 9, 10, 11, 12, 13, 14, 15, 2, 120cantnflem1d 8128 . . . . . . . 8
122119, 121eqeltrd 2545 . . . . . . 7
123 ss0 3816 . . . . . . . . . . . . . 14
124123fveq2d 5875 . . . . . . . . . . . . 13
125124sseq2d 3531 . . . . . . . . . . . 12
126125ifbid 3963 . . . . . . . . . . 11
127126mpteq2dv 4539 . . . . . . . . . 10
128127fveq2d 5875 . . . . . . . . 9
129 suceq 4948 . . . . . . . . . . 11
130123, 129syl 16 . . . . . . . . . 10
131130fveq2d 5875 . . . . . . . . 9
132128, 131eleq12d 2539 . . . . . . . 8
133132adantl 466 . . . . . . 7
134122, 133syl5ibcom 220 . . . . . 6
135 ordelon 4907 . . . . . . . . . . . . 13
13643, 59, 135sylancr 663 . . . . . . . . . . . 12
137136adantr 465 . . . . . . . . . . 11
13843a1i 11 . . . . . . . . . . . 12
139 ordelon 4907 . . . . . . . . . . . 12
140138, 139sylan 471 . . . . . . . . . . 11
141 onsseleq 4924 . . . . . . . . . . 11
142137, 140, 141syl2anc 661 . . . . . . . . . 10
143 sucelon 6652 . . . . . . . . . . . . . . 15
144140, 143sylibr 212 . . . . . . . . . . . . . 14
145 eloni 4893 . . . . . . . . . . . . . 14
146144, 145syl 16 . . . . . . . . . . . . 13
147 ordsssuc 4969 . . . . . . . . . . . . 13
148137, 146, 147syl2anc 661 . . . . . . . . . . . 12
149 ordtr 4897 . . . . . . . . . . . . . . . . 17
15043, 149mp1i 12 . . . . . . . . . . . . . . . 16
151 simprl 756 . . . . . . . . . . . . . . . 16
152 trsuc 4967 . . . . . . . . . . . . . . . 16
153150, 151, 152syl2anc 661 . . . . . . . . . . . . . . 15
154 simprr 757 . . . . . . . . . . . . . . 15
155153, 154jca 532 . . . . . . . . . . . . . 14
1569adantr 465 . . . . . . . . . . . . . . . . . . 19
15710adantr 465 . . . . . . . . . . . . . . . . . . 19
158 oecl 7206 . . . . . . . . . . . . . . . . . . 19
159156, 157, 158syl2anc 661 . . . . . . . . . . . . . . . . . 18
1608, 156, 157cantnff 8114 . . . . . . . . . . . . . . . . . . 19
1618, 9, 10cantnfs 8106 . . . . . . . . . . . . . . . . . . . . . . . . . 26
16212, 161mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25
163162simpld 459 . . . . . . . . . . . . . . . . . . . . . . . 24
164163ffvelrnda 6031 . . . . . . . . . . . . . . . . . . . . . . 23
1658, 9, 10, 11, 12, 13, 14, 15oemapvali 8124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
166165simp1d 1008 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
16722, 166ffvelrnd 6032 . . . . . . . . . . . . . . . . . . . . . . . . . 26
168 ne0i 3790 . . . . . . . . . . . . . . . . . . . . . . . . . 26
169167, 168syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
170 on0eln0 4938 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1719, 170syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
172169, 171mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24
173172adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
174164, 173ifcld 3984 . . . . . . . . . . . . . . . . . . . . . 22
175 eqid 2457 . . . . . . . . . . . . . . . . . . . . . 22
176174, 175fmptd 6055 . . . . . . . . . . . . . . . . . . . . 21
177 mptexg 6142 . . . . . . . . . . . . . . . . . . . . . . 23
17810, 177syl 16 . . . . . . . . . . . . . . . . . . . . . 22
179 funmpt 5629 . . . . . . . . . . . . . . . . . . . . . . 23
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
181162simprd 463 . . . . . . . . . . . . . . . . . . . . . 22
182 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
183 eqimss2 3556 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
184182, 183mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . 26
185 0ex 4582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
187163, 184, 10, 186suppssr 6950 . . . . . . . . . . . . . . . . . . . . . . . . 25
188187ifeq1d 3959 . . . . . . . . . . . . . . . . . . . . . . . 24
189 ifid 3978 . . . . . . . . . . . . . . . . . . . . . . . 24
190188, 189syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . 23
191190, 10suppss2 6953 . . . . . . . . . . . . . . . . . . . . . 22
192 fsuppsssupp 7865 . . . . . . . . . . . . . . . . . . . . . 22
193178, 180, 181, 191, 192syl22anc 1229 . . . . . . . . . . . . . . . . . . . . 21
1948, 9, 10cantnfs 8106 . . . . . . . . . . . . . . . . . . . . 21
195176, 193, 194mpbir2and 922 . . . . . . . . . . . . . . . . . . . 20
196195adantr 465 . . . . . . . . . . . . . . . . . . 19
197160, 196ffvelrnd 6032 . . . . . . . . . . . . . . . . . 18
198 onelon 4908 . . . . . . . . . . . . . . . . . 18
199159, 197, 198syl2anc 661 . . . . . . . . . . . . . . . . 17
20038adantr 465 . . . . . . . . . . . . . . . . . . 19
201 elnn 6710 . . . . . . . . . . . . . . . . . . 19