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

Theorem infxpenlem 8412
Description: Lemma for infxpen 8413. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
leweon.1
r0weon.1
infxpen.1
infxpen.2
infxpen.3
infxpen.4
Assertion
Ref Expression
infxpenlem
Distinct variable groups:   ,   ,J   , ,   , ,M   , ,   ,Q   , , , , ,

Proof of Theorem infxpenlem
StepHypRef Expression
1 sseq2 3525 . . . 4
2 xpeq12 5023 . . . . . 6
32anidms 645 . . . . 5
4 id 22 . . . . 5
53, 4breq12d 4465 . . . 4
61, 5imbi12d 320 . . 3
7 sseq2 3525 . . . 4
8 xpeq12 5023 . . . . . 6
98anidms 645 . . . . 5
10 id 22 . . . . 5
119, 10breq12d 4465 . . . 4
127, 11imbi12d 320 . . 3
13 infxpen.2 . . . . . . . 8
14 vex 3112 . . . . . . . . . . . . 13
1514, 14xpex 6604 . . . . . . . . . . . 12
16 simpll 753 . . . . . . . . . . . . . . . . . 18
1713, 16sylbi 195 . . . . . . . . . . . . . . . . 17
18 onss 6626 . . . . . . . . . . . . . . . . 17
1917, 18syl 16 . . . . . . . . . . . . . . . 16
20 xpss12 5113 . . . . . . . . . . . . . . . 16
2119, 19, 20syl2anc 661 . . . . . . . . . . . . . . 15
22 leweon.1 . . . . . . . . . . . . . . . . 17
23 r0weon.1 . . . . . . . . . . . . . . . . 17
2422, 23r0weon 8411 . . . . . . . . . . . . . . . 16
2524simpli 458 . . . . . . . . . . . . . . 15
26 wess 4871 . . . . . . . . . . . . . . 15
2721, 25, 26mpisyl 18 . . . . . . . . . . . . . 14
28 weinxp 5072 . . . . . . . . . . . . . 14
2927, 28sylib 196 . . . . . . . . . . . . 13
30 infxpen.1 . . . . . . . . . . . . . 14
31 weeq1 4872 . . . . . . . . . . . . . 14
3230, 31ax-mp 5 . . . . . . . . . . . . 13
3329, 32sylibr 212 . . . . . . . . . . . 12
34 infxpen.4 . . . . . . . . . . . . 13
3534oiiso 7983 . . . . . . . . . . . 12
3615, 33, 35sylancr 663 . . . . . . . . . . 11
37 isof1o 6221 . . . . . . . . . . 11
38 f1ocnv 5833 . . . . . . . . . . 11
39 f1of1 5820 . . . . . . . . . . 11
4036, 37, 38, 394syl 21 . . . . . . . . . 10
41 f1f1orn 5832 . . . . . . . . . 10
4215f1oen 7556 . . . . . . . . . 10
4340, 41, 423syl 20 . . . . . . . . 9
44 f1ofn 5822 . . . . . . . . . . 11
4536, 37, 38, 444syl 21 . . . . . . . . . 10
4636adantr 465 . . . . . . . . . . . . . . . . 17
4737, 38, 393syl 20 . . . . . . . . . . . . . . . . . 18
48 cnvimass 5362 . . . . . . . . . . . . . . . . . . 19
49 inss2 3718 . . . . . . . . . . . . . . . . . . . . . 22
5030, 49eqsstri 3533 . . . . . . . . . . . . . . . . . . . . 21
51 dmss 5207 . . . . . . . . . . . . . . . . . . . . 21
5250, 51ax-mp 5 . . . . . . . . . . . . . . . . . . . 20
53 dmxpid 5227 . . . . . . . . . . . . . . . . . . . 20
5452, 53sseqtri 3535 . . . . . . . . . . . . . . . . . . 19
5548, 54sstri 3512 . . . . . . . . . . . . . . . . . 18
56 f1ores 5835 . . . . . . . . . . . . . . . . . 18
5747, 55, 56sylancl 662 . . . . . . . . . . . . . . . . 17
5815, 15xpex 6604 . . . . . . . . . . . . . . . . . . . . . 22
5958inex2 4594 . . . . . . . . . . . . . . . . . . . . 21
6030, 59eqeltri 2541 . . . . . . . . . . . . . . . . . . . 20
6160cnvex 6747 . . . . . . . . . . . . . . . . . . 19
62 imaexg 6737 . . . . . . . . . . . . . . . . . . 19
6361, 62ax-mp 5 . . . . . . . . . . . . . . . . . 18
6463f1oen 7556 . . . . . . . . . . . . . . . . 17
6546, 57, 643syl 20 . . . . . . . . . . . . . . . 16
66 sseqin2 3716 . . . . . . . . . . . . . . . . . . 19
6755, 66mpbi 208 . . . . . . . . . . . . . . . . . 18
6867imaeq2i 5340 . . . . . . . . . . . . . . . . 17
69 isocnv 6226 . . . . . . . . . . . . . . . . . . . 20
7046, 69syl 16 . . . . . . . . . . . . . . . . . . 19
71 simpr 461 . . . . . . . . . . . . . . . . . . 19
72 isoini 6234 . . . . . . . . . . . . . . . . . . 19
7370, 71, 72syl2anc 661 . . . . . . . . . . . . . . . . . 18
74 fvex 5881 . . . . . . . . . . . . . . . . . . . . 21
7574epini 5372 . . . . . . . . . . . . . . . . . . . 20
7675ineq2i 3696 . . . . . . . . . . . . . . . . . . 19
7734oicl 7975 . . . . . . . . . . . . . . . . . . . . 21
78 f1of 5821 . . . . . . . . . . . . . . . . . . . . . . 23
7936, 37, 38, 784syl 21 . . . . . . . . . . . . . . . . . . . . . 22
8079ffvelrnda 6031 . . . . . . . . . . . . . . . . . . . . 21
81 ordelss 4899 . . . . . . . . . . . . . . . . . . . . 21
8277, 80, 81sylancr 663 . . . . . . . . . . . . . . . . . . . 20
83 dfss1 3702 . . . . . . . . . . . . . . . . . . . 20
8482, 83sylib 196 . . . . . . . . . . . . . . . . . . 19
8576, 84syl5eq 2510 . . . . . . . . . . . . . . . . . 18
8673, 85eqtrd 2498 . . . . . . . . . . . . . . . . 17
8768, 86syl5eqr 2512 . . . . . . . . . . . . . . . 16
8865, 87breqtrd 4476 . . . . . . . . . . . . . . 15
8988ensymd 7586 . . . . . . . . . . . . . 14
90 infxpen.3 . . . . . . . . . . . . . . . . . . 19
91 fvex 5881 . . . . . . . . . . . . . . . . . . . 20
92 fvex 5881 . . . . . . . . . . . . . . . . . . . 20
9391, 92unex 6598 . . . . . . . . . . . . . . . . . . 19
9490, 93eqeltri 2541 . . . . . . . . . . . . . . . . . 18
9594sucex 6646 . . . . . . . . . . . . . . . . 17
9695, 95xpex 6604 . . . . . . . . . . . . . . . 16
97 xpss 5114 . . . . . . . . . . . . . . . . . . . 20
98 simp3 998 . . . . . . . . . . . . . . . . . . . . . 22
99 vex 3112 . . . . . . . . . . . . . . . . . . . . . . 23
100 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . 24
101100eliniseg 5371 . . . . . . . . . . . . . . . . . . . . . . 23
10299, 101ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22
10398, 102sylib 196 . . . . . . . . . . . . . . . . . . . . 21
10430breqi 4458 . . . . . . . . . . . . . . . . . . . . . . 23
105 brin 4501 . . . . . . . . . . . . . . . . . . . . . . 23
106104, 105bitri 249 . . . . . . . . . . . . . . . . . . . . . 22
107106simprbi 464 . . . . . . . . . . . . . . . . . . . . 21
108 brxp 5035 . . . . . . . . . . . . . . . . . . . . . 22
109108simplbi 460 . . . . . . . . . . . . . . . . . . . . 21
110103, 107, 1093syl 20 . . . . . . . . . . . . . . . . . . . 20
11197, 110sseldi 3501 . . . . . . . . . . . . . . . . . . 19
11217adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
1131123adant3 1016 . . . . . . . . . . . . . . . . . . . . 21
114 xp1st 6830 . . . . . . . . . . . . . . . . . . . . . 22
115 onelon 4908 . . . . . . . . . . . . . . . . . . . . . 22
116114, 115sylan2 474 . . . . . . . . . . . . . . . . . . . . 21
117113, 110, 116syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
118 eloni 4893 . . . . . . . . . . . . . . . . . . . . . . . . . 26
119 elxp7 6833 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
120119simprbi 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26
121 ordunel 6662 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1221213expib 1199 . . . . . . . . . . . . . . . . . . . . . . . . . 26
123118, 120, 122syl2im 38 . . . . . . . . . . . . . . . . . . . . . . . . 25
124112, 71, 123sylc 60 . . . . . . . . . . . . . . . . . . . . . . . 24
12590, 124syl5eqel 2549 . . . . . . . . . . . . . . . . . . . . . . 23
126 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
12713, 126sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . 26
128 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
12913, 128sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . 26
130 iscard 8377 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
131 cardlim 8374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132 sseq2 3525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133 limeq 4895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134132, 133bibi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135131, 134mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136130, 135sylbir 213 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
137136biimpa 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26
13817, 127, 129, 137syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . 25
139138adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
140 limsuc 6684 . . . . . . . . . . . . . . . . . . . . . . . 24
141139, 140syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
142125, 141mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22
143 onelon 4908 . . . . . . . . . . . . . . . . . . . . . 22
144112, 142, 143syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
1451443adant3 1016 . . . . . . . . . . . . . . . . . . . 20
146 ssun1 3666 . . . . . . . . . . . . . . . . . . . . 21
147146a1i 11 . . . . . . . . . . . . . . . . . . . 20
148106simplbi 460 . . . . . . . . . . . . . . . . . . . . 21
149 df-br 4453 . . . . . . . . . . . . . . . . . . . . . . . . . 26
15023eleq2i 2535 . . . . . . . . . . . . . . . . . . . . . . . . . 26
151 opabid 4759 . . . . . . . . . . . . . . . . . . . . . . . . . 26
152149, 150, 1513bitri 271 . . . . . . . . . . . . . . . . . . . . . . . . 25
153152simprbi 464 . . . . . . . . . . . . . . . . . . . . . . . 24
154 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . 25
155154orim2i 518 . . . . . . . . . . . . . . . . . . . . . . . 24
156153, 155syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
157 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . . . 25
158 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . . . 25
159157, 158unex 6598 . . . . . . . . . . . . . . . . . . . . . . . 24
160159elsuc 4952 . . . . . . . . . . . . . . . . . . . . . . 23
161156, 160sylibr 212 . . . . . . . . . . . . . . . . . . . . . 22
162 suceq 4948 . . . . . . . . . . . . . . . . . . . . . . 23
16390, 162ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22
164161, 163syl6eleqr 2556 . . . . . . . . . . . . . . . . . . . . 21
165103, 148, 1643syl 20 . . . . . . . . . . . . . . . . . . . 20
166 ontr2 4930 . . . . . . . . . . . . . . . . . . . . 21
167166imp 429 . . . . . . . . . . . . . . . . . . . 20
168117, 145, 147, 165, 167syl22anc 1229 . . . . . . . . . . . . . . . . . . 19
169 xp2nd 6831 . . . . . . . . . . . . . . . . . . . . . 22
170 onelon 4908 . . . . . . . . . . . . . . . . . . . . . 22
171169, 170sylan2 474 . . . . . . . . . . . . . . . . . . . . 21
172113, 110, 171syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
173 ssun2 3667 . . . . . . . . . . . . . . . . . . . . 21
174173a1i 11 . . . . . . . . . . . . . . . . . . . 20
175 ontr2 4930 . . . . . . . . . . . . . . . . . . . . 21
176175imp 429 . . . . . . . . . . . . . . . . . . . 20
177172, 145, 174, 165, 176syl22anc 1229 . . . . . . . . . . . . . . . . . . 19
178 elxp7 6833 . . . . . . . . . . . . . . . . . . . 20
179178biimpri 206 . . . . . . . . . . . . . . . . . . 19
180111, 168, 177, 179syl12anc 1226 . . . . . . . . . . . . . . . . . 18
1811803expia 1198 . . . . . . . . . . . . . . . . 17
182181ssrdv 3509 . . . . . . . . . . . . . . . 16
183 ssdomg 7581 . . . . . . . . . . . . . . . 16
18496, 182, 183mpsyl 63 . . . . . . . . . . . . . . 15
185129adantr 465 . . . . . . . . . . . . . . . . 17
186 nnfi 7730 . . . . . . . . . . . . . . . . . . . 20
187 xpfi 7811 . . . . . . . . . . . . . . . . . . . . . 22
188187anidms 645 . . . . . . . . . . . . . . . . . . . . 21
189 isfinite 8090 . . . . . . . . . . . . . . . . . . . . 21
190188, 189sylib 196 . . . . . . . . . . . . . . . . . . . 20
191186, 190syl 16 . . . . . . . . . . . . . . . . . . 19
192 ssdomg 7581 . . . . . . . . . . . . . . . . . . . 20
19314, 192ax-mp 5 . . . . . . . . . . . . . . . . . . 19
194 sdomdomtr 7670 . . . . . . . . . . . . . . . . . . 19
195191, 193, 194syl2an 477 . . . . . . . . . . . . . . . . . 18
196195expcom 435 . . . . . . . . . . . . . . . . 17
197185, 196syl 16 . . . . . . . . . . . . . . . 16
198127adantr 465 . . . . . . . . . . . . . . . . . 18
199 breq1 4455 . . . . . . . . . . . . . . . . . . 19
200199rspccv 3207 . . . . . . . . . . . . . . . . . 18
201198, 142, 200sylc 60 . . . . . . . . . . . . . . . . 17
202 omelon 8084 . . . . . . . . . . . . . . . . . . 19
203 ontri1 4917 . . . . . . . . . . . . . . . . . . 19
204202, 144, 203sylancr 663 . . . . . . . . . . . . . . . . . 18
205 simplr 755 . . . . . . . . . . . . . . . . . . . . 21
20613, 205sylbi 195 . . . . . . . . . . . . . . . . . . . 20
207206adantr 465 . . . . . . . . . . . . . . . . . . 19
208 sseq2 3525 . . . . . . . . . . . . . . . . . . . . 21
209 xpeq12 5023 . . . . . . . . . . . . . . . . . . . . . . 23
210209anidms 645 . . . . . . . . . . . . . . . . . . . . . 22
211 id 22 . . . . . . . . . . . . . . . . . . . . . 22
212210, 211breq12d 4465 . . . . . . . . . . . . . . . . . . . . 21
213208, 212imbi12d 320 . . . . . . . . . . . . . . . . . . . 20
214213rspccv 3207 . . . . . . . . . . . . . . . . . . 19
215207, 142, 214sylc 60 . . . . . . . . . . . . . . . . . 18