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

Theorem cantnflem1 8212
 Description: Lemma for cantnf 8216. 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.) (Revised by AV, 2-Jul-2019.)
Hypotheses
Ref Expression
cantnfs.s CNF
cantnfs.a
cantnfs.b
oemapval.t
oemapval.f
oemapval.g
oemapvali.r
oemapvali.x
cantnflem1.o OrdIso supp
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 ovex 6336 . . . . . 6 supp
2 cantnflem1.o . . . . . . 7 OrdIso supp
32oion 8069 . . . . . 6 supp
41, 3mp1i 13 . . . . 5
5 uniexg 6607 . . . . 5
6 sucidg 5508 . . . . 5
74, 5, 63syl 18 . . . 4
8 cantnfs.s . . . . . . . . . 10 CNF
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 8208 . . . . . . . . 9 supp
17 n0i 3727 . . . . . . . . 9 supp supp
1816, 17syl 17 . . . . . . . 8 supp
19 suppssdm 6946 . . . . . . . . . . . 12 supp
208, 9, 10cantnfs 8189 . . . . . . . . . . . . . . 15 finSupp
2113, 20mpbid 215 . . . . . . . . . . . . . 14 finSupp
2221simpld 466 . . . . . . . . . . . . 13
23 fdm 5745 . . . . . . . . . . . . 13
2422, 23syl 17 . . . . . . . . . . . 12
2519, 24syl5sseq 3466 . . . . . . . . . . 11 supp
2610, 25ssexd 4543 . . . . . . . . . 10 supp
278, 9, 10, 2, 13cantnfcl 8190 . . . . . . . . . . 11 supp
2827simpld 466 . . . . . . . . . 10 supp
292oien 8071 . . . . . . . . . 10 supp supp supp
3026, 28, 29syl2anc 673 . . . . . . . . 9 supp
31 breq1 4398 . . . . . . . . . 10 supp supp
32 ensymb 7635 . . . . . . . . . . 11 supp supp
33 en0 7650 . . . . . . . . . . 11 supp supp
3432, 33bitri 257 . . . . . . . . . 10 supp supp
3531, 34syl6bb 269 . . . . . . . . 9 supp supp
3630, 35syl5ibcom 228 . . . . . . . 8 supp
3718, 36mtod 182 . . . . . . 7
3827simprd 470 . . . . . . . 8
39 nnlim 6724 . . . . . . . 8
4038, 39syl 17 . . . . . . 7
41 ioran 498 . . . . . . 7
4237, 40, 41sylanbrc 677 . . . . . 6
432oicl 8062 . . . . . . 7
44 unizlim 5546 . . . . . . 7
4543, 44mp1i 13 . . . . . 6
4642, 45mtbird 308 . . . . 5
47 orduniorsuc 6676 . . . . . . 7
4843, 47mp1i 13 . . . . . 6
4948ord 384 . . . . 5
5046, 49mpd 15 . . . 4
517, 50eleqtrrd 2552 . . 3
522oiiso 8070 . . . . . . . 8 supp supp supp
5326, 28, 52syl2anc 673 . . . . . . 7 supp
54 isof1o 6234 . . . . . . 7 supp supp
5553, 54syl 17 . . . . . 6 supp
56 f1ocnv 5840 . . . . . 6 supp supp
57 f1of 5828 . . . . . 6 supp supp
5855, 56, 573syl 18 . . . . 5 supp
5958, 16ffvelrnd 6038 . . . 4
60 elssuni 4219 . . . 4
6159, 60syl 17 . . 3
6250, 38eqeltrrd 2550 . . . . 5
63 peano2b 6727 . . . . 5
6462, 63sylibr 217 . . . 4
65 eleq1 2537 . . . . . . . 8
66 sseq2 3440 . . . . . . . 8
6765, 66anbi12d 725 . . . . . . 7
68 fveq2 5879 . . . . . . . . . . . 12
6968sseq2d 3446 . . . . . . . . . . 11
7069ifbid 3894 . . . . . . . . . 10
7170mpteq2dv 4483 . . . . . . . . 9
7271fveq2d 5883 . . . . . . . 8 CNF CNF
73 suceq 5495 . . . . . . . . 9
7473fveq2d 5883 . . . . . . . 8
7572, 74eleq12d 2543 . . . . . . 7 CNF CNF
7667, 75imbi12d 327 . . . . . 6 CNF CNF
7776imbi2d 323 . . . . 5 CNF CNF
78 eleq1 2537 . . . . . . . 8
79 sseq2 3440 . . . . . . . 8
8078, 79anbi12d 725 . . . . . . 7
81 fveq2 5879 . . . . . . . . . . . 12
8281sseq2d 3446 . . . . . . . . . . 11
8382ifbid 3894 . . . . . . . . . 10
8483mpteq2dv 4483 . . . . . . . . 9
8584fveq2d 5883 . . . . . . . 8 CNF CNF
86 suceq 5495 . . . . . . . . 9
8786fveq2d 5883 . . . . . . . 8
8885, 87eleq12d 2543 . . . . . . 7 CNF CNF
8980, 88imbi12d 327 . . . . . 6 CNF CNF
90 eleq1 2537 . . . . . . . 8
91 sseq2 3440 . . . . . . . 8
9290, 91anbi12d 725 . . . . . . 7
93 fveq2 5879 . . . . . . . . . . . 12
9493sseq2d 3446 . . . . . . . . . . 11
9594ifbid 3894 . . . . . . . . . 10
9695mpteq2dv 4483 . . . . . . . . 9
9796fveq2d 5883 . . . . . . . 8 CNF CNF
98 suceq 5495 . . . . . . . . 9
9998fveq2d 5883 . . . . . . . 8
10097, 99eleq12d 2543 . . . . . . 7 CNF CNF
10192, 100imbi12d 327 . . . . . 6 CNF CNF
102 eleq1 2537 . . . . . . . 8
103 sseq2 3440 . . . . . . . 8
104102, 103anbi12d 725 . . . . . . 7
105 fveq2 5879 . . . . . . . . . . . 12
106105sseq2d 3446 . . . . . . . . . . 11
107106ifbid 3894 . . . . . . . . . 10
108107mpteq2dv 4483 . . . . . . . . 9
109108fveq2d 5883 . . . . . . . 8 CNF CNF
110 suceq 5495 . . . . . . . . 9
111110fveq2d 5883 . . . . . . . 8
112109, 111eleq12d 2543 . . . . . . 7 CNF CNF
113104, 112imbi12d 327 . . . . . 6 CNF CNF
114 f1ocnvfv2 6194 . . . . . . . . . . . . 13 supp supp
11555, 16, 114syl2anc 673 . . . . . . . . . . . 12
116115sseq2d 3446 . . . . . . . . . . 11
117116ifbid 3894 . . . . . . . . . 10
118117mpteq2dv 4483 . . . . . . . . 9
119118fveq2d 5883 . . . . . . . 8 CNF CNF
120 cantnflem1.h . . . . . . . . 9 seq𝜔
1218, 9, 10, 11, 12, 13, 14, 15, 2, 120cantnflem1d 8211 . . . . . . . 8 CNF
122119, 121eqeltrd 2549 . . . . . . 7 CNF
123 ss0 3768 . . . . . . . . . . . . . 14
124123fveq2d 5883 . . . . . . . . . . . . 13
125124sseq2d 3446 . . . . . . . . . . . 12
126125ifbid 3894 . . . . . . . . . . 11
127126mpteq2dv 4483 . . . . . . . . . 10
128127fveq2d 5883 . . . . . . . . 9 CNF CNF
129 suceq 5495 . . . . . . . . . . 11
130123, 129syl 17 . . . . . . . . . 10
131130fveq2d 5883 . . . . . . . . 9
132128, 131eleq12d 2543 . . . . . . . 8 CNF CNF
133132adantl 473 . . . . . . 7 CNF CNF
134122, 133syl5ibcom 228 . . . . . 6 CNF
135 ordelon 5454 . . . . . . . . . . . . 13
13643, 59, 135sylancr 676 . . . . . . . . . . . 12
137136adantr 472 . . . . . . . . . . 11
13843a1i 11 . . . . . . . . . . . 12
139 ordelon 5454 . . . . . . . . . . . 12
140138, 139sylan 479 . . . . . . . . . . 11
141 onsseleq 5471 . . . . . . . . . . 11
142137, 140, 141syl2anc 673 . . . . . . . . . 10
143 sucelon 6663 . . . . . . . . . . . . . . 15
144140, 143sylibr 217 . . . . . . . . . . . . . 14
145 eloni 5440 . . . . . . . . . . . . . 14
146144, 145syl 17 . . . . . . . . . . . . 13
147 ordsssuc 5516 . . . . . . . . . . . . 13
148137, 146, 147syl2anc 673 . . . . . . . . . . . 12
149 ordtr 5444 . . . . . . . . . . . . . . . . 17
15043, 149mp1i 13 . . . . . . . . . . . . . . . 16
151 simprl 772 . . . . . . . . . . . . . . . 16
152 trsuc 5514 . . . . . . . . . . . . . . . 16
153150, 151, 152syl2anc 673 . . . . . . . . . . . . . . 15
154 simprr 774 . . . . . . . . . . . . . . 15
155153, 154jca 541 . . . . . . . . . . . . . 14
1569adantr 472 . . . . . . . . . . . . . . . . . . 19
15710adantr 472 . . . . . . . . . . . . . . . . . . 19
158 oecl 7257 . . . . . . . . . . . . . . . . . . 19
159156, 157, 158syl2anc 673 . . . . . . . . . . . . . . . . . 18
1608, 156, 157cantnff 8197 . . . . . . . . . . . . . . . . . . 19 CNF
1618, 9, 10cantnfs 8189 . . . . . . . . . . . . . . . . . . . . . . . . . 26 finSupp
16212, 161mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . 25 finSupp
163162simpld 466 . . . . . . . . . . . . . . . . . . . . . . . 24
164163ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . 23
1658, 9, 10, 11, 12, 13, 14, 15oemapvali 8207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
166165simp1d 1042 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
16722, 166ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . . 26
168 ne0i 3728 . . . . . . . . . . . . . . . . . . . . . . . . . 26
169167, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25
170 on0eln0 5485 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1719, 170syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25
172169, 171mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . 24
173172adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
174164, 173ifcld 3915 . . . . . . . . . . . . . . . . . . . . . 22
175 eqid 2471 . . . . . . . . . . . . . . . . . . . . . 22
176174, 175fmptd 6061 . . . . . . . . . . . . . . . . . . . . 21
177 mptexg 6151 . . . . . . . . . . . . . . . . . . . . . . 23
17810, 177syl 17 . . . . . . . . . . . . . . . . . . . . . 22
179 funmpt 5625 . . . . . . . . . . . . . . . . . . . . . . 23
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
181162simprd 470 . . . . . . . . . . . . . . . . . . . . . 22 finSupp
182 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 supp supp
183 eqimss2 3471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 supp supp supp supp
184182, 183mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26 supp supp
185 0ex 4528 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
187163, 184, 10, 186suppssr 6965 . . . . . . . . . . . . . . . . . . . . . . . . 25 supp
188187ifeq1d 3890 . . . . . . . . . . . . . . . . . . . . . . . 24 supp
189 ifid 3909 . . . . . . . . . . . . . . . . . . . . . . . 24
190188, 189syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . 23 supp
191190, 10suppss2 6968 . . . . . . . . . . . . . . . . . . . . . 22 supp supp
192 fsuppsssupp 7917 . . . . . . . . . . . . . . . . . . . . . 22 finSupp supp supp finSupp
193178, 180, 181, 191, 192syl22anc 1293 . . . . . . . . . . . . . . . . . . . . 21 finSupp
1948, 9, 10cantnfs 8189 . . . . . . . . . . . . . . . . . . . . 21 finSupp
195176, 193, 194mpbir2and 936 . . . . . . . . . . . . . . . . . . . 20
196195adantr 472 . . . . . . . . . . . . . . . . . . 19
197160, 196ffvelrnd 6038 . . . . . . . . . . . . . . . . . 18 CNF
198 onelon 5455 . . . . . . . . . . . . . . . . . 18 CNF CNF
199159, 197, 198syl2anc 673 . . . . . . . . . . . . . . . . 17 CNF
20038adantr 472 . . . . . . . . . . . . . . . . . . 19
201 elnn 6721 . . . . . . . . . . . . . . . . . . 19
202151, 200, 201syl2anc 673 . . . . . . . . . . . . . . . . . 18
203120cantnfvalf 8188 . . . . . . . . . . . . . . . . . . 19
204203ffvelrni 6036 . . . . . . . . . . . . . . . . . 18
205202, 204syl 17 . . . . . . . . . . . . . . . . 17
20625adantr 472 . . . . . . . . . . . . . . . . . . . . 21 supp
2072oif 8063 . . . . . . . . . . . . . . . . . . . . . . 23 supp
208207ffvelrni 6036 . . . . . . . . . . . . . . . . . . . . . 22 supp
209151, 208syl 17 . . . . . . . . . . . . . . . . . . . . 21 supp
210206, 209sseldd 3419 . . . . . . . . . . . . . . . . . . . 20
211 onelon 5455 . . . . . . . . . . . . . . . . . . . 20
212157, 210, 211syl2anc 673 . . . . . . . . . . . . . . . . . . 19
213 oecl 7257 . . . . . . . . . . . . . . . . . . 19
214156, 212, 213syl2anc 673 . . . . . . . . . . . . . . . . . 18
215163adantr 472 . . . . . . . . . . . . . . . . . . . 20
216215, 210ffvelrnd 6038 . . . . . . . . . . . . . . . . . . 19
217 onelon 5455 . . . . . . . . . . . . . . . . . . 19
218156, 216, 217syl2anc 673 . . . . . . . . . . . . . . . . . 18
219 omcl 7256 . . . . . . . . . . . . . . . . . 18
220214, 218, 219syl2anc 673 . . . . . . . . . . . . . . . . 17
221 oaord 7266 . . . . . . . . . . . . . . . . 17 CNF CNF CNF
222199, 205, 220, 221syl3anc 1292 . . . . . . . . . . . . . . . 16 CNF CNF
223 ifeq1 3876 . . . . . . . . . . . . . . . . . . . . . . 23
224 ifid 3909 . . . . . . . . . . . . . . . . . . . . . . 23
225223, 224syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . 22
226 ifeq1 3876 . . . . . . . . . . . . . . . . . . . . . . 23
227 ifid 3909 . . . . . . . . . . . . . . . . . . . . . . 23
228226, 227syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . 22
229225, 228eqeq12d 2486 . . . . . . . . . . . . . . . . . . . . 21
230 onss 6636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
23110, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
232231sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
233232adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26
234212adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
235 onsseleq 5471 . . . . . . . . . . . . . . . . . . . . . . . . . 26
236233, 234, 235syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . 25
237236adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
238233adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
239207ffvelrni 6036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 supp
240153, 239syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 supp
241206, 240sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
242 onelon 5455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
243157, 241, 242syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
244243ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
245 onsssuc 5517 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
246238, 244, 245syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
247 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
248247sucid 5509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
24953adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 supp
250 isorel 6235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 supp
251249, 153, 151, 250syl12anc 1290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
252247sucex 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
253252epelc 4752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
254 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
255254epelc 4752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
256251, 253, 2553bitr3g 295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
257248, 256mpbii 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
258 eloni 5440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
259212, 258syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
260 ordelsuc 6666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
261243, 259, 260syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
262257, 261mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
263262ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
264263sseld 3417 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
265246, 264sylbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . 26
266 simprr 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
267249ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 supp
268267, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 supp
2698, 9, 10, 11, 12, 13, 14, 15, 2cantnflem1c 8210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 supp
270 f1ocnvfv2 6194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 supp supp
271268, 269, 270syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
272266, 271eleqtrrd 2552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
273153ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
274268, 56, 573syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 supp
275274, 269ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
276 isorel 6235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 supp
277267, 273, 275, 276syl12anc 1290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
278 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
279278epelc 4752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
280 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
281280epelc 4752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
282277, 279, 2813bitr3g 295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
283272, 282mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
284 ordelon 5454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
28543, 275, 284sylancr 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
286 eloni 5440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
287285, 286syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
288 ordelsuc 6666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
289283, 287, 288syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
290283, 289mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
291151ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
29243, 291, 139sylancr 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
293 ontri1 5464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
294292, 285, 293syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
295290, 294mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
296 isorel 6235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 supp
297267, 275, 291, 296syl12anc 1290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
298252epelc 4752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
299254epelc 4752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
300297, 298, 2993bitr3g 295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
301271eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
302300, 301bitrd 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
303295, 302mtbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
304303expr 626 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
305304con2d 119 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
306 ontri1 5464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
307238, 244, 306syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
308305, 307sylibrd 242 . . . . . . . . . . . . . . . . . . . . . . . . . 26
309265, 308impbid 195 . . . . . . . . . . . . . . . . . . . . . . . . 25
310309orbi1d 717 . . . . . . . . . . . . . . . . . . . . . . . 24
311237, 310bitr4d 264 . . . . . . . . . . . . . . . . . . . . . . 23
312 orcom 394 . . . . . . . . . . . . . . . . . . . . . . 23
313311, 312syl6bb 269 . . . . . . . . . . . . . . . . . . . . . 22
314313ifbid 3894 . . . . . . . . . . . . . . . . . . . . 21
315 eqidd 2472 . . . . . . . . . . . . . . . . . . . . 21
316229, 314, 315pm2.61ne 2728 . . . . . . . . . . . . . . . . . . . 20
317316mpteq2dva 4482 . . . . . . . . . . . . . . . . . . 19
318317fveq2d 5883 . . . . . . . . . . . . . . . . . 18 CNF CNF
319 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
320319, 185ifex 3940 . . . . . . . . . . . . . . . . . . . . . . . . . 26
321320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
322321ralrimivw 2810 . . . . . . . . . . . . . . . . . . . . . . . 24
323175fnmpt 5714 . . . . . . . . . . . . . . . . . . . . . . . 24
324322, 323syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
325185a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
326 suppvalfn 6940 . . . . . . . . . . . . . . . . . . . . . . . 24 supp
327 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . . 25
328 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . . 25
329 nffvmpt1 5887 . . . . . . . . . . . . . . . . . . . . . . . . . 26
330 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . . . 26
331329, 330nfne 2742 . . . . . . . . . . . . . . . . . . . . . . . . 25
332 nfv 1769 . . . . . . . . . . . . . . . . . . . . . . . . 25
333 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . 26
334333neeq1d 2702 . . . . . . . . . . . . . . . . . . . . . . . . 25
335327, 328, 331, 332, 334cbvrab 3029 . . . . . . . . . . . . . . . . . . . . . . . 24
336326, 335syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . 23 supp
337324, 157, 325, 336syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . 22 supp
338 eqidd 2472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
339320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
340338, 339fvmpt2d 5974 . . . . . . . . . . . . . . . . . . . . . . . . 25
341340neeq1d 2702 . . . . . . . . . . . . . . . . . . . . . . . 24
342339biantrurd 516 . . . . . . . . . . . . . . . . . . . . . . . . 25
343 dif1o 7220 . . . . . . . . . . . . . . . . . . . . . . . . 25
344342, 343syl6bbr 271 . . . . . . . . . . . . . . . . . . . . . . . 24
345341, 344bitrd 261 . . . . . . . . . . . . . . . . . . . . . . 23
346345rabbidva 3021 . . . . . . . . . . . . . . . . . . . . . 22
347337, 346eqtrd 2505 . . . . . . . . . . . . . . . . . . . . 21 supp
348320, 343mpbiran 932 . . . . . . . . . . . . . . . . . . . . . . . 24
349 ifeq1 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
350349, 189syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
351350necon3i 2675 . . . . . . . . . . . . . . . . . . . . . . . . . 26
352 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
353352necon1ai 2670 . . . . . . . . . . . . . . . . . . . . . . . . . 26
354351, 353jca 541 . . . . . . . . . . . . . . . . . . . . . . . . 25
355265expimpd 614 . . . . . . . . . . . . . . . . . . . . . . . . 25
356354, 355syl5 32 . . . . . . . . . . . . . . . . . . . . . . . 24
357348, 356syl5bi 225 . . . . . . . . . . . . . . . . . . . . . . 23
3583573impia 1228 . . . . . . . . . . . . . . . . . . . . . 22
359358rabssdv 3495 . . . . . . . . . . . . . . . . . . . . 21
360347, 359eqsstrd 3452 . . . . . . . . . . . . . . . . . . . 20 supp
361 eqeq1 2475 . . . . . . . . . . . . . . . . . . . . . . . 24
362 sseq1 3439 . . . . . . . . . . . . . . . . . . . . . . . 24
363361, 362orbi12d 724 . . . . . . . . . . . . . . . . . . . . . . 23
364 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23
365363, 364ifbieq1d 3895 . . . . . . . . . . . . . . . . . . . . . 22
366365cbvmptv 4488 . . . . . . . . . . . . . . . . . . . . 21
367 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25
368367adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24
369368ifeq1da 3902 . . . . . . . . . . . . . . . . . . . . . . 23
370362, 364ifbieq1d 3895 . . . . . . . . . . . . . . . . . . . . . . . . . 26
371 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
372371, 185ifex 3940 . . . . . . . . . . . . . . . . . . . . . . . . . 26
373370, 175, 372fvmpt 5963 . . . . . . . . . . . . . . . . . . . . . . . . 25
374373ifeq2d 3891 . . . . . . . . . . . . . . . . . . . . . . . 24
375 ifor 3919 . . . . . . . . . . . . . . . . . . . . . . . 24
376374, 375syl6eqr 2523 . . . . . . . . . . . . . . . . . . . . . . 23
377369, 376eqtr3d 2507 . . . . . . . . . . . . . . . . . . . . . 22
378377mpteq2ia 4478 . . . . . . . . . . . . . . . . . . . . 21
379366, 378eqtr4i 2496 . . . . . . . . . . . . . . . . . . . 20
3808, 156, 157, 196, 210, 216, 360, 379cantnfp1 8204 . . . . . . . . . . . . . . . . . . 19 CNF CNF
381380simprd 470 . . . . . . . . . . . . . . . . . 18