Step | Hyp | Ref
| Expression |
1 | | rge0ssre 12280 |
. . . . . . 7
|
2 | | ax-resscn 9993 |
. . . . . . 7
|
3 | 1, 2 | sstri 3612 |
. . . . . 6
|
4 | 3 | sseli 3599 |
. . . . 5
|
5 | | cxpcn3.d |
. . . . . . 7
|
6 | | cnvimass 5485 |
. . . . . . . 8
|
7 | | ref 13852 |
. . . . . . . . 9
|
8 | 7 | fdmi 6052 |
. . . . . . . 8
|
9 | 6, 8 | sseqtri 3637 |
. . . . . . 7
|
10 | 5, 9 | eqsstri 3635 |
. . . . . 6
|
11 | 10 | sseli 3599 |
. . . . 5
|
12 | | cxpcl 24420 |
. . . . 5
|
13 | 4, 11, 12 | syl2an 494 |
. . . 4
|
14 | 13 | rgen2 2975 |
. . 3
|
15 | | eqid 2622 |
. . . 4
|
16 | 15 | fmpt2 7237 |
. . 3
|
17 | 14, 16 | mpbi 220 |
. 2
|
18 | | cxpcn3.j |
. . . . . . . . . . . . 13
ℂfld |
19 | 18 | cnfldtopon 22586 |
. . . . . . . . . . . 12
TopOn |
20 | | rpre 11839 |
. . . . . . . . . . . . . . 15
|
21 | | rpge0 11845 |
. . . . . . . . . . . . . . 15
|
22 | | elrege0 12278 |
. . . . . . . . . . . . . . 15
|
23 | 20, 21, 22 | sylanbrc 698 |
. . . . . . . . . . . . . 14
|
24 | 23 | ssriv 3607 |
. . . . . . . . . . . . 13
|
25 | 24, 3 | sstri 3612 |
. . . . . . . . . . . 12
|
26 | | resttopon 20965 |
. . . . . . . . . . . 12
TopOn
↾t TopOn |
27 | 19, 25, 26 | mp2an 708 |
. . . . . . . . . . 11
↾t
TopOn |
28 | 27 | toponunii 20721 |
. . . . . . . . . . . 12
↾t |
29 | 28 | restid 16094 |
. . . . . . . . . . 11
↾t TopOn
↾t
↾t ↾t |
30 | 27, 29 | ax-mp 5 |
. . . . . . . . . 10
↾t
↾t ↾t |
31 | 30 | eqcomi 2631 |
. . . . . . . . 9
↾t
↾t ↾t |
32 | 27 | a1i 11 |
. . . . . . . . 9
↾t TopOn |
33 | | ssid 3624 |
. . . . . . . . . 10
|
34 | 33 | a1i 11 |
. . . . . . . . 9
|
35 | | cxpcn3.l |
. . . . . . . . 9
↾t |
36 | 19 | a1i 11 |
. . . . . . . . 9
TopOn |
37 | 10 | a1i 11 |
. . . . . . . . 9
|
38 | | eqid 2622 |
. . . . . . . . . . 11
↾t
↾t |
39 | 18, 38 | cxpcn2 24487 |
. . . . . . . . . 10
↾t |
40 | 39 | a1i 11 |
. . . . . . . . 9
↾t |
41 | 31, 32, 34, 35, 36, 37, 40 | cnmpt2res 21480 |
. . . . . . . 8
↾t |
42 | | elrege0 12278 |
. . . . . . . . . . . . 13
|
43 | 42 | simplbi 476 |
. . . . . . . . . . . 12
|
44 | 43 | adantr 481 |
. . . . . . . . . . 11
|
45 | 44 | adantr 481 |
. . . . . . . . . 10
|
46 | | simpr 477 |
. . . . . . . . . 10
|
47 | 45, 46 | elrpd 11869 |
. . . . . . . . 9
|
48 | | simplr 792 |
. . . . . . . . 9
|
49 | | opelxp 5146 |
. . . . . . . . 9
|
50 | 47, 48, 49 | sylanbrc 698 |
. . . . . . . 8
|
51 | | resttopon 20965 |
. . . . . . . . . . . . 13
TopOn
↾t TopOn |
52 | 19, 10, 51 | mp2an 708 |
. . . . . . . . . . . 12
↾t TopOn |
53 | 35, 52 | eqeltri 2697 |
. . . . . . . . . . 11
TopOn |
54 | | txtopon 21394 |
. . . . . . . . . . 11
↾t TopOn TopOn
↾t TopOn |
55 | 27, 53, 54 | mp2an 708 |
. . . . . . . . . 10
↾t TopOn |
56 | 55 | toponunii 20721 |
. . . . . . . . 9
↾t |
57 | 56 | cncnpi 21082 |
. . . . . . . 8
↾t
↾t
|
58 | 41, 50, 57 | syl2anc 693 |
. . . . . . 7
↾t
|
59 | | ssid 3624 |
. . . . . . . 8
|
60 | | resmpt2 6758 |
. . . . . . . 8
|
61 | 24, 59, 60 | mp2an 708 |
. . . . . . 7
|
62 | | cxpcn3.k |
. . . . . . . . . . . 12
↾t |
63 | | resttopon 20965 |
. . . . . . . . . . . . 13
TopOn
↾t TopOn |
64 | 19, 3, 63 | mp2an 708 |
. . . . . . . . . . . 12
↾t TopOn |
65 | 62, 64 | eqeltri 2697 |
. . . . . . . . . . 11
TopOn |
66 | | ioorp 12251 |
. . . . . . . . . . . . . 14
|
67 | | iooretop 22569 |
. . . . . . . . . . . . . 14
|
68 | 66, 67 | eqeltrri 2698 |
. . . . . . . . . . . . 13
|
69 | | retop 22565 |
. . . . . . . . . . . . . . 15
|
70 | | ovex 6678 |
. . . . . . . . . . . . . . 15
|
71 | | restopnb 20979 |
. . . . . . . . . . . . . . 15
↾t |
72 | 69, 70, 71 | mpanl12 718 |
. . . . . . . . . . . . . 14
↾t |
73 | 68, 24, 33, 72 | mp3an 1424 |
. . . . . . . . . . . . 13
↾t |
74 | 68, 73 | mpbi 220 |
. . . . . . . . . . . 12
↾t |
75 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
76 | 18, 75 | rerest 22607 |
. . . . . . . . . . . . . 14
↾t
↾t
|
77 | 1, 76 | ax-mp 5 |
. . . . . . . . . . . . 13
↾t ↾t
|
78 | 62, 77 | eqtri 2644 |
. . . . . . . . . . . 12
↾t |
79 | 74, 78 | eleqtrri 2700 |
. . . . . . . . . . 11
|
80 | | toponmax 20730 |
. . . . . . . . . . . 12
TopOn
|
81 | 53, 80 | ax-mp 5 |
. . . . . . . . . . 11
|
82 | | txrest 21434 |
. . . . . . . . . . 11
TopOn TopOn
↾t
↾t ↾t |
83 | 65, 53, 79, 81, 82 | mp4an 709 |
. . . . . . . . . 10
↾t
↾t ↾t |
84 | 62 | oveq1i 6660 |
. . . . . . . . . . . 12
↾t
↾t
↾t |
85 | | restabs 20969 |
. . . . . . . . . . . . 13
TopOn
↾t ↾t
↾t |
86 | 19, 24, 70, 85 | mp3an 1424 |
. . . . . . . . . . . 12
↾t
↾t ↾t |
87 | 84, 86 | eqtri 2644 |
. . . . . . . . . . 11
↾t
↾t |
88 | 53 | toponunii 20721 |
. . . . . . . . . . . . 13
|
89 | 88 | restid 16094 |
. . . . . . . . . . . 12
TopOn
↾t |
90 | 53, 89 | ax-mp 5 |
. . . . . . . . . . 11
↾t |
91 | 87, 90 | oveq12i 6662 |
. . . . . . . . . 10
↾t ↾t ↾t |
92 | 83, 91 | eqtri 2644 |
. . . . . . . . 9
↾t
↾t |
93 | 92 | oveq1i 6660 |
. . . . . . . 8
↾t
↾t
|
94 | 93 | fveq1i 6192 |
. . . . . . 7
↾t ↾t |
95 | 58, 61, 94 | 3eltr4g 2718 |
. . . . . 6
↾t
|
96 | | txtopon 21394 |
. . . . . . . . . 10
TopOn TopOn
TopOn
|
97 | 65, 53, 96 | mp2an 708 |
. . . . . . . . 9
TopOn
|
98 | 97 | topontopi 20720 |
. . . . . . . 8
|
99 | 98 | a1i 11 |
. . . . . . 7
|
100 | | xpss1 5228 |
. . . . . . . 8
|
101 | 24, 100 | mp1i 13 |
. . . . . . 7
|
102 | | txopn 21405 |
. . . . . . . . . 10
TopOn TopOn
|
103 | 65, 53, 79, 81, 102 | mp4an 709 |
. . . . . . . . 9
|
104 | | isopn3i 20886 |
. . . . . . . . 9
|
105 | 98, 103, 104 | mp2an 708 |
. . . . . . . 8
|
106 | 50, 105 | syl6eleqr 2712 |
. . . . . . 7
|
107 | 17 | a1i 11 |
. . . . . . 7
|
108 | 65 | topontopi 20720 |
. . . . . . . . 9
|
109 | 53 | topontopi 20720 |
. . . . . . . . 9
|
110 | 65 | toponunii 20721 |
. . . . . . . . 9
|
111 | 108, 109,
110, 88 | txunii 21396 |
. . . . . . . 8
|
112 | 19 | toponunii 20721 |
. . . . . . . 8
|
113 | 111, 112 | cnprest 21093 |
. . . . . . 7
↾t
|
114 | 99, 101, 106, 107, 113 | syl22anc 1327 |
. . . . . 6
↾t
|
115 | 95, 114 | mpbird 247 |
. . . . 5
|
116 | 17 | a1i 11 |
. . . . . . . 8
|
117 | | eqid 2622 |
. . . . . . . . . . 11
|
118 | | eqid 2622 |
. . . . . . . . . . 11
|
119 | 5, 18, 62, 35, 117, 118 | cxpcn3lem 24488 |
. . . . . . . . . 10
|
120 | 119 | ralrimiva 2966 |
. . . . . . . . 9
|
121 | | 0e0icopnf 12282 |
. . . . . . . . . . . . . . . . . 18
|
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
123 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
|
124 | 122, 123 | ovresd 6801 |
. . . . . . . . . . . . . . . 16
|
125 | | 0cn 10032 |
. . . . . . . . . . . . . . . . 17
|
126 | 3, 123 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
127 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
128 | 127 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . 17
|
129 | 125, 126,
128 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
130 | | df-neg 10269 |
. . . . . . . . . . . . . . . . . 18
|
131 | 130 | fveq2i 6194 |
. . . . . . . . . . . . . . . . 17
|
132 | 126 | absnegd 14188 |
. . . . . . . . . . . . . . . . 17
|
133 | 131, 132 | syl5eqr 2670 |
. . . . . . . . . . . . . . . 16
|
134 | 124, 129,
133 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
|
135 | 134 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
136 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
|
137 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
|
138 | 136, 137 | ovresd 6801 |
. . . . . . . . . . . . . . . 16
|
139 | 10, 136 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
140 | 10, 137 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
141 | 127 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . 17
|
142 | 139, 140,
141 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
143 | 138, 142 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
144 | 143 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
145 | 135, 144 | anbi12d 747 |
. . . . . . . . . . . . 13
|
146 | | oveq12 6659 |
. . . . . . . . . . . . . . . . . . 19
|
147 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . 19
|
148 | 146, 15, 147 | ovmpt2a 6791 |
. . . . . . . . . . . . . . . . . 18
|
149 | 121, 136,
148 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
150 | 5 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . 21
|
151 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . 22
|
152 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . . . . . 22
|
153 | 7, 151, 152 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . 21
|
154 | 150, 153 | bitri 264 |
. . . . . . . . . . . . . . . . . . . 20
|
155 | 154 | simplbi 476 |
. . . . . . . . . . . . . . . . . . 19
|
156 | 154 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . 21
|
157 | 156 | rpne0d 11877 |
. . . . . . . . . . . . . . . . . . . 20
|
158 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
|
159 | | re0 13892 |
. . . . . . . . . . . . . . . . . . . . . 22
|
160 | 158, 159 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . 21
|
161 | 160 | necon3i 2826 |
. . . . . . . . . . . . . . . . . . . 20
|
162 | 157, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
163 | 155, 162 | 0cxpd 24456 |
. . . . . . . . . . . . . . . . . 18
|
164 | 163 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
165 | 149, 164 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
166 | | oveq12 6659 |
. . . . . . . . . . . . . . . . . 18
|
167 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
|
168 | 166, 15, 167 | ovmpt2a 6791 |
. . . . . . . . . . . . . . . . 17
|
169 | 168 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
170 | 165, 169 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
171 | 126, 140 | cxpcld 24454 |
. . . . . . . . . . . . . . . 16
|
172 | 127 | cnmetdval 22574 |
. . . . . . . . . . . . . . . 16
|
173 | 125, 171,
172 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
174 | | df-neg 10269 |
. . . . . . . . . . . . . . . . 17
|
175 | 174 | fveq2i 6194 |
. . . . . . . . . . . . . . . 16
|
176 | 171 | absnegd 14188 |
. . . . . . . . . . . . . . . 16
|
177 | 175, 176 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
|
178 | 170, 173,
177 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
179 | 178 | breq1d 4663 |
. . . . . . . . . . . . 13
|
180 | 145, 179 | imbi12d 334 |
. . . . . . . . . . . 12
|
181 | 180 | 2ralbidva 2988 |
. . . . . . . . . . 11
|
182 | 181 | rexbidv 3052 |
. . . . . . . . . 10
|
183 | 182 | ralbidv 2986 |
. . . . . . . . 9
|
184 | 120, 183 | mpbird 247 |
. . . . . . . 8
|
185 | | cnxmet 22576 |
. . . . . . . . . . 11
|
186 | 185 | a1i 11 |
. . . . . . . . . 10
|
187 | | xmetres2 22166 |
. . . . . . . . . 10
|
188 | 186, 3, 187 | sylancl 694 |
. . . . . . . . 9
|
189 | | xmetres2 22166 |
. . . . . . . . . 10
|
190 | 186, 10, 189 | sylancl 694 |
. . . . . . . . 9
|
191 | 121 | a1i 11 |
. . . . . . . . 9
|
192 | | id 22 |
. . . . . . . . 9
|
193 | | eqid 2622 |
. . . . . . . . . . . . 13
|
194 | 18 | cnfldtopn 22585 |
. . . . . . . . . . . . 13
|
195 | | eqid 2622 |
. . . . . . . . . . . . 13
|
196 | 193, 194,
195 | metrest 22329 |
. . . . . . . . . . . 12
↾t
|
197 | 185, 3, 196 | mp2an 708 |
. . . . . . . . . . 11
↾t
|
198 | 62, 197 | eqtri 2644 |
. . . . . . . . . 10
|
199 | | eqid 2622 |
. . . . . . . . . . . . 13
|
200 | | eqid 2622 |
. . . . . . . . . . . . 13
|
201 | 199, 194,
200 | metrest 22329 |
. . . . . . . . . . . 12
↾t
|
202 | 185, 10, 201 | mp2an 708 |
. . . . . . . . . . 11
↾t
|
203 | 35, 202 | eqtri 2644 |
. . . . . . . . . 10
|
204 | 198, 203,
194 | txmetcnp 22352 |
. . . . . . . . 9
|
205 | 188, 190,
186, 191, 192, 204 | syl32anc 1334 |
. . . . . . . 8
|
206 | 116, 184,
205 | mpbir2and 957 |
. . . . . . 7
|
207 | 206 | ad2antlr 763 |
. . . . . 6
|
208 | | simpr 477 |
. . . . . . . 8
|
209 | 208 | opeq1d 4408 |
. . . . . . 7
|
210 | 209 | fveq2d 6195 |
. . . . . 6
|
211 | 207, 210 | eleqtrd 2703 |
. . . . 5
|
212 | 42 | simprbi 480 |
. . . . . . 7
|
213 | 212 | adantr 481 |
. . . . . 6
|
214 | | 0re 10040 |
. . . . . . 7
|
215 | | leloe 10124 |
. . . . . . 7
|
216 | 214, 44, 215 | sylancr 695 |
. . . . . 6
|
217 | 213, 216 | mpbid 222 |
. . . . 5
|
218 | 115, 211,
217 | mpjaodan 827 |
. . . 4
|
219 | 218 | rgen2 2975 |
. . 3
|
220 | | fveq2 6191 |
. . . . 5
|
221 | 220 | eleq2d 2687 |
. . . 4
|
222 | 221 | ralxp 5263 |
. . 3
|
223 | 219, 222 | mpbir 221 |
. 2
|
224 | | cncnp 21084 |
. . 3
TopOn
TopOn
|
225 | 97, 19, 224 | mp2an 708 |
. 2
|
226 | 17, 223, 225 | mpbir2an 955 |
1
|