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

Theorem cantnfp1lem3OLD 8146
Description: Lemma for cantnfp1OLD 8147. (Contributed by Mario Carneiro, 28-May-2015.) Obsolete version of cantnfp1lem3 8120 as of 1-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
cantnfsOLD.1
cantnfsOLD.2
cantnfsOLD.3
cantnfp1OLD.4
cantnfp1OLD.5
cantnfp1OLD.6
cantnfp1OLD.7
cantnfp1OLD.f
cantnfp1OLD.8
cantnfp1OLD.o
cantnfp1OLD.h
cantnfp1OLD.k
cantnfp1OLD.m
Assertion
Ref Expression
cantnfp1lem3OLD
Distinct variable groups:   , , ,   , , ,   , ,   S, , ,   , , ,   , , ,   ,O,   , , ,   , , ,   , , ,

Proof of Theorem cantnfp1lem3OLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfsOLD.1 . . 3
2 cantnfsOLD.2 . . 3
3 cantnfsOLD.3 . . 3
4 cantnfp1OLD.o . . 3
5 cantnfp1OLD.4 . . . 4
6 cantnfp1OLD.5 . . . 4
7 cantnfp1OLD.6 . . . 4
8 cantnfp1OLD.7 . . . 4
9 cantnfp1OLD.f . . . 4
101, 2, 3, 5, 6, 7, 8, 9cantnfp1lem1OLD 8144 . . 3
11 cantnfp1OLD.h . . 3
121, 2, 3, 4, 10, 11cantnfvalOLD 8138 . 2
13 cantnfp1OLD.8 . . . 4
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2OLD 8145 . . 3
1514fveq2d 5875 . 2
161, 2, 3, 4, 10cantnfclOLD 8137 . . . . . . 7
1716simprd 463 . . . . . 6
1814, 17eqeltrrd 2546 . . . . 5
19 peano2b 6716 . . . . 5
2018, 19sylibr 212 . . . 4
211, 2, 3, 4, 10, 11cantnfsucOLD 8140 . . . 4
2220, 21mpdan 668 . . 3
23 cnvimass 5362 . . . . . . . . . . . . . . . . 17
247adantr 465 . . . . . . . . . . . . . . . . . . . 20
251, 2, 3cantnfsOLD 8136 . . . . . . . . . . . . . . . . . . . . . . 23
265, 25mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22
2726simpld 459 . . . . . . . . . . . . . . . . . . . . 21
2827ffvelrnda 6031 . . . . . . . . . . . . . . . . . . . 20
29 ifcl 3983 . . . . . . . . . . . . . . . . . . . 20
3024, 28, 29syl2anc 661 . . . . . . . . . . . . . . . . . . 19
3130, 9fmptd 6055 . . . . . . . . . . . . . . . . . 18
32 fdm 5740 . . . . . . . . . . . . . . . . . 18
3331, 32syl 16 . . . . . . . . . . . . . . . . 17
3423, 33syl5sseq 3551 . . . . . . . . . . . . . . . 16
353, 34ssexd 4599 . . . . . . . . . . . . . . 15
3616simpld 459 . . . . . . . . . . . . . . 15
374oiiso 7983 . . . . . . . . . . . . . . 15
3835, 36, 37syl2anc 661 . . . . . . . . . . . . . 14
39 isof1o 6221 . . . . . . . . . . . . . 14
4038, 39syl 16 . . . . . . . . . . . . 13
41 f1ocnv 5833 . . . . . . . . . . . . 13
42 f1of 5821 . . . . . . . . . . . . 13
4340, 41, 423syl 20 . . . . . . . . . . . 12
44 iftrue 3947 . . . . . . . . . . . . . . . . 17
4544, 9fvmptg 5954 . . . . . . . . . . . . . . . 16
466, 7, 45syl2anc 661 . . . . . . . . . . . . . . 15
47 onelon 4908 . . . . . . . . . . . . . . . . . 18
482, 7, 47syl2anc 661 . . . . . . . . . . . . . . . . 17
49 on0eln0 4938 . . . . . . . . . . . . . . . . 17
5048, 49syl 16 . . . . . . . . . . . . . . . 16
5113, 50mpbid 210 . . . . . . . . . . . . . . 15
5246, 51eqnetrd 2750 . . . . . . . . . . . . . 14
53 fvex 5881 . . . . . . . . . . . . . . 15
54 dif1o 7169 . . . . . . . . . . . . . . 15
5553, 54mpbiran 918 . . . . . . . . . . . . . 14
5652, 55sylibr 212 . . . . . . . . . . . . 13
57 ffn 5736 . . . . . . . . . . . . . 14
58 elpreima 6007 . . . . . . . . . . . . . 14
5931, 57, 583syl 20 . . . . . . . . . . . . 13
606, 56, 59mpbir2and 922 . . . . . . . . . . . 12
6143, 60ffvelrnd 6032 . . . . . . . . . . 11
62 elssuni 4279 . . . . . . . . . . 11
6361, 62syl 16 . . . . . . . . . 10
644oicl 7975 . . . . . . . . . . . 12
65 ordelon 4907 . . . . . . . . . . . 12
6664, 61, 65sylancr 663 . . . . . . . . . . 11
67 nnon 6706 . . . . . . . . . . . 12
6820, 67syl 16 . . . . . . . . . . 11
69 ontri1 4917 . . . . . . . . . . 11
7066, 68, 69syl2anc 661 . . . . . . . . . 10
7163, 70mpbid 210 . . . . . . . . 9
72 sucidg 4961 . . . . . . . . . . . . . 14
7320, 72syl 16 . . . . . . . . . . . . 13
7473, 14eleqtrrd 2548 . . . . . . . . . . . 12
75 isorel 6222 . . . . . . . . . . . 12
7638, 74, 61, 75syl12anc 1226 . . . . . . . . . . 11
77 fvex 5881 . . . . . . . . . . . 12
7877epelc 4798 . . . . . . . . . . 11
79 fvex 5881 . . . . . . . . . . . 12
8079epelc 4798 . . . . . . . . . . 11
8176, 78, 803bitr3g 287 . . . . . . . . . 10
82 f1ocnvfv2 6183 . . . . . . . . . . . 12
8340, 60, 82syl2anc 661 . . . . . . . . . . 11
8483eleq2d 2527 . . . . . . . . . 10
8581, 84bitrd 253 . . . . . . . . 9
8671, 85mtbid 300 . . . . . . . 8
878sseld 3502 . . . . . . . . . 10
88 onss 6626 . . . . . . . . . . . . . . . 16
893, 88syl 16 . . . . . . . . . . . . . . 15
9034, 89sstrd 3513 . . . . . . . . . . . . . 14
914oif 7976 . . . . . . . . . . . . . . . 16
9291ffvelrni 6030 . . . . . . . . . . . . . . 15
9374, 92syl 16 . . . . . . . . . . . . . 14
9490, 93sseldd 3504 . . . . . . . . . . . . 13
95 eloni 4893 . . . . . . . . . . . . 13
9694, 95syl 16 . . . . . . . . . . . 12
97 ordn2lp 4903 . . . . . . . . . . . 12
9896, 97syl 16 . . . . . . . . . . 11
99 imnan 422 . . . . . . . . . . 11
10098, 99sylibr 212 . . . . . . . . . 10
10187, 100syld 44 . . . . . . . . 9
102 onelon 4908 . . . . . . . . . . . . 13
1033, 6, 102syl2anc 661 . . . . . . . . . . . 12
104 eloni 4893 . . . . . . . . . . . 12
105103, 104syl 16 . . . . . . . . . . 11
106 ordirr 4901 . . . . . . . . . . 11
107105, 106syl 16 . . . . . . . . . 10
108 elsni 4054 . . . . . . . . . . . 12
109108eleq2d 2527 . . . . . . . . . . 11
110109notbid 294 . . . . . . . . . 10
111107, 110syl5ibrcom 222 . . . . . . . . 9
112 df1o2 7161 . . . . . . . . . . . . . 14
113112difeq2i 3618 . . . . . . . . . . . . 13
114113imaeq2i 5340 . . . . . . . . . . . 12
115 eldifi 3625 . . . . . . . . . . . . . . . 16
116115adantl 466 . . . . . . . . . . . . . . 15
1177adantr 465 . . . . . . . . . . . . . . . 16
118 fvex 5881 . . . . . . . . . . . . . . . 16
119 ifexg 4011 . . . . . . . . . . . . . . . 16
120117, 118, 119sylancl 662 . . . . . . . . . . . . . . 15
121 eqeq1 2461 . . . . . . . . . . . . . . . . 17
122 fveq2 5871 . . . . . . . . . . . . . . . . 17
123121, 122ifbieq2d 3966 . . . . . . . . . . . . . . . 16
124123, 9fvmptg 5954 . . . . . . . . . . . . . . 15
125116, 120, 124syl2anc 661 . . . . . . . . . . . . . 14
126 eldifn 3626 . . . . . . . . . . . . . . . . 17
127126adantl 466 . . . . . . . . . . . . . . . 16
128 elsn 4043 . . . . . . . . . . . . . . . . 17
129 elun2 3671 . . . . . . . . . . . . . . . . 17
130128, 129sylbir 213 . . . . . . . . . . . . . . . 16
131127, 130nsyl 121 . . . . . . . . . . . . . . 15
132 iffalse 3950 . . . . . . . . . . . . . . 15
133131, 132syl 16 . . . . . . . . . . . . . 14
134 ssun1 3666 . . . . . . . . . . . . . . . . 17
135 sscon 3637 . . . . . . . . . . . . . . . . 17
136134, 135ax-mp 5 . . . . . . . . . . . . . . . 16
137136sseli 3499 . . . . . . . . . . . . . . 15
138113imaeq2i 5340 . . . . . . . . . . . . . . . . 17
139 eqimss2 3556 . . . . . . . . . . . . . . . . 17
140138, 139mp1i 12 . . . . . . . . . . . . . . . 16
14127, 140suppssrOLD 6021 . . . . . . . . . . . . . . 15
142137, 141sylan2 474 . . . . . . . . . . . . . 14
143125, 133, 1423eqtrd 2502 . . . . . . . . . . . . 13
14431, 143suppssOLD 6020 . . . . . . . . . . . 12
145114, 144syl5eqss 3547 . . . . . . . . . . 11
146145, 93sseldd 3504 . . . . . . . . . 10
147 elun 3644 . . . . . . . . . 10
148146, 147sylib 196 . . . . . . . . 9
149101, 111, 148mpjaod 381 . . . . . . . 8
150 ioran 490 . . . . . . . 8
15186, 149, 150sylanbrc 664 . . . . . . 7
152 ordtri3 4919 . . . . . . . 8
15396, 105, 152syl2anc 661 . . . . . . 7
154151, 153mpbird 232 . . . . . 6
155154oveq2d 6312 . . . . 5
156154fveq2d 5875 . . . . . 6
157156, 46eqtrd 2498 . . . . 5
158155, 157oveq12d 6314 . . . 4
159 nnord 6708 . . . . . . . . 9
16020, 159syl 16 . . . . . . . 8
161 sssucid 4960 . . . . . . . . . 10
162161, 14syl5sseqr 3552 . . . . . . . . 9
163 f1ofo 5828 . . . . . . . . . . . . 13
16440, 163syl 16 . . . . . . . . . . . 12
165 foima 5805 . . . . . . . . . . . 12
166164, 165syl 16 . . . . . . . . . . 11
167 ffn 5736 . . . . . . . . . . . . . 14
16891, 167ax-mp 5 . . . . . . . . . . . . 13
169 fnsnfv 5933 . . . . . . . . . . . . 13
170168, 74, 169sylancr 663 . . . . . . . . . . . 12
171154sneqd 4041 . . . . . . . . . . . 12
172170, 171eqtr3d 2500 . . . . . . . . . . 11
173166, 172difeq12d 3622 . . . . . . . . . 10
174 ordirr 4901 . . . . . . . . . . . . . . . . 17
175160, 174syl 16 . . . . . . . . . . . . . . . 16
176 disjsn 4090 . . . . . . . . . . . . . . . 16
177175, 176sylibr 212 . . . . . . . . . . . . . . 15
178 disj3 3871 . . . . . . . . . . . . . . 15
179177, 178sylib 196 . . . . . . . . . . . . . 14
180 difun2 3907 . . . . . . . . . . . . . 14
181179, 180syl6eqr 2516 . . . . . . . . . . . . 13
182 df-suc 4889 . . . . . . . . . . . . . . 15
18314, 182syl6eq 2514 . . . . . . . . . . . . . 14
184183difeq1d 3620 . . . . . . . . . . . . 13
185181, 184eqtr4d 2501 . . . . . . . . . . . 12
186185imaeq2d 5342 . . . . . . . . . . 11
187 dff1o3 5827 . . . . . . . . . . . . 13
188187simprbi 464 . . . . . . . . . . . 12
189 imadif 5668 . . . . . . . . . . . 12
19040, 188, 1893syl 20 . . . . . . . . . . 11
191186, 190eqtrd 2498 . . . . . . . . . 10
1928, 107ssneldd 3506 . . . . . . . . . . . . 13
193 disjsn 4090 . . . . . . . . . . . . 13
194192, 193sylibr 212 . . . . . . . . . . . 12
195 fvex 5881 . . . . . . . . . . . . . . . . . . . . . 22
196 dif1o 7169 . . . . . . . . . . . . . . . . . . . . . 22
197195, 196mpbiran 918 . . . . . . . . . . . . . . . . . . . . 21
198 ffn 5736 . . . . . . . . . . . . . . . . . . . . . . . . 25
19927, 198syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
200 elpreima 6007 . . . . . . . . . . . . . . . . . . . . . . . 24
201199, 200syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
2028sseld 3502 . . . . . . . . . . . . . . . . . . . . . . 23
203201, 202sylbird 235 . . . . . . . . . . . . . . . . . . . . . 22
2046, 203mpand 675 . . . . . . . . . . . . . . . . . . . . 21
205197, 204syl5bir 218 . . . . . . . . . . . . . . . . . . . 20
206205necon1bd 2675 . . . . . . . . . . . . . . . . . . 19
207107, 206mpd 15 . . . . . . . . . . . . . . . . . 18
208207adantr 465 . . . . . . . . . . . . . . . . 17
209 fveq2 5871 . . . . . . . . . . . . . . . . . 18
210209eqeq1d 2459 . . . . . . . . . . . . . . . . 17
211208, 210syl5ibrcom 222 . . . . . . . . . . . . . . . 16
212 eldifi 3625 . . . . . . . . . . . . . . . . . . . 20
213212adantl 466 . . . . . . . . . . . . . . . . . . 19
2147adantr 465 . . . . . . . . . . . . . . . . . . . 20
215214, 118, 119sylancl 662 . . . . . . . . . . . . . . . . . . 19
216213, 215, 124syl2anc 661 . . . . . . . . . . . . . . . . . 18
217 ssid 3522 . . . . . . . . . . . . . . . . . . . 20
218217a1i 11 . . . . . . . . . . . . . . . . . . 19
21931, 218suppssrOLD 6021 . . . . . . . . . . . . . . . . . 18
220216, 219eqtr3d 2500 . . . . . . . . . . . . . . . . 17
221132eqeq1d 2459 . . . . . . . . . . . . . . . . 17
222220, 221syl5ibcom 220 . . . . . . . . . . . . . . . 16
223211, 222pm2.61d 158 . . . . . . . . . . . . . . 15
22427, 223suppssOLD 6020 . . . . . . . . . . . . . 14
225224, 138, 1143sstr4g 3544 . . . . . . . . . . . . 13
226 reldisj 3870 . . . . . . . . . . . . 13
227225, 226syl 16 . . . . . . . . . . . 12
228194, 227mpbid 210 . . . . . . . . . . 11
229 uncom 3647 . . . . . . . . . . . . 13
230145, 229syl6sseq 3549 . . . . . . . . . . . 12
231 ssundif 3911 . . . . . . . . . . . 12
232230, 231sylib 196 . . . . . . . . . . 11
233228, 232eqssd 3520 . . . . . . . . . 10
234173, 191, 2333eqtr4rd 2509 . . . . . . . . 9
235 isores3 6231 . . . . . . . . 9
23638, 162, 234, 235syl3anc 1228 . . . . . . . 8
237 cantnfp1OLD.k . . . . . . . . . . 11
2381, 2, 3, 237, 5cantnfclOLD 8137 . . . . . . . . . 10
239238simpld 459 . . . . . . . . 9
240 epse 4867 . . . . . . . . 9
241237oieu 7985 . . . . . . . . 9 <