Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
   |
2 | | poimir.i |
. . 3
   ![[,] [,]](_icc.gif)        |
3 | | poimir.r |
. . 3
                 |
4 | | poimir.1 |
. . 3
   ↾t     |
5 | | poimir.2 |
. . 3
 
    
                |
6 | | poimir.3 |
. . 3
 
    
                |
7 | 1, 2, 3, 4, 5, 6 | poimirlem32 31965 |
. 2
  
     
 ↾t   

               |
8 | | ovex 6316 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
9 | | retopon 21777 |
. . . . . . . . . . . . . . . . . . . . . 22
    TopOn   |
10 | 3 | pttoponconst 20605 |
. . . . . . . . . . . . . . . . . . . . . 22
          TopOn  
TopOn          |
11 | 8, 9, 10 | mp2an 677 |
. . . . . . . . . . . . . . . . . . . . 21
TopOn         |
12 | 11 | topontopi 19939 |
. . . . . . . . . . . . . . . . . . . 20
 |
13 | | reex 9627 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
14 | | unitssre 11776 |
. . . . . . . . . . . . . . . . . . . . . 22
  ![[,] [,]](_icc.gif)   |
15 | | mapss 7511 |
. . . . . . . . . . . . . . . . . . . . . 22
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)               |
16 | 13, 14, 15 | mp2an 677 |
. . . . . . . . . . . . . . . . . . . . 21
   ![[,] [,]](_icc.gif)       
      |
17 | 2, 16 | eqsstri 3461 |
. . . . . . . . . . . . . . . . . . . 20

      |
18 | 11 | toponunii 19940 |
. . . . . . . . . . . . . . . . . . . . 21
        |
19 | 18 | restuni 20171 |
. . . . . . . . . . . . . . . . . . . 20
        
  ↾t    |
20 | 12, 17, 19 | mp2an 677 |
. . . . . . . . . . . . . . . . . . 19
  ↾t   |
21 | 20, 18 | cnf 20255 |
. . . . . . . . . . . . . . . . . 18
   ↾t               |
22 | 4, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
             |
23 | 22 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . 16
 
             |
24 | | elmapi 7490 |
. . . . . . . . . . . . . . . 16
                         |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . 15
 
               |
26 | 25 | ffvelrnda 6020 |
. . . . . . . . . . . . . 14
                   |
27 | | recn 9626 |
. . . . . . . . . . . . . . . . 17
        
          |
28 | | absrpcl 13344 |
. . . . . . . . . . . . . . . . . 18
                                 |
29 | 28 | ex 436 |
. . . . . . . . . . . . . . . . 17
        
        
               |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
        
        
               |
31 | | ltsubrp 11332 |
. . . . . . . . . . . . . . . . . 18
                                                       |
32 | | ltaddrp 11333 |
. . . . . . . . . . . . . . . . . 18
                                                       |
33 | 31, 32 | jca 535 |
. . . . . . . . . . . . . . . . 17
                                                                                       |
34 | 33 | ex 436 |
. . . . . . . . . . . . . . . 16
        
                                                   
                          |
35 | 30, 34 | syld 45 |
. . . . . . . . . . . . . . 15
        
        
                              
                                  |
36 | 27 | abscld 13491 |
. . . . . . . . . . . . . . . . . 18
        
              |
37 | | resubcl 9935 |
. . . . . . . . . . . . . . . . . 18
                                               |
38 | 36, 37 | mpdan 673 |
. . . . . . . . . . . . . . . . 17
        
                        |
39 | 38 | rexrd 9687 |
. . . . . . . . . . . . . . . 16
        
                        |
40 | | readdcl 9619 |
. . . . . . . . . . . . . . . . . 18
                                               |
41 | 36, 40 | mpdan 673 |
. . . . . . . . . . . . . . . . 17
        
                        |
42 | 41 | rexrd 9687 |
. . . . . . . . . . . . . . . 16
        
                        |
43 | | rexr 9683 |
. . . . . . . . . . . . . . . 16
        
          |
44 | | elioo5 11689 |
. . . . . . . . . . . . . . . 16
                       
                     
                                                                 
                              
                                  |
45 | 39, 42, 43, 44 | syl3anc 1267 |
. . . . . . . . . . . . . . 15
        
                                                        
                              
                                  |
46 | 35, 45 | sylibrd 238 |
. . . . . . . . . . . . . 14
        
        
                                                           |
47 | 26, 46 | syl 17 |
. . . . . . . . . . . . 13
                                                                             |
48 | | fveq2 5863 |
. . . . . . . . . . . . . . . . 17
           |
49 | 48 | fveq1d 5865 |
. . . . . . . . . . . . . . . 16
                   |
50 | | eqid 2450 |
. . . . . . . . . . . . . . . 16
                     |
51 | | fvex 5873 |
. . . . . . . . . . . . . . . 16
         |
52 | 49, 50, 51 | fvmpt 5946 |
. . . . . . . . . . . . . . 15
                         |
53 | 52 | eleq1d 2512 |
. . . . . . . . . . . . . 14
                                                               
                                                           |
54 | 53 | ad2antlr 732 |
. . . . . . . . . . . . 13
                                                                       
                                                           |
55 | 47, 54 | sylibrd 238 |
. . . . . . . . . . . 12
                                                                                   |
56 | | iooretop 21779 |
. . . . . . . . . . . . 13
                                                     |
57 | | resttopon 20170 |
. . . . . . . . . . . . . . . . . . . 20
  TopOn 
      
     
 ↾t  TopOn    |
58 | 11, 17, 57 | mp2an 677 |
. . . . . . . . . . . . . . . . . . 19
 ↾t  TopOn   |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
      ↾t  TopOn    |
60 | 22 | feqmptd 5916 |
. . . . . . . . . . . . . . . . . . . 20
         |
61 | 60, 4 | eqeltrrd 2529 |
. . . . . . . . . . . . . . . . . . 19
        
↾t     |
62 | 61 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
             ↾t     |
63 | 11 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
     TopOn          |
64 | | retop 21775 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
65 | 64 | fconst6 5771 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
66 | 18, 3 | ptpjcn 20619 |
. . . . . . . . . . . . . . . . . . . . 21
                                                               |
67 | 8, 65, 66 | mp3an12 1353 |
. . . . . . . . . . . . . . . . . . . 20
                                     |
68 | | fvex 5873 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
69 | 68 | fvconst2 6118 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
70 | 69 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . 20
                               |
71 | 67, 70 | eleqtrd 2530 |
. . . . . . . . . . . . . . . . . . 19
                         |
72 | 71 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
                         |
73 | | fveq1 5862 |
. . . . . . . . . . . . . . . . . 18
                   |
74 | 59, 62, 63, 72, 73 | cnmpt11 20671 |
. . . . . . . . . . . . . . . . 17
 
                 ↾t    
    |
75 | 20 | cncnpi 20287 |
. . . . . . . . . . . . . . . . 17
             
↾t    
 
             
↾t    
       |
76 | 74, 75 | sylan 474 |
. . . . . . . . . . . . . . . 16
                     
↾t    
       |
77 | 76 | an32s 812 |
. . . . . . . . . . . . . . 15
                     
↾t    
       |
78 | | iscnp 20246 |
. . . . . . . . . . . . . . . . 17
  
↾t  TopOn    
 TopOn 

             
↾t    
                                        
 
↾t                 
      |
79 | 58, 9, 78 | mp3an12 1353 |
. . . . . . . . . . . . . . . 16
               ↾t                                              
 ↾t                 
      |
80 | 79 | ad2antlr 732 |
. . . . . . . . . . . . . . 15
                       ↾t                                              
 ↾t                 
      |
81 | 77, 80 | mpbid 214 |
. . . . . . . . . . . . . 14
                                            
 
↾t                 
     |
82 | 81 | simprd 465 |
. . . . . . . . . . . . 13
                             
 
↾t                 
    |
83 | | eleq2 2517 |
. . . . . . . . . . . . . . 15
                                                               
                                                                 |
84 | | sseq2 3453 |
. . . . . . . . . . . . . . . . 17
                                                               
                                                                 |
85 | 84 | anbi2d 709 |
. . . . . . . . . . . . . . . 16
                                                                
                                                                    |
86 | 85 | rexbidv 2900 |
. . . . . . . . . . . . . . 15
                                                   
↾t                 
   ↾t                                                                      |
87 | 83, 86 | imbi12d 322 |
. . . . . . . . . . . . . 14
                                                                 
 ↾t                 
                                                                 
 ↾t                 
                                                     |
88 | 87 | rspcv 3145 |
. . . . . . . . . . . . 13
                                                                          
 
↾t                 
 
                                                                
↾t                 
                                                     |
89 | 56, 82, 88 | mpsyl 65 |
. . . . . . . . . . . 12
                                                                        
 ↾t                 
                                                    |
90 | 55, 89 | syld 45 |
. . . . . . . . . . 11
                  
 ↾t                 
                                                    |
91 | | 0re 9640 |
. . . . . . . . . . . 12
 |
92 | | letric 9731 |
. . . . . . . . . . . 12
         
         
           |
93 | 26, 91, 92 | sylancl 667 |
. . . . . . . . . . 11
                 
           |
94 | 90, 93 | jctird 547 |
. . . . . . . . . 10
                    
↾t                 
                                                         
             |
95 | | r19.41v 2941 |
. . . . . . . . . . 11
   ↾t                  
                                                         
            
↾t                 
                                                         
            |
96 | | anass 654 |
. . . . . . . . . . . 12
                                                                                    

                                                                       
             |
97 | 96 | rexbii 2888 |
. . . . . . . . . . 11
   ↾t                  
                                                         
            ↾t                                                                           
             |
98 | 95, 97 | bitr3i 255 |
. . . . . . . . . 10
    ↾t                 
                                                         
            ↾t                                                                           
             |
99 | 94, 98 | syl6ib 230 |
. . . . . . . . 9
                  
 ↾t                                                                           
              |
100 | 58 | topontopi 19939 |
. . . . . . . . . . . . 13
 ↾t   |
101 | 20 | eltopss 19930 |
. . . . . . . . . . . . 13
  
↾t   ↾t     |
102 | 100, 101 | mpan 675 |
. . . . . . . . . . . 12
  ↾t    |
103 | | fvex 5873 |
. . . . . . . . . . . . . . . . . 18
         |
104 | 103, 50 | dmmpti 5705 |
. . . . . . . . . . . . . . . . 17
           |
105 | 104 | sseq2i 3456 |
. . . . . . . . . . . . . . . 16


        
  |
106 | | funmpt 5617 |
. . . . . . . . . . . . . . . . 17
           |
107 | | funimass4 5914 |
. . . . . . . . . . . . . . . . 17
                      
              
                                               

                                                                 |
108 | 106, 107 | mpan 675 |
. . . . . . . . . . . . . . . 16


                                                                        
                                                                 |
109 | 105, 108 | sylbir 217 |
. . . . . . . . . . . . . . 15
                                                               

                                                                 |
110 | | ssel2 3426 |
. . . . . . . . . . . . . . . . 17
 
   |
111 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . 21
           |
112 | 111 | fveq1d 5865 |
. . . . . . . . . . . . . . . . . . . 20
                   |
113 | | fvex 5873 |
. . . . . . . . . . . . . . . . . . . 20
         |
114 | 112, 50, 113 | fvmpt 5946 |
. . . . . . . . . . . . . . . . . . 19
                         |
115 | 114 | eleq1d 2512 |
. . . . . . . . . . . . . . . . . 18
                                                               
                                                           |
116 | | eliooord 11691 |
. . . . . . . . . . . . . . . . . 18
                                                                                               
                         |
117 | 115, 116 | syl6bi 232 |
. . . . . . . . . . . . . . . . 17
                                                                                                      
                          |
118 | 110, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
 
                                                                                                      
                          |
119 | 118 | ralimdva 2795 |
. . . . . . . . . . . . . . 15
  
                                                              
                                      
                          |
120 | 109, 119 | sylbid 219 |
. . . . . . . . . . . . . 14
                                                                
                                      
                          |
121 | 120 | adantl 468 |
. . . . . . . . . . . . 13
   

     
              
                                                
                              
                                  |
122 | | absnid 13354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 
                        |
123 | 122 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 
                                            |
124 | 27 | negidd 9973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        
                     |
125 | 124 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 
                      |
126 | 123, 125 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 
                         |
127 | 26, 126 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   

             
                        |
128 | 127 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                             |
129 | 128 | breq2d 4413 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             
                     
           |
130 | 22 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
             |
131 | | elmapi 7490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                         |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
               |
133 | 132 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   |
134 | 133 | an32s 812 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
135 | | 0red 9641 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
136 | 134, 135 | ltnled 9779 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 
           |
137 | 136 | adantllr 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

     
        
           |
138 | 137 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             
           |
139 | 129, 138 | bitrd 257 |
. . . . . . . . . . . . . . . . . . . . . 22
                             
                     
           |
140 | 139 | biimpd 211 |
. . . . . . . . . . . . . . . . . . . . 21
                             
                                 |
141 | 110, 140 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . 20
                    
 
                              
           |
142 | 141 | anassrs 653 |
. . . . . . . . . . . . . . . . . . 19
     
                         
                                 |
143 | 142 | adantld 469 |
. . . . . . . . . . . . . . . . . 18
     
                                                        
                      
           |
144 | 143 | ralimdva 2795 |
. . . . . . . . . . . . . . . . 17
                      
                                      
                       
           |
145 | 144 | an32s 812 |
. . . . . . . . . . . . . . . 16
                      
                                      
                       
           |
146 | 145 | impancom 442 |
. . . . . . . . . . . . . . 15
            
                                                                                    |
147 | | absid 13352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                         |
148 | 147 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                                             |
149 | 27 | subidd 9971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        
                    |
150 | 149 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                       |
151 | 148, 150 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                           |
152 | 26, 151 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   

             
                        |
153 | 152 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                             |
154 | 153 | breq1d 4411 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                   
           |
155 | 135, 134 | ltnled 9779 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
       
           |
156 | 155 | adantllr 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

     
        
           |
157 | 156 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     
       
           |
158 | 154, 157 | bitrd 257 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                   
           |
159 | 158 | biimpd 211 |
. . . . . . . . . . . . . . . . . . . . 21
                                                           
   |
160 | 110, 159 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . 20
                    
 
                              
           |
161 | 160 | anassrs 653 |
. . . . . . . . . . . . . . . . . . 19
     
                                                       
   |
162 | 161 | adantrd 470 |
. . . . . . . . . . . . . . . . . 18
     
                                                        
                              
   |
163 | 162 | ralimdva 2795 |
. . . . . . . . . . . . . . . . 17
                      
                                      
                       
       
   |
164 | 163 | an32s 812 |
. . . . . . . . . . . . . . . 16
                      
                                      
                       
       
   |
165 | 164 | impancom 442 |
. . . . . . . . . . . . . . 15
            
                                                                                    |
166 | 146, 165 | orim12d 848 |
. . . . . . . . . . . . . 14
            
                                                                                   
                     |
167 | 166 | expimpd 607 |
. . . . . . . . . . . . 13
   

     
  
                                      
                               
         
 
        
       
    |
168 | 121, 167 | syland 484 |
. . . . . . . . . . . 12
   

     
                                                                        
         
 
        
       
    |
169 | 102, 168 | sylan2 477 |
. . . . . . . . . . 11
   

      ↾t                                                                                                
            |
170 | 169 | anim2d 568 |
. . . . . . . . . 10
   

      ↾t                   
                                                        
          

 
                      |
171 | 170 | reximdva 2861 |
. . . . . . . . 9
          
 ↾t                                                                           
            
↾t     
                      |
172 | 99, 171 | syld 45 |
. . . . . . . 8
                  
 ↾t     
                      |
173 | | ralnex 2833 |
. . . . . . . . . . . . . 14
 
         

            |
174 | 173 | rexbii 2888 |
. . . . . . . . . . . . 13
   
         


            |
175 | | letsr 16466 |
. . . . . . . . . . . . . . 15
 |
176 | 175 | elexi 3054 |
. . . . . . . . . . . . . 14
 |
177 | 176 | cnvex 6737 |
. . . . . . . . . . . . . 14
 |
178 | | breq 4403 |
. . . . . . . . . . . . . . . 16

          
           |
179 | 178 | notbid 296 |
. . . . . . . . . . . . . . 15

          
           |
180 | 179 | ralbidv 2826 |
. . . . . . . . . . . . . 14

 
         

           |
181 | | breq 4403 |
. . . . . . . . . . . . . . . . 17
           
            |
182 | | c0ex 9634 |
. . . . . . . . . . . . . . . . . 18
 |
183 | 182, 113 | brcnv 5016 |
. . . . . . . . . . . . . . . . 17
         
          |
184 | 181, 183 | syl6bb 265 |
. . . . . . . . . . . . . . . 16
           
           |
185 | 184 | notbid 296 |
. . . . . . . . . . . . . . 15
                   
   |
186 | 185 | ralbidv 2826 |
. . . . . . . . . . . . . 14
                     
   |
187 | 176, 177,
180, 186 | rexpr 4025 |
. . . . . . . . . . . . 13
   
         
 
        
       
   |
188 | | rexnal 2835 |
. . . . . . . . . . . . 13
  
         

              |
189 | 174, 187,
188 | 3bitr3i 279 |
. . . . . . . . . . . 12
                    

              |
190 | 189 | anbi2i 699 |
. . . . . . . . . . 11
                      


 
             |
191 | | annim 427 |
. . . . . . . . . . 11
    
          
 
 
             |
192 | 190, 191 | bitri 253 |
. . . . . . . . . 10
                      
 
 
             |
193 | 192 | rexbii 2888 |
. . . . . . . . 9
   ↾t     
        
       
    ↾t   
 
             |
194 | | rexnal 2835 |
. . . . . . . . 9
   ↾t   
            
 
↾t    
               |
195 | 193, 194 | bitri 253 |
. . . . . . . 8
   ↾t     
        
       
 
 
↾t    
               |
196 | 172, 195 | syl6ib 230 |
. . . . . . 7
                    ↾t    
                |
197 | 196 | necon4ad 2642 |
. . . . . 6
          
 ↾t    
            
           |
198 | 197 | ralimdva 2795 |
. . . . 5
 
  
     
 ↾t   

            
                 |
199 | | ffn 5726 |
. . . . . 6
                       |
200 | 25, 199 | syl 17 |
. . . . 5
 
           |
201 | 198, 200 | jctild 546 |
. . . 4
 
  
     
 ↾t   

            
        
                  |
202 | | fconstfv 6124 |
. . . . 5
                       
                 |
203 | 182 | fconst2 6119 |
. . . . 5
                             |
204 | 202, 203 | bitr3i 255 |
. . . 4
                        
              |
205 | 201, 204 | syl6ib 230 |
. . 3
 
  
     
 ↾t   

            
               |
206 | 205 | reximdva 2861 |
. 2
          
↾t    
            

               |
207 | 7, 206 | mpd 15 |
1
                |