Step | Hyp | Ref
| Expression |
1 | | rge0ssre 11766 |
. . . . . . 7
    |
2 | | ax-resscn 9614 |
. . . . . . 7
 |
3 | 1, 2 | sstri 3427 |
. . . . . 6
    |
4 | 3 | sseli 3414 |
. . . . 5
   
  |
5 | | cxpcn3.d |
. . . . . . 7
      |
6 | | cnvimass 5194 |
. . . . . . . 8
      |
7 | | ref 13252 |
. . . . . . . . 9
     |
8 | 7 | fdmi 5746 |
. . . . . . . 8
 |
9 | 6, 8 | sseqtri 3450 |
. . . . . . 7
      |
10 | 5, 9 | eqsstri 3448 |
. . . . . 6
 |
11 | 10 | sseli 3414 |
. . . . 5
   |
12 | | cxpcl 23698 |
. . . . 5
 
      |
13 | 4, 11, 12 | syl2an 485 |
. . . 4
    
      |
14 | 13 | rgen2 2818 |
. . 3
      
   |
15 | | eqid 2471 |
. . . 4
             
     |
16 | 15 | fmpt2 6879 |
. . 3
 
    
  
    
               |
17 | 14, 16 | mpbi 213 |
. 2
                   |
18 | | cxpcn3.j |
. . . . . . . . . . . . 13
  ℂfld |
19 | 18 | cnfldtopon 21881 |
. . . . . . . . . . . 12
TopOn   |
20 | | rpre 11331 |
. . . . . . . . . . . . . . 15

  |
21 | | rpge0 11337 |
. . . . . . . . . . . . . . 15

  |
22 | | elrege0 11764 |
. . . . . . . . . . . . . . 15
   
    |
23 | 20, 21, 22 | sylanbrc 677 |
. . . . . . . . . . . . . 14

     |
24 | 23 | ssriv 3422 |
. . . . . . . . . . . . 13
 
  |
25 | 24, 3 | sstri 3427 |
. . . . . . . . . . . 12
 |
26 | | resttopon 20254 |
. . . . . . . . . . . 12
  TopOn 
  ↾t  TopOn    |
27 | 19, 25, 26 | mp2an 686 |
. . . . . . . . . . 11
 ↾t 
TopOn   |
28 | 27 | toponunii 20024 |
. . . . . . . . . . . 12
 
↾t   |
29 | 28 | restid 15410 |
. . . . . . . . . . 11
  ↾t  TopOn   
↾t 
↾t   ↾t    |
30 | 27, 29 | ax-mp 5 |
. . . . . . . . . 10
  ↾t 
↾t   ↾t   |
31 | 30 | eqcomi 2480 |
. . . . . . . . 9
 ↾t 
  ↾t  ↾t   |
32 | 27 | a1i 11 |
. . . . . . . . 9
     


 ↾t  TopOn    |
33 | | ssid 3437 |
. . . . . . . . . 10
 |
34 | 33 | a1i 11 |
. . . . . . . . 9
     


  |
35 | | cxpcn3.l |
. . . . . . . . 9

↾t   |
36 | 19 | a1i 11 |
. . . . . . . . 9
     


TopOn    |
37 | 10 | a1i 11 |
. . . . . . . . 9
     


  |
38 | | eqid 2471 |
. . . . . . . . . . 11
 ↾t 
 ↾t   |
39 | 18, 38 | cxpcn2 23765 |
. . . . . . . . . 10
         ↾t     |
40 | 39 | a1i 11 |
. . . . . . . . 9
     


         ↾t      |
41 | 31, 32, 34, 35, 36, 37, 40 | cnmpt2res 20769 |
. . . . . . . 8
     


         ↾t      |
42 | | elrege0 11764 |
. . . . . . . . . . . . 13
   
    |
43 | 42 | simplbi 467 |
. . . . . . . . . . . 12
   
  |
44 | 43 | adantr 472 |
. . . . . . . . . . 11
    
   |
45 | 44 | adantr 472 |
. . . . . . . . . 10
     


  |
46 | | simpr 468 |
. . . . . . . . . 10
     


  |
47 | 45, 46 | elrpd 11361 |
. . . . . . . . 9
     


  |
48 | | simplr 770 |
. . . . . . . . 9
     


  |
49 | | opelxp 4869 |
. . . . . . . . 9
    
     |
50 | 47, 48, 49 | sylanbrc 677 |
. . . . . . . 8
     


  
    |
51 | | resttopon 20254 |
. . . . . . . . . . . . 13
  TopOn 

 ↾t  TopOn    |
52 | 19, 10, 51 | mp2an 686 |
. . . . . . . . . . . 12
 ↾t  TopOn   |
53 | 35, 52 | eqeltri 2545 |
. . . . . . . . . . 11
TopOn   |
54 | | txtopon 20683 |
. . . . . . . . . . 11
  
↾t  TopOn  TopOn  
  ↾t   TopOn      |
55 | 27, 53, 54 | mp2an 686 |
. . . . . . . . . 10
  ↾t   TopOn     |
56 | 55 | toponunii 20024 |
. . . . . . . . 9
     ↾t    |
57 | 56 | cncnpi 20371 |
. . . . . . . 8
           ↾t   
  
             ↾t  
         |
58 | 41, 50, 57 | syl2anc 673 |
. . . . . . 7
     


         
↾t  
         |
59 | | ssid 3437 |
. . . . . . . 8
 |
60 | | resmpt2 6413 |
. . . . . . . 8
    
      
               |
61 | 24, 59, 60 | mp2an 686 |
. . . . . . 7
                    |
62 | | cxpcn3.k |
. . . . . . . . . . . 12

↾t      |
63 | | resttopon 20254 |
. . . . . . . . . . . . 13
  TopOn 
 
   ↾t     TopOn       |
64 | 19, 3, 63 | mp2an 686 |
. . . . . . . . . . . 12
 ↾t     TopOn      |
65 | 62, 64 | eqeltri 2545 |
. . . . . . . . . . 11
TopOn      |
66 | | ioorp 11737 |
. . . . . . . . . . . . . 14
    |
67 | | iooretop 21864 |
. . . . . . . . . . . . . 14
        |
68 | 66, 67 | eqeltrri 2546 |
. . . . . . . . . . . . 13
     |
69 | | retop 21860 |
. . . . . . . . . . . . . . 15
     |
70 | | ovex 6336 |
. . . . . . . . . . . . . . 15
    |
71 | | restopnb 20268 |
. . . . . . . . . . . . . . 15
         
 
  

     
  
     
↾t        |
72 | 69, 70, 71 | mpanl12 696 |
. . . . . . . . . . . . . 14
 
     

 
  
     
↾t        |
73 | 68, 24, 33, 72 | mp3an 1390 |
. . . . . . . . . . . . 13
         
↾t       |
74 | 68, 73 | mpbi 213 |
. . . . . . . . . . . 12
     ↾t      |
75 | | eqid 2471 |
. . . . . . . . . . . . . . 15
         |
76 | 18, 75 | rerest 21900 |
. . . . . . . . . . . . . 14
   
 ↾t  
       ↾t  
    |
77 | 1, 76 | ax-mp 5 |
. . . . . . . . . . . . 13
 ↾t          ↾t  
   |
78 | 62, 77 | eqtri 2493 |
. . . . . . . . . . . 12
     ↾t      |
79 | 74, 78 | eleqtrri 2548 |
. . . . . . . . . . 11
 |
80 | | toponmax 20020 |
. . . . . . . . . . . 12
 TopOn 
  |
81 | 53, 80 | ax-mp 5 |
. . . . . . . . . . 11
 |
82 | | txrest 20723 |
. . . . . . . . . . 11
   TopOn     TopOn  

    
↾t     
↾t   ↾t     |
83 | 65, 53, 79, 81, 82 | mp4an 687 |
. . . . . . . . . 10
   ↾t 
    ↾t   ↾t    |
84 | 62 | oveq1i 6318 |
. . . . . . . . . . . 12
 ↾t 
  ↾t    
↾t   |
85 | | restabs 20258 |
. . . . . . . . . . . . 13
  TopOn 
 
   
   ↾t     ↾t 
 ↾t    |
86 | 19, 24, 70, 85 | mp3an 1390 |
. . . . . . . . . . . 12
  ↾t    
↾t   ↾t   |
87 | 84, 86 | eqtri 2493 |
. . . . . . . . . . 11
 ↾t 
 ↾t   |
88 | 53 | toponunii 20024 |
. . . . . . . . . . . . 13
  |
89 | 88 | restid 15410 |
. . . . . . . . . . . 12
 TopOn 
 ↾t    |
90 | 53, 89 | ax-mp 5 |
. . . . . . . . . . 11
 ↾t   |
91 | 87, 90 | oveq12i 6320 |
. . . . . . . . . 10
  ↾t   ↾t     ↾t    |
92 | 83, 91 | eqtri 2493 |
. . . . . . . . 9
   ↾t 
    ↾t    |
93 | 92 | oveq1i 6318 |
. . . . . . . 8
    ↾t 
     
↾t  
  |
94 | 93 | fveq1i 5880 |
. . . . . . 7
    
↾t               ↾t           |
95 | 58, 61, 94 | 3eltr4g 2566 |
. . . . . 6
     


                  ↾t 
           |
96 | | txtopon 20683 |
. . . . . . . . . 10
  TopOn     TopOn  
  TopOn    
    |
97 | 65, 53, 96 | mp2an 686 |
. . . . . . . . 9
  TopOn   
    |
98 | 97 | topontopi 20023 |
. . . . . . . 8
   |
99 | 98 | a1i 11 |
. . . . . . 7
     


    |
100 | | xpss1 4948 |
. . . . . . . 8
     
  
    |
101 | 24, 100 | mp1i 13 |
. . . . . . 7
     


         |
102 | | txopn 20694 |
. . . . . . . . . 10
   TopOn     TopOn  

  
     |
103 | 65, 53, 79, 81, 102 | mp4an 687 |
. . . . . . . . 9
     |
104 | | isopn3i 20175 |
. . . . . . . . 9
                     
   |
105 | 98, 103, 104 | mp2an 686 |
. . . . . . . 8
            
  |
106 | 50, 105 | syl6eleqr 2560 |
. . . . . . 7
     


  
              |
107 | 17 | a1i 11 |
. . . . . . 7
     


    
               |
108 | 65 | topontopi 20023 |
. . . . . . . . 9
 |
109 | 53 | topontopi 20023 |
. . . . . . . . 9
 |
110 | 65 | toponunii 20024 |
. . . . . . . . 9
     |
111 | 108, 109,
110, 88 | txunii 20685 |
. . . . . . . 8
      
  |
112 | 19 | toponunii 20024 |
. . . . . . . 8
  |
113 | 111, 112 | cnprest 20382 |
. . . . . . 7
     

  
                       
              
                    
                  ↾t 
            |
114 | 99, 101, 106, 107, 113 | syl22anc 1293 |
. . . . . 6
     


                    
                  ↾t 
            |
115 | 95, 114 | mpbird 240 |
. . . . 5
     


    
                 |
116 | 17 | a1i 11 |
. . . . . . . 8
                     |
117 | | eqid 2471 |
. . . . . . . . . . 11
                     
         |
118 | | eqid 2471 |
. . . . . . . . . . 11
                                                               
                   
                                                      
            |
119 | 5, 18, 62, 35, 117, 118 | cxpcn3lem 23766 |
. . . . . . . . . 10
 
 
                             |
120 | 119 | ralrimiva 2809 |
. . . . . . . . 9
        
                       |
121 | | 0e0icopnf 11768 |
. . . . . . . . . . . . . . . . . 18
    |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . 17
     
       |
123 | | simprl 772 |
. . . . . . . . . . . . . . . . 17
     
       |
124 | 122, 123 | ovresd 6456 |
. . . . . . . . . . . . . . . 16
     
     
                  |
125 | | 0cn 9653 |
. . . . . . . . . . . . . . . . 17
 |
126 | 3, 123 | sseldi 3416 |
. . . . . . . . . . . . . . . . 17
     
    |
127 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18

  |
128 | 127 | cnmetdval 21869 |
. . . . . . . . . . . . . . . . 17
 
   
          |
129 | 125, 126,
128 | sylancr 676 |
. . . . . . . . . . . . . . . 16
     
               |
130 | | df-neg 9883 |
. . . . . . . . . . . . . . . . . 18
    |
131 | 130 | fveq2i 5882 |
. . . . . . . . . . . . . . . . 17
            |
132 | 126 | absnegd 13588 |
. . . . . . . . . . . . . . . . 17
     
             |
133 | 131, 132 | syl5eqr 2519 |
. . . . . . . . . . . . . . . 16
     
              |
134 | 124, 129,
133 | 3eqtrd 2509 |
. . . . . . . . . . . . . . 15
     
     
                 |
135 | 134 | breq1d 4405 |
. . . . . . . . . . . . . 14
     
          
 
    
       |
136 | | simpl 464 |
. . . . . . . . . . . . . . . . 17
     
    |
137 | | simprr 774 |
. . . . . . . . . . . . . . . . 17
     
    |
138 | 136, 137 | ovresd 6456 |
. . . . . . . . . . . . . . . 16
     
     
            |
139 | 10, 136 | sseldi 3416 |
. . . . . . . . . . . . . . . . 17
     
    |
140 | 10, 137 | sseldi 3416 |
. . . . . . . . . . . . . . . . 17
     
    |
141 | 127 | cnmetdval 21869 |
. . . . . . . . . . . . . . . . 17
 
   
          |
142 | 139, 140,
141 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
     
               |
143 | 138, 142 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
     
     
             |
144 | 143 | breq1d 4405 |
. . . . . . . . . . . . . 14
     
           
         |
145 | 135, 144 | anbi12d 725 |
. . . . . . . . . . . . 13
     
                            
    
          |
146 | | oveq12 6317 |
. . . . . . . . . . . . . . . . . . 19
           |
147 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . 19
    |
148 | 146, 15, 147 | ovmpt2a 6446 |
. . . . . . . . . . . . . . . . . 18
    
                   |
149 | 121, 136,
148 | sylancr 676 |
. . . . . . . . . . . . . . . . 17
     
        
           |
150 | 5 | eleq2i 2541 |
. . . . . . . . . . . . . . . . . . . . 21

       |
151 | | ffn 5739 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
152 | | elpreima 6017 |
. . . . . . . . . . . . . . . . . . . . . 22
                |
153 | 7, 151, 152 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . 21
     
        |
154 | 150, 153 | bitri 257 |
. . . . . . . . . . . . . . . . . . . 20

        |
155 | 154 | simplbi 467 |
. . . . . . . . . . . . . . . . . . 19
   |
156 | 154 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . 21
       |
157 | 156 | rpne0d 11369 |
. . . . . . . . . . . . . . . . . . . 20
       |
158 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
159 | | re0 13292 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
160 | 158, 159 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . 21
       |
161 | 160 | necon3i 2675 |
. . . . . . . . . . . . . . . . . . . 20
       |
162 | 157, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
   |
163 | 155, 162 | 0cxpd 23734 |
. . . . . . . . . . . . . . . . . 18
      |
164 | 163 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
       |
165 | 149, 164 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
     
        
        |
166 | | oveq12 6317 |
. . . . . . . . . . . . . . . . . 18
 
         |
167 | | ovex 6336 |
. . . . . . . . . . . . . . . . . 18
    |
168 | 166, 15, 167 | ovmpt2a 6446 |
. . . . . . . . . . . . . . . . 17
    
                   |
169 | 168 | adantl 473 |
. . . . . . . . . . . . . . . 16
     
        
           |
170 | 165, 169 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
     
                 
       
         
       |
171 | 126, 140 | cxpcld 23732 |
. . . . . . . . . . . . . . . 16
     
       |
172 | 127 | cnmetdval 21869 |
. . . . . . . . . . . . . . . 16
                         |
173 | 125, 171,
172 | sylancr 676 |
. . . . . . . . . . . . . . 15
     
                     |
174 | | df-neg 9883 |
. . . . . . . . . . . . . . . . 17
          |
175 | 174 | fveq2i 5882 |
. . . . . . . . . . . . . . . 16
                  |
176 | 171 | absnegd 13588 |
. . . . . . . . . . . . . . . 16
     
                   |
177 | 175, 176 | syl5eqr 2519 |
. . . . . . . . . . . . . . 15
     
                    |
178 | 170, 173,
177 | 3eqtrd 2509 |
. . . . . . . . . . . . . 14
     
                 
       
                |
179 | 178 | breq1d 4405 |
. . . . . . . . . . . . 13
     
                                 
          |
180 | 145, 179 | imbi12d 327 |
. . . . . . . . . . . 12
     
        
                                                                             |
181 | 180 | 2ralbidva 2831 |
. . . . . . . . . . 11
  
 
  
     
                                                     
 
  
                        |
182 | 181 | rexbidv 2892 |
. . . . . . . . . 10
  
           
                                                     
                              |
183 | 182 | ralbidv 2829 |
. . . . . . . . 9
  
            
                                                     
                               |
184 | 120, 183 | mpbird 240 |
. . . . . . . 8
        
     
                                                       |
185 | | cnxmet 21871 |
. . . . . . . . . . 11

      |
186 | 185 | a1i 11 |
. . . . . . . . . 10
         |
187 | | xmetres2 21454 |
. . . . . . . . . 10
  
          
                   |
188 | 186, 3, 187 | sylancl 675 |
. . . . . . . . 9
  
   
 
        
    |
189 | | xmetres2 21454 |
. . . . . . . . . 10
  
       
          |
190 | 186, 10, 189 | sylancl 675 |
. . . . . . . . 9
  
          |
191 | 121 | a1i 11 |
. . . . . . . . 9
      |
192 | | id 22 |
. . . . . . . . 9
   |
193 | | eqid 2471 |
. . . . . . . . . . . . 13
     
 
               |
194 | 18 | cnfldtopn 21880 |
. . . . . . . . . . . . 13
      |
195 | | eqid 2471 |
. . . . . . . . . . . . 13
    
              
   
 
     |
196 | 193, 194,
195 | metrest 21617 |
. . . . . . . . . . . 12
  
         
↾t         
            |
197 | 185, 3, 196 | mp2an 686 |
. . . . . . . . . . 11
 ↾t         
           |
198 | 62, 197 | eqtri 2493 |
. . . . . . . . . 10
        
 
     |
199 | | eqid 2471 |
. . . . . . . . . . . . 13
           |
200 | | eqid 2471 |
. . . . . . . . . . . . 13
    
        
     |
201 | 199, 194,
200 | metrest 21617 |
. . . . . . . . . . . 12
  
      
↾t      
      |
202 | 185, 10, 201 | mp2an 686 |
. . . . . . . . . . 11
 ↾t      
     |
203 | 35, 202 | eqtri 2493 |
. . . . . . . . . 10
     
    |
204 | 198, 203,
194 | txmetcnp 21640 |
. . . . . . . . 9
    
                  
       
          
 
                    
                                
                                                         |
205 | 188, 190,
186, 191, 192, 204 | syl32anc 1300 |
. . . . . . . 8
      
            
       
                          
                                                         |
206 | 116, 184,
205 | mpbir2and 936 |
. . . . . . 7
                       |
207 | 206 | ad2antlr 741 |
. . . . . 6
     

                       |
208 | | simpr 468 |
. . . . . . . 8
     

   |
209 | 208 | opeq1d 4164 |
. . . . . . 7
     

         |
210 | 209 | fveq2d 5883 |
. . . . . 6
     

                         |
211 | 207, 210 | eleqtrd 2551 |
. . . . 5
     

                       |
212 | 42 | simprbi 471 |
. . . . . . 7
   
  |
213 | 212 | adantr 472 |
. . . . . 6
    

  |
214 | | 0re 9661 |
. . . . . . 7
 |
215 | | leloe 9738 |
. . . . . . 7
 
       |
216 | 214, 44, 215 | sylancr 676 |
. . . . . 6
    
       |
217 | 213, 216 | mpbid 215 |
. . . . 5
    
 
   |
218 | 115, 211,
217 | mpjaodan 803 |
. . . 4
    
     
                 |
219 | 218 | rgen2 2818 |
. . 3
      
 
 
                |
220 | | fveq2 5879 |
. . . . 5
                         |
221 | 220 | eleq2d 2534 |
. . . 4
                     
    
                  |
222 | 221 | ralxp 4981 |
. . 3
 
  
                   
      
 
 
                 |
223 | 219, 222 | mpbir 214 |
. 2
    
      
             |
224 | | cncnp 20373 |
. . 3
    TopOn    
  TopOn  
                   
                                         |
225 | 97, 19, 224 | mp2an 686 |
. 2
                   
                                        |
226 | 17, 223, 225 | mpbir2an 934 |
1
              |