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

Theorem cantnfp1lem3 8120
Description: Lemma for cantnfp1 8121. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 1-Jul-2019.)
Hypotheses
Ref Expression
cantnfs.s
cantnfs.a
cantnfs.b
cantnfp1.g
cantnfp1.x
cantnfp1.y
cantnfp1.s
cantnfp1.f
cantnfp1.e
cantnfp1.o
cantnfp1.h
cantnfp1.k
cantnfp1.m
Assertion
Ref Expression
cantnfp1lem3
Distinct variable groups:   , , ,   , , ,   , ,   S, , ,   , , ,   , , ,   ,O,   , , ,   , , ,   , , ,

Proof of Theorem cantnfp1lem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfs.s . . 3
2 cantnfs.a . . 3
3 cantnfs.b . . 3
4 cantnfp1.o . . 3
5 cantnfp1.g . . . 4
6 cantnfp1.x . . . 4
7 cantnfp1.y . . . 4
8 cantnfp1.s . . . 4
9 cantnfp1.f . . . 4
101, 2, 3, 5, 6, 7, 8, 9cantnfp1lem1 8118 . . 3
11 cantnfp1.h . . 3
121, 2, 3, 4, 10, 11cantnfval 8108 . 2
13 cantnfp1.e . . . 4
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 8119 . . 3
1514fveq2d 5875 . 2
161, 2, 3, 4, 10cantnfcl 8107 . . . . . . 7
1716simprd 463 . . . . . 6
1814, 17eqeltrrd 2546 . . . . 5
19 peano2b 6716 . . . . 5
2018, 19sylibr 212 . . . 4
211, 2, 3, 4, 10, 11cantnfsuc 8110 . . . 4
2220, 21mpdan 668 . . 3
23 suppssdm 6931 . . . . . . . . . . . . . . . . 17
247adantr 465 . . . . . . . . . . . . . . . . . . . 20
251, 2, 3cantnfs 8106 . . . . . . . . . . . . . . . . . . . . . . 23
265, 25mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22
2726simpld 459 . . . . . . . . . . . . . . . . . . . . 21
2827ffvelrnda 6031 . . . . . . . . . . . . . . . . . . . 20
2924, 28ifcld 3984 . . . . . . . . . . . . . . . . . . 19
3029, 9fmptd 6055 . . . . . . . . . . . . . . . . . 18
31 fdm 5740 . . . . . . . . . . . . . . . . . 18
3230, 31syl 16 . . . . . . . . . . . . . . . . 17
3323, 32syl5sseq 3551 . . . . . . . . . . . . . . . 16
343, 33ssexd 4599 . . . . . . . . . . . . . . 15
3516simpld 459 . . . . . . . . . . . . . . 15
364oiiso 7983 . . . . . . . . . . . . . . 15
3734, 35, 36syl2anc 661 . . . . . . . . . . . . . 14
38 isof1o 6221 . . . . . . . . . . . . . 14
3937, 38syl 16 . . . . . . . . . . . . 13
40 f1ocnv 5833 . . . . . . . . . . . . 13
41 f1of 5821 . . . . . . . . . . . . 13
4239, 40, 413syl 20 . . . . . . . . . . . 12
43 iftrue 3947 . . . . . . . . . . . . . . . 16
4443, 9fvmptg 5954 . . . . . . . . . . . . . . 15
456, 7, 44syl2anc 661 . . . . . . . . . . . . . 14
46 onelon 4908 . . . . . . . . . . . . . . . . 17
472, 7, 46syl2anc 661 . . . . . . . . . . . . . . . 16
48 on0eln0 4938 . . . . . . . . . . . . . . . 16
4947, 48syl 16 . . . . . . . . . . . . . . 15
5013, 49mpbid 210 . . . . . . . . . . . . . 14
5145, 50eqnetrd 2750 . . . . . . . . . . . . 13
52 ffn 5736 . . . . . . . . . . . . . . 15
5330, 52syl 16 . . . . . . . . . . . . . 14
54 0ex 4582 . . . . . . . . . . . . . . 15
5554a1i 11 . . . . . . . . . . . . . 14
56 elsuppfn 6926 . . . . . . . . . . . . . 14
5753, 3, 55, 56syl3anc 1228 . . . . . . . . . . . . 13
586, 51, 57mpbir2and 922 . . . . . . . . . . . 12
5942, 58ffvelrnd 6032 . . . . . . . . . . 11
60 elssuni 4279 . . . . . . . . . . 11
6159, 60syl 16 . . . . . . . . . 10
624oicl 7975 . . . . . . . . . . . 12
63 ordelon 4907 . . . . . . . . . . . 12
6462, 59, 63sylancr 663 . . . . . . . . . . 11
65 nnon 6706 . . . . . . . . . . . 12
6620, 65syl 16 . . . . . . . . . . 11
67 ontri1 4917 . . . . . . . . . . 11
6864, 66, 67syl2anc 661 . . . . . . . . . 10
6961, 68mpbid 210 . . . . . . . . 9
70 sucidg 4961 . . . . . . . . . . . . . 14
7120, 70syl 16 . . . . . . . . . . . . 13
7271, 14eleqtrrd 2548 . . . . . . . . . . . 12
73 isorel 6222 . . . . . . . . . . . 12
7437, 72, 59, 73syl12anc 1226 . . . . . . . . . . 11
75 fvex 5881 . . . . . . . . . . . 12
7675epelc 4798 . . . . . . . . . . 11
77 fvex 5881 . . . . . . . . . . . 12
7877epelc 4798 . . . . . . . . . . 11
7974, 76, 783bitr3g 287 . . . . . . . . . 10
80 f1ocnvfv2 6183 . . . . . . . . . . . 12
8139, 58, 80syl2anc 661 . . . . . . . . . . 11
8281eleq2d 2527 . . . . . . . . . 10
8379, 82bitrd 253 . . . . . . . . 9
8469, 83mtbid 300 . . . . . . . 8
858sseld 3502 . . . . . . . . . 10
86 onss 6626 . . . . . . . . . . . . . . . 16
873, 86syl 16 . . . . . . . . . . . . . . 15
8833, 87sstrd 3513 . . . . . . . . . . . . . 14
894oif 7976 . . . . . . . . . . . . . . . 16
9089ffvelrni 6030 . . . . . . . . . . . . . . 15
9172, 90syl 16 . . . . . . . . . . . . . 14
9288, 91sseldd 3504 . . . . . . . . . . . . 13
93 eloni 4893 . . . . . . . . . . . . 13
9492, 93syl 16 . . . . . . . . . . . 12
95 ordn2lp 4903 . . . . . . . . . . . 12
9694, 95syl 16 . . . . . . . . . . 11
97 imnan 422 . . . . . . . . . . 11
9896, 97sylibr 212 . . . . . . . . . 10
9985, 98syld 44 . . . . . . . . 9
100 onelon 4908 . . . . . . . . . . . . 13
1013, 6, 100syl2anc 661 . . . . . . . . . . . 12
102 eloni 4893 . . . . . . . . . . . 12
103101, 102syl 16 . . . . . . . . . . 11
104 ordirr 4901 . . . . . . . . . . 11
105103, 104syl 16 . . . . . . . . . 10
106 elsni 4054 . . . . . . . . . . . 12
107106eleq2d 2527 . . . . . . . . . . 11
108107notbid 294 . . . . . . . . . 10
109105, 108syl5ibrcom 222 . . . . . . . . 9
110 eldifi 3625 . . . . . . . . . . . . . . 15
111110adantl 466 . . . . . . . . . . . . . 14
1127adantr 465 . . . . . . . . . . . . . . 15
113 fvex 5881 . . . . . . . . . . . . . . 15
114 ifexg 4011 . . . . . . . . . . . . . . 15
115112, 113, 114sylancl 662 . . . . . . . . . . . . . 14
116 eqeq1 2461 . . . . . . . . . . . . . . . 16
117 fveq2 5871 . . . . . . . . . . . . . . . 16
118116, 117ifbieq2d 3966 . . . . . . . . . . . . . . 15
119118, 9fvmptg 5954 . . . . . . . . . . . . . 14
120111, 115, 119syl2anc 661 . . . . . . . . . . . . 13
121 eldifn 3626 . . . . . . . . . . . . . . . 16
122121adantl 466 . . . . . . . . . . . . . . 15
123 elsn 4043 . . . . . . . . . . . . . . . 16
124 elun2 3671 . . . . . . . . . . . . . . . 16
125123, 124sylbir 213 . . . . . . . . . . . . . . 15
126122, 125nsyl 121 . . . . . . . . . . . . . 14
127126iffalsed 3952 . . . . . . . . . . . . 13
128 ssun1 3666 . . . . . . . . . . . . . . . 16
129 sscon 3637 . . . . . . . . . . . . . . . 16
130128, 129ax-mp 5 . . . . . . . . . . . . . . 15
131130sseli 3499 . . . . . . . . . . . . . 14
132 ssid 3522 . . . . . . . . . . . . . . . 16
133132a1i 11 . . . . . . . . . . . . . . 15
13427, 133, 3, 13suppssr 6950 . . . . . . . . . . . . . 14
135131, 134sylan2 474 . . . . . . . . . . . . 13
136120, 127, 1353eqtrd 2502 . . . . . . . . . . . 12
13730, 136suppss 6949 . . . . . . . . . . 11
138137, 91sseldd 3504 . . . . . . . . . 10
139 elun 3644 . . . . . . . . . 10
140138, 139sylib 196 . . . . . . . . 9
14199, 109, 140mpjaod 381 . . . . . . . 8
142 ioran 490 . . . . . . . 8
14384, 141, 142sylanbrc 664 . . . . . . 7
144 ordtri3 4919 . . . . . . . 8
14594, 103, 144syl2anc 661 . . . . . . 7
146143, 145mpbird 232 . . . . . 6
147146oveq2d 6312 . . . . 5
148146fveq2d 5875 . . . . . 6
149148, 45eqtrd 2498 . . . . 5
150147, 149oveq12d 6314 . . . 4
151 nnord 6708 . . . . . . . . 9
15220, 151syl 16 . . . . . . . 8
153 sssucid 4960 . . . . . . . . . 10
154153, 14syl5sseqr 3552 . . . . . . . . 9
155 f1ofo 5828 . . . . . . . . . . . . 13
15639, 155syl 16 . . . . . . . . . . . 12
157 foima 5805 . . . . . . . . . . . 12
158156, 157syl 16 . . . . . . . . . . 11
159 ffn 5736 . . . . . . . . . . . . . 14
16089, 159ax-mp 5 . . . . . . . . . . . . 13
161 fnsnfv 5933 . . . . . . . . . . . . 13
162160, 72, 161sylancr 663 . . . . . . . . . . . 12
163146sneqd 4041 . . . . . . . . . . . 12
164162, 163eqtr3d 2500 . . . . . . . . . . 11
165158, 164difeq12d 3622 . . . . . . . . . 10
166 ordirr 4901 . . . . . . . . . . . . . . . . 17
167152, 166syl 16 . . . . . . . . . . . . . . . 16
168 disjsn 4090 . . . . . . . . . . . . . . . 16
169167, 168sylibr 212 . . . . . . . . . . . . . . 15
170 disj3 3871 . . . . . . . . . . . . . . 15
171169, 170sylib 196 . . . . . . . . . . . . . 14
172 difun2 3907 . . . . . . . . . . . . . 14
173171, 172syl6eqr 2516 . . . . . . . . . . . . 13
174 df-suc 4889 . . . . . . . . . . . . . . 15
17514, 174syl6eq 2514 . . . . . . . . . . . . . 14
176175difeq1d 3620 . . . . . . . . . . . . 13
177173, 176eqtr4d 2501 . . . . . . . . . . . 12
178177imaeq2d 5342 . . . . . . . . . . 11
179 dff1o3 5827 . . . . . . . . . . . . 13
180179simprbi 464 . . . . . . . . . . . 12
181 imadif 5668 . . . . . . . . . . . 12
18239, 180, 1813syl 20 . . . . . . . . . . 11
183178, 182eqtrd 2498 . . . . . . . . . 10
1848, 105ssneldd 3506 . . . . . . . . . . . . 13
185 disjsn 4090 . . . . . . . . . . . . 13
186184, 185sylibr 212 . . . . . . . . . . . 12
187 fvex 5881 . . . . . . . . . . . . . . . . . . . . 21
188 dif1o 7169 . . . . . . . . . . . . . . . . . . . . 21
189187, 188mpbiran 918 . . . . . . . . . . . . . . . . . . . 20
190 ffn 5736 . . . . . . . . . . . . . . . . . . . . . . . . 25
19127, 190syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
192 elsuppfn 6926 . . . . . . . . . . . . . . . . . . . . . . . 24
193191, 3, 55, 192syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23
194189a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
195194bicomd 201 . . . . . . . . . . . . . . . . . . . . . . . 24
196195anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . 23
197193, 196bitrd 253 . . . . . . . . . . . . . . . . . . . . . 22
1988sseld 3502 . . . . . . . . . . . . . . . . . . . . . 22
199197, 198sylbird 235 . . . . . . . . . . . . . . . . . . . . 21
2006, 199mpand 675 . . . . . . . . . . . . . . . . . . . 20
201189, 200syl5bir 218 . . . . . . . . . . . . . . . . . . 19
202201necon1bd 2675 . . . . . . . . . . . . . . . . . 18
203105, 202mpd 15 . . . . . . . . . . . . . . . . 17
204203adantr 465 . . . . . . . . . . . . . . . 16
205 fveq2 5871 . . . . . . . . . . . . . . . . 17
206205eqeq1d 2459 . . . . . . . . . . . . . . . 16
207204, 206syl5ibrcom 222 . . . . . . . . . . . . . . 15
208 eldifi 3625 . . . . . . . . . . . . . . . . . . 19
209208adantl 466 . . . . . . . . . . . . . . . . . 18
2107adantr 465 . . . . . . . . . . . . . . . . . . 19
211210, 113, 114sylancl 662 . . . . . . . . . . . . . . . . . 18
212209, 211, 119syl2anc 661 . . . . . . . . . . . . . . . . 17
213 ssid 3522 . . . . . . . . . . . . . . . . . . 19
214213a1i 11 . . . . . . . . . . . . . . . . . 18
21530, 214, 3, 13suppssr 6950 . . . . . . . . . . . . . . . . 17
216212, 215eqtr3d 2500 . . . . . . . . . . . . . . . 16
217 iffalse 3950 . . . . . . . . . . . . . . . . 17
218217eqeq1d 2459 . . . . . . . . . . . . . . . 16
219216, 218syl5ibcom 220 . . . . . . . . . . . . . . 15
220207, 219pm2.61d 158 . . . . . . . . . . . . . 14
22127, 220suppss 6949 . . . . . . . . . . . . 13
222 reldisj 3870 . . . . . . . . . . . . 13
223221, 222syl 16 . . . . . . . . . . . 12
224186, 223mpbid 210 . . . . . . . . . . 11
225 uncom 3647 . . . . . . . . . . . . 13
226137, 225syl6sseq 3549 . . . . . . . . . . . 12
227 ssundif 3911 . . . . . . . . . . . 12
228226, 227sylib 196 . . . . . . . . . . 11
229224, 228eqssd 3520 . . . . . . . . . 10
230165, 183, 2293eqtr4rd 2509 . . . . . . . . 9
231 isores3 6231 . . . . . . . . 9
23237, 154, 230, 231syl3anc 1228 . . . . . . . 8
233 cantnfp1.k . . . . . . . . . . 11
2341, 2, 3, 233, 5cantnfcl 8107 . . . . . . . . . 10
235234simpld 459 . . . . . . . . 9
236 epse 4867 . . . . . . . . 9
237233oieu 7985 . . . . . . . . 9
238235, 236, 237sylancl 662 . . . . . . . 8
239152, 232, 238mpbi2and 921 . . . . . . 7
240239simpld 459 . . . . . 6
241240fveq2d 5875 . . . . 5
242 eleq1 2529 . . . . . . . . . 10
243 fveq2 5871 . . . . . . . . . . 11
244 fveq2 5871 . . . . . . . . . . . 12
245 cantnfp1.m . . . . . . . . . . . . . 14
246245seqom0g 7140 . . . . . . . . . . . . 13
24754, 246ax-mp 5 . . . . . . . . . . . 12
248244, 247syl6eq 2514 . . . . . . . . . . 11
249243, 248eqeq12d 2479 . . . . . . . . . 10
250242, 249imbi12d 320 . . . . . . . . 9
251250imbi2d 316 . . . . . . . 8
252 eleq1 2529 . . . . . . . . . 10
253 fveq2 5871 . . . . . . . . . . 11
254 fveq2 5871 . . . . . . . . . . 11
255253, 254eqeq12d 2479 . . . . . . . . . 10
256252, 255imbi12d 320 . . . . . . . . 9
257256imbi2d 316 . . . . . . . 8
258 eleq1 2529 . . . . . . . . . 10
259 fveq2 5871 . . . . . . . . . . 11