Step | Hyp | Ref
| Expression |
1 | | xrlimcnp.r |
. . . . 5
|
2 | | eqid 2622 |
. . . . 5
|
3 | 1, 2 | fmptd 6385 |
. . . 4
|
4 | 3 | adantr 481 |
. . 3
|
5 | | ssun2 3777 |
. . . . . . . . . 10
|
6 | | pnfex 10093 |
. . . . . . . . . . 11
|
7 | 6 | snid 4208 |
. . . . . . . . . 10
|
8 | 5, 7 | sselii 3600 |
. . . . . . . . 9
|
9 | | xrlimcnp.a |
. . . . . . . . 9
|
10 | 8, 9 | syl5eleqr 2708 |
. . . . . . . 8
|
11 | 1 | ralrimiva 2966 |
. . . . . . . . 9
|
12 | | xrlimcnp.c |
. . . . . . . . . . 11
|
13 | 12 | eleq1d 2686 |
. . . . . . . . . 10
|
14 | 13 | rspcv 3305 |
. . . . . . . . 9
|
15 | 10, 11, 14 | sylc 65 |
. . . . . . . 8
|
16 | 12, 2 | fvmptg 6280 |
. . . . . . . 8
|
17 | 10, 15, 16 | syl2anc 693 |
. . . . . . 7
|
18 | 17 | ad2antrr 762 |
. . . . . 6
|
19 | 18 | eleq1d 2686 |
. . . . 5
|
20 | | cnxmet 22576 |
. . . . . . . 8
|
21 | | xrlimcnp.j |
. . . . . . . . . 10
ℂfld |
22 | 21 | cnfldtopn 22585 |
. . . . . . . . 9
|
23 | 22 | mopni2 22298 |
. . . . . . . 8
|
24 | 20, 23 | mp3an1 1411 |
. . . . . . 7
|
25 | | ssun1 3776 |
. . . . . . . . . . . . 13
|
26 | 25, 9 | syl5sseqr 3654 |
. . . . . . . . . . . 12
|
27 | | ssralv 3666 |
. . . . . . . . . . . 12
|
28 | 26, 11, 27 | sylc 65 |
. . . . . . . . . . 11
|
29 | 28 | ad2antrr 762 |
. . . . . . . . . 10
|
30 | | simprl 794 |
. . . . . . . . . 10
|
31 | | simplr 792 |
. . . . . . . . . 10
|
32 | 29, 30, 31 | rlimi 14244 |
. . . . . . . . 9
|
33 | | letop 21010 |
. . . . . . . . . . . . . . 15
ordTop |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
ordTop |
35 | | xrlimcnp.b |
. . . . . . . . . . . . . . . . . . 19
|
36 | | ressxr 10083 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 35, 36 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . 18
|
38 | | pnfxr 10092 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 39 | snssd 4340 |
. . . . . . . . . . . . . . . . . 18
|
41 | 37, 40 | unssd 3789 |
. . . . . . . . . . . . . . . . 17
|
42 | 9, 41 | eqsstrd 3639 |
. . . . . . . . . . . . . . . 16
|
43 | | xrex 11829 |
. . . . . . . . . . . . . . . . 17
|
44 | 43 | ssex 4802 |
. . . . . . . . . . . . . . . 16
|
45 | 42, 44 | syl 17 |
. . . . . . . . . . . . . . 15
|
46 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
47 | | iocpnfordt 21019 |
. . . . . . . . . . . . . . 15
ordTop
|
48 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
ordTop |
49 | | elrestr 16089 |
. . . . . . . . . . . . . 14
ordTop
ordTop ordTop ↾t |
50 | 34, 46, 48, 49 | syl3anc 1326 |
. . . . . . . . . . . . 13
ordTop
↾t |
51 | | xrlimcnp.k |
. . . . . . . . . . . . 13
ordTop ↾t |
52 | 50, 51 | syl6eleqr 2712 |
. . . . . . . . . . . 12
|
53 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
54 | 53 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
55 | 38 | a1i 11 |
. . . . . . . . . . . . . 14
|
56 | | ltpnf 11954 |
. . . . . . . . . . . . . . 15
|
57 | 53, 56 | syl 17 |
. . . . . . . . . . . . . 14
|
58 | | ubioc1 12227 |
. . . . . . . . . . . . . 14
|
59 | 54, 55, 57, 58 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
60 | 10 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
61 | 59, 60 | elind 3798 |
. . . . . . . . . . . 12
|
62 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
63 | 62 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
64 | | elioc1 12217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
65 | 63, 38, 64 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
66 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
67 | 65, 66 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | 35 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
69 | 68 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
70 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
71 | 62, 69, 70 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
72 | 67, 71 | syld 47 |
. . . . . . . . . . . . . . . . . . . . 21
|
73 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
74 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
75 | 74 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
76 | | rpxr 11840 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
78 | 15 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
79 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
80 | 79 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
81 | | elbl3 22197 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
82 | 73, 77, 78, 80, 81 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
83 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
84 | 83 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
85 | 80, 78, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
86 | 85 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
87 | 82, 86 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . 22
|
88 | 87 | biimprd 238 |
. . . . . . . . . . . . . . . . . . . . 21
|
89 | 72, 88 | imim12d 81 |
. . . . . . . . . . . . . . . . . . . 20
|
90 | 89 | ralimdva 2962 |
. . . . . . . . . . . . . . . . . . 19
|
91 | 90 | impr 649 |
. . . . . . . . . . . . . . . . . 18
|
92 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
93 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
|
94 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . 21
|
95 | | blcntr 22218 |
. . . . . . . . . . . . . . . . . . . . 21
|
96 | 92, 93, 94, 95 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | 96 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
|
98 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . 21
|
99 | 12 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . 21
|
100 | 98, 99 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
|
101 | 6, 100 | ralsn 4222 |
. . . . . . . . . . . . . . . . . . 19
|
102 | 97, 101 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
|
103 | | ralunb 3794 |
. . . . . . . . . . . . . . . . . 18
|
104 | 91, 102, 103 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
|
105 | 9 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
106 | 105 | raleqdv 3144 |
. . . . . . . . . . . . . . . . 17
|
107 | 104, 106 | mpbird 247 |
. . . . . . . . . . . . . . . 16
|
108 | | ss2rab 3678 |
. . . . . . . . . . . . . . . 16
|
109 | 107, 108 | sylibr 224 |
. . . . . . . . . . . . . . 15
|
110 | | incom 3805 |
. . . . . . . . . . . . . . . 16
|
111 | | dfin5 3582 |
. . . . . . . . . . . . . . . 16
|
112 | 110, 111 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
113 | 2 | mptpreima 5628 |
. . . . . . . . . . . . . . 15
|
114 | 109, 112,
113 | 3sstr4g 3646 |
. . . . . . . . . . . . . 14
|
115 | | funmpt 5926 |
. . . . . . . . . . . . . . 15
|
116 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
|
117 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
118 | | fdm 6051 |
. . . . . . . . . . . . . . . . 17
|
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
|
120 | 116, 119 | syl5sseqr 3654 |
. . . . . . . . . . . . . . 15
|
121 | | funimass3 6333 |
. . . . . . . . . . . . . . 15
|
122 | 115, 120,
121 | sylancr 695 |
. . . . . . . . . . . . . 14
|
123 | 114, 122 | mpbird 247 |
. . . . . . . . . . . . 13
|
124 | | simplrr 801 |
. . . . . . . . . . . . 13
|
125 | 123, 124 | sstrd 3613 |
. . . . . . . . . . . 12
|
126 | | eleq2 2690 |
. . . . . . . . . . . . . 14
|
127 | | imaeq2 5462 |
. . . . . . . . . . . . . . 15
|
128 | 127 | sseq1d 3632 |
. . . . . . . . . . . . . 14
|
129 | 126, 128 | anbi12d 747 |
. . . . . . . . . . . . 13
|
130 | 129 | rspcev 3309 |
. . . . . . . . . . . 12
|
131 | 52, 61, 125, 130 | syl12anc 1324 |
. . . . . . . . . . 11
|
132 | 131 | rexlimdvaa 3032 |
. . . . . . . . . 10
|
133 | 132 | adantlr 751 |
. . . . . . . . 9
|
134 | 32, 133 | mpd 15 |
. . . . . . . 8
|
135 | 134 | rexlimdvaa 3032 |
. . . . . . 7
|
136 | 24, 135 | syl5 34 |
. . . . . 6
|
137 | 136 | expdimp 453 |
. . . . 5
|
138 | 19, 137 | sylbid 230 |
. . . 4
|
139 | 138 | ralrimiva 2966 |
. . 3
|
140 | | letopon 21009 |
. . . . . . 7
ordTop TopOn |
141 | | resttopon 20965 |
. . . . . . 7
ordTop
TopOn ordTop ↾t TopOn |
142 | 140, 42, 141 | sylancr 695 |
. . . . . 6
ordTop ↾t TopOn |
143 | 51, 142 | syl5eqel 2705 |
. . . . 5
TopOn |
144 | 21 | cnfldtopon 22586 |
. . . . . 6
TopOn |
145 | 144 | a1i 11 |
. . . . 5
TopOn |
146 | | iscnp 21041 |
. . . . 5
TopOn TopOn
|
147 | 143, 145,
10, 146 | syl3anc 1326 |
. . . 4
|
148 | 147 | adantr 481 |
. . 3
|
149 | 4, 139, 148 | mpbir2and 957 |
. 2
|
150 | | simplr 792 |
. . . . . . 7
|
151 | 20 | a1i 11 |
. . . . . . . 8
|
152 | 15 | ad2antrr 762 |
. . . . . . . 8
|
153 | 76 | adantl 482 |
. . . . . . . 8
|
154 | 22 | blopn 22305 |
. . . . . . . 8
|
155 | 151, 152,
153, 154 | syl3anc 1326 |
. . . . . . 7
|
156 | 17 | ad2antrr 762 |
. . . . . . . 8
|
157 | | simpr 477 |
. . . . . . . . 9
|
158 | 151, 152,
157, 95 | syl3anc 1326 |
. . . . . . . 8
|
159 | 156, 158 | eqeltrd 2701 |
. . . . . . 7
|
160 | | cnpimaex 21060 |
. . . . . . 7
|
161 | 150, 155,
159, 160 | syl3anc 1326 |
. . . . . 6
|
162 | | vex 3203 |
. . . . . . . . 9
|
163 | 162 | inex1 4799 |
. . . . . . . 8
|
164 | 163 | a1i 11 |
. . . . . . 7
ordTop
|
165 | 51 | eleq2i 2693 |
. . . . . . . 8
ordTop
↾t |
166 | 45 | ad2antrr 762 |
. . . . . . . . 9
|
167 | | elrest 16088 |
. . . . . . . . 9
ordTop
ordTop ↾t
ordTop
|
168 | 33, 166, 167 | sylancr 695 |
. . . . . . . 8
ordTop
↾t
ordTop |
169 | 165, 168 | syl5bb 272 |
. . . . . . 7
ordTop |
170 | | eleq2 2690 |
. . . . . . . . 9
|
171 | | imaeq2 5462 |
. . . . . . . . . 10
|
172 | 171 | sseq1d 3632 |
. . . . . . . . 9
|
173 | 170, 172 | anbi12d 747 |
. . . . . . . 8
|
174 | 173 | adantl 482 |
. . . . . . 7
|
175 | 164, 169,
174 | rexxfr2d 4883 |
. . . . . 6
ordTop
|
176 | 161, 175 | mpbid 222 |
. . . . 5
ordTop
|
177 | | inss1 3833 |
. . . . . . . . . . . 12
|
178 | 177 | sseli 3599 |
. . . . . . . . . . 11
|
179 | | pnfnei 21024 |
. . . . . . . . . . 11
ordTop
|
180 | 178, 179 | sylan2 491 |
. . . . . . . . . 10
ordTop
|
181 | | df-ima 5127 |
. . . . . . . . . . . . . . . 16
|
182 | | inss2 3834 |
. . . . . . . . . . . . . . . . . 18
|
183 | | resmpt 5449 |
. . . . . . . . . . . . . . . . . 18
|
184 | 182, 183 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
185 | 184 | rneqi 5352 |
. . . . . . . . . . . . . . . 16
|
186 | 181, 185 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
187 | 186 | sseq1i 3629 |
. . . . . . . . . . . . . 14
|
188 | | dfss3 3592 |
. . . . . . . . . . . . . 14
|
189 | 187, 188 | bitri 264 |
. . . . . . . . . . . . 13
|
190 | 11 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
191 | | ssralv 3666 |
. . . . . . . . . . . . . . . 16
|
192 | 182, 190,
191 | mpsyl 68 |
. . . . . . . . . . . . . . 15
|
193 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
194 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
|
195 | 193, 194 | ralrnmpt 6368 |
. . . . . . . . . . . . . . 15
|
196 | 192, 195 | syl 17 |
. . . . . . . . . . . . . 14
|
197 | 196 | biimpd 219 |
. . . . . . . . . . . . 13
|
198 | 189, 197 | syl5bi 232 |
. . . . . . . . . . . 12
|
199 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
200 | 37 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
201 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
202 | 200, 201 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
203 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
204 | | pnfge 11964 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
205 | 202, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
206 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
207 | 206 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
208 | 207, 38, 64 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
209 | 202, 203,
205, 208 | mpbir3and 1245 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
210 | 199, 209 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
211 | 26 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
212 | 211 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
213 | 212 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
214 | 210, 213 | elind 3798 |
. . . . . . . . . . . . . . . . . . . . . 22
|
215 | 214 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
|
216 | 215 | imim1d 82 |
. . . . . . . . . . . . . . . . . . . 20
|
217 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
218 | 76 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
219 | 218 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
220 | 15 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
221 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
222 | 221 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
223 | 222 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
224 | 217, 219,
220, 223, 81 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . 22
|
225 | 223, 220,
84 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
226 | 225 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . 22
|
227 | 224, 226 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . 21
|
228 | 227 | pm5.74da 723 |
. . . . . . . . . . . . . . . . . . . 20
|
229 | 216, 228 | sylibd 229 |
. . . . . . . . . . . . . . . . . . 19
|
230 | 229 | exp4a 633 |
. . . . . . . . . . . . . . . . . 18
|
231 | 230 | ralimdv2 2961 |
. . . . . . . . . . . . . . . . 17
|
232 | 231 | imp 445 |
. . . . . . . . . . . . . . . 16
|
233 | 232 | an32s 846 |
. . . . . . . . . . . . . . 15
|
234 | 233 | expr 643 |
. . . . . . . . . . . . . 14
|
235 | 234 | reximdva 3017 |
. . . . . . . . . . . . 13
|
236 | 235 | ex 450 |
. . . . . . . . . . . 12
|
237 | 198, 236 | syld 47 |
. . . . . . . . . . 11
|
238 | 237 | com23 86 |
. . . . . . . . . 10
|
239 | 180, 238 | syl5 34 |
. . . . . . . . 9
ordTop
|
240 | 239 | impl 650 |
. . . . . . . 8
ordTop
|
241 | 240 | expimpd 629 |
. . . . . . 7
ordTop
|
242 | 241 | rexlimdva 3031 |
. . . . . 6
ordTop
|
243 | 242 | adantlr 751 |
. . . . 5
ordTop
|
244 | 176, 243 | mpd 15 |
. . . 4
|
245 | 244 | ralrimiva 2966 |
. . 3
|
246 | 28, 35, 15 | rlim2lt 14228 |
. . . 4
|
247 | 246 | adantr 481 |
. . 3
|
248 | 245, 247 | mpbird 247 |
. 2
|
249 | 149, 248 | impbida 877 |
1
|