Step | Hyp | Ref
| Expression |
1 | | xkoptsub.j |
. . . . 5
         |
2 | | xkoptsub.x |
. . . . . . . . 9
  |
3 | 2 | topopn 19984 |
. . . . . . . 8
   |
4 | 3 | adantr 471 |
. . . . . . 7
 
   |
5 | | fconstg 5792 |
. . . . . . . . 9
             |
6 | 5 | adantl 472 |
. . . . . . . 8
 
             |
7 | | ffn 5750 |
. . . . . . . 8
                 |
8 | 6, 7 | syl 17 |
. . . . . . 7
 
       |
9 | | eqid 2461 |
. . . . . . . 8
                                            
    
            
                 
        |
10 | 9 | ptval 20633 |
. . . . . . 7
  
   
                                                          |
11 | 4, 8, 10 | syl2anc 671 |
. . . . . 6
 
                                                           |
12 | | simpr 467 |
. . . . . . . . . . 11
 
   |
13 | 12 | snssd 4129 |
. . . . . . . . . 10
 
     |
14 | 6, 13 | fssd 5760 |
. . . . . . . . 9
 
           |
15 | | eqid 2461 |
. . . . . . . . . 10

         
          |
16 | 9, 15 | ptbasfi 20644 |
. . . . . . . . 9
  
       
                                                             
           
                      |
17 | 4, 14, 16 | syl2anc 671 |
. . . . . . . 8
 
      
            
                 
                        
           
                      |
18 | | fvconst2g 6141 |
. . . . . . . . . . . . . . 15
 
           |
19 | 18 | adantll 725 |
. . . . . . . . . . . . . 14
   

          |
20 | 19 | unieqd 4221 |
. . . . . . . . . . . . 13
   

            |
21 | 20 | ixpeq2dva 7562 |
. . . . . . . . . . . 12
 
           
   |
22 | | eqid 2461 |
. . . . . . . . . . . . . 14
   |
23 | 22 | topopn 19984 |
. . . . . . . . . . . . 13
    |
24 | | ixpconstg 7556 |
. . . . . . . . . . . . 13
     
 
   |
25 | 3, 23, 24 | syl2an 484 |
. . . . . . . . . . . 12
 
  
 
   |
26 | 21, 25 | eqtrd 2495 |
. . . . . . . . . . 11
 
                |
27 | 26 | sneqd 3991 |
. . . . . . . . . 10
 
                    |
28 | | eqid 2461 |
. . . . . . . . . . . 12
 |
29 | | fvconst2g 6141 |
. . . . . . . . . . . . . . 15
 
           |
30 | 29 | adantll 725 |
. . . . . . . . . . . . . 14
   

          |
31 | 26 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
   

               |
32 | 31 | mpteq1d 4497 |
. . . . . . . . . . . . . . . . 17
   

                           |
33 | 32 | cnveqd 5028 |
. . . . . . . . . . . . . . . 16
   

  
                          |
34 | 33 | imaeq1d 5185 |
. . . . . . . . . . . . . . 15
   

  

                                 |
35 | 34 | ralrimivw 2814 |
. . . . . . . . . . . . . 14
   

             
                                 |
36 | 30, 35 | jca 539 |
. . . . . . . . . . . . 13
   

                      
                                  |
37 | 36 | ralrimiva 2813 |
. . . . . . . . . . . 12
 
          
             
                                  |
38 | | mpt2eq123 6376 |
. . . . . . . . . . . 12
                         
                                
             
                                     |
39 | 28, 37, 38 | sylancr 674 |
. . . . . . . . . . 11
 
  
           
                   
                 |
40 | 39 | rneqd 5080 |
. . . . . . . . . 10
 
              
                   
                 |
41 | 27, 40 | uneq12d 3600 |
. . . . . . . . 9
 
   
           
           
                          
                  |
42 | 41 | fveq2d 5891 |
. . . . . . . 8
 
                  
           
                              
                   |
43 | 17, 42 | eqtrd 2495 |
. . . . . . 7
 
      
            
                 
                 
                   |
44 | 43 | fveq2d 5891 |
. . . . . 6
 
                                                              
                    |
45 | 11, 44 | eqtrd 2495 |
. . . . 5
 
                      
                    |
46 | 1, 45 | syl5eq 2507 |
. . . 4
 
              
                    |
47 | 46 | oveq1d 6329 |
. . 3
 
 
↾t                  
                  ↾t      |
48 | | firest 15379 |
. . . . 5
           
                ↾t                
                
↾t     |
49 | 48 | fveq2i 5890 |
. . . 4
              
                ↾t                    
                
↾t      |
50 | | fvex 5897 |
. . . . 5
          
                  |
51 | | ovex 6342 |
. . . . 5
   |
52 | | tgrest 20223 |
. . . . 5
            
                                  
                
↾t                   
                  ↾t      |
53 | 50, 51, 52 | mp2an 683 |
. . . 4
              
                
↾t                   
                  ↾t     |
54 | 49, 53 | eqtri 2483 |
. . 3
              
                ↾t                    
                  ↾t     |
55 | 47, 54 | syl6eqr 2513 |
. 2
 
 
↾t                  
                ↾t        |
56 | | xkotop 20651 |
. . 3
 
       |
57 | | snex 4654 |
. . . . . 6
      |
58 | | mpt2exga 6895 |
. . . . . . . 8
 
  
                 |
59 | 3, 58 | sylan 478 |
. . . . . . 7
 
  
                 |
60 | | rnexg 6751 |
. . . . . . 7
  
                
                 |
61 | 59, 60 | syl 17 |
. . . . . 6
 
                    |
62 | | unexg 6618 |
. . . . . 6
        
                       
                  |
63 | 57, 61, 62 | sylancr 674 |
. . . . 5
 
        
                  |
64 | | restval 15373 |
. . . . 5
         
                           
                ↾t            
                       |
65 | 63, 51, 64 | sylancl 673 |
. . . 4
 
         
                ↾t    
       
                       |
66 | | elun 3585 |
. . . . . . 7
        
                     
 
                  |
67 | 2, 22 | cnf 20310 |
. . . . . . . . . . . . . 14
          |
68 | | elmapg 7510 |
. . . . . . . . . . . . . . 15
  

   
        |
69 | 23, 3, 68 | syl2anr 485 |
. . . . . . . . . . . . . 14
 
             |
70 | 67, 69 | syl5ibr 229 |
. . . . . . . . . . . . 13
 
          |
71 | 70 | ssrdv 3449 |
. . . . . . . . . . . 12
 
  
     |
72 | 71 | adantr 471 |
. . . . . . . . . . 11
   
       
     |
73 | | elsni 4004 |
. . . . . . . . . . . 12
           |
74 | 73 | adantl 472 |
. . . . . . . . . . 11
   
     
     |
75 | 72, 74 | sseqtr4d 3480 |
. . . . . . . . . 10
   
       
  |
76 | | dfss1 3648 |
. . . . . . . . . 10
  
        |
77 | 75, 76 | sylib 201 |
. . . . . . . . 9
   
              |
78 | | eqid 2461 |
. . . . . . . . . . . 12
         |
79 | 78 | xkouni 20662 |
. . . . . . . . . . 11
 
          |
80 | | eqid 2461 |
. . . . . . . . . . . . 13
           |
81 | 80 | topopn 19984 |
. . . . . . . . . . . 12
                |
82 | 56, 81 | syl 17 |
. . . . . . . . . . 11
 
            |
83 | 79, 82 | eqeltrd 2539 |
. . . . . . . . . 10
 
         |
84 | 83 | adantr 471 |
. . . . . . . . 9
   
              |
85 | 77, 84 | eqeltrd 2539 |
. . . . . . . 8
   
                |
86 | | eqid 2461 |
. . . . . . . . . . 11
 
                
                |
87 | 86 | rnmpt2 6432 |
. . . . . . . . . 10
 
                 
  
 
           |
88 | 87 | abeq2i 2573 |
. . . . . . . . 9
  
              


                |
89 | | cnvresima 5342 |
. . . . . . . . . . . . . . 15
                                     |
90 | 71 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
    
         |
91 | 90 | resmptd 5174 |
. . . . . . . . . . . . . . . . 17
    
            
            |
92 | 91 | cnveqd 5028 |
. . . . . . . . . . . . . . . 16
    
                 
         |
93 | 92 | imaeq1d 5185 |
. . . . . . . . . . . . . . 15
    
                                   |
94 | 89, 93 | syl5eqr 2509 |
. . . . . . . . . . . . . 14
    
                                   |
95 | | fvex 5897 |
. . . . . . . . . . . . . . . . . . . 20
     |
96 | 95 | rgenw 2760 |
. . . . . . . . . . . . . . . . . . 19
         |
97 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . 20
                 |
98 | 97 | fnmpt 5725 |
. . . . . . . . . . . . . . . . . . 19
 
                   |
99 | 96, 98 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
    
              |
100 | | elpreima 6024 |
. . . . . . . . . . . . . . . . . 18
                        
  
                |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . . 17
    
                  
                |
102 | | fveq1 5886 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
103 | | fvex 5897 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
104 | 102, 97, 103 | fvmpt 5970 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
105 | 104 | adantl 472 |
. . . . . . . . . . . . . . . . . . . 20
   


 

                    |
106 | 105 | eleq1d 2523 |
. . . . . . . . . . . . . . . . . . 19
   


 

                      |
107 | 103 | snss 4108 |
. . . . . . . . . . . . . . . . . . . 20
    
        |
108 | 90 | sselda 3443 |
. . . . . . . . . . . . . . . . . . . . . . 23
   


 

       |
109 | | elmapi 7518 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
110 | | ffn 5750 |
. . . . . . . . . . . . . . . . . . . . . . 23
        |
111 | 108, 109,
110 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
   


 

    |
112 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . . . . 22
   


 

    |
113 | | fnsnfv 5947 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
114 | 111, 112,
113 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . 21
   


 

                |
115 | 114 | sseq1d 3470 |
. . . . . . . . . . . . . . . . . . . 20
   


 

                  |
116 | 107, 115 | syl5bb 265 |
. . . . . . . . . . . . . . . . . . 19
   


 

      
         |
117 | 106, 116 | bitrd 261 |
. . . . . . . . . . . . . . . . . 18
   


 

                        |
118 | 117 | pm5.32da 651 |
. . . . . . . . . . . . . . . . 17
    
                  
  
          |
119 | 101, 118 | bitrd 261 |
. . . . . . . . . . . . . . . 16
    
                  
          |
120 | 119 | abbi2dv 2580 |
. . . . . . . . . . . . . . 15
    
                             |
121 | | df-rab 2757 |
. . . . . . . . . . . . . . 15
         
   
         |
122 | 120, 121 | syl6eqr 2513 |
. . . . . . . . . . . . . 14
    
                           |
123 | 94, 122 | eqtrd 2495 |
. . . . . . . . . . . . 13
    
                                |
124 | | simpll 765 |
. . . . . . . . . . . . . 14
    
    |
125 | 12 | adantr 471 |
. . . . . . . . . . . . . 14
    
    |
126 | | simprl 769 |
. . . . . . . . . . . . . . 15
    
    |
127 | 126 | snssd 4129 |
. . . . . . . . . . . . . 14
    
   
  |
128 | 2 | toptopon 19996 |
. . . . . . . . . . . . . . . . 17

TopOn    |
129 | 124, 128 | sylib 201 |
. . . . . . . . . . . . . . . 16
    
  TopOn    |
130 | | restsn2 20235 |
. . . . . . . . . . . . . . . 16
  TopOn    ↾t         |
131 | 129, 126,
130 | syl2anc 671 |
. . . . . . . . . . . . . . 15
    
   ↾t         |
132 | | snfi 7675 |
. . . . . . . . . . . . . . . 16
   |
133 | | discmp 20461 |
. . . . . . . . . . . . . . . 16
        |
134 | 132, 133 | mpbi 213 |
. . . . . . . . . . . . . . 15
    |
135 | 131, 134 | syl6eqel 2547 |
. . . . . . . . . . . . . 14
    
   ↾t      |
136 | | simprr 771 |
. . . . . . . . . . . . . 14
    
    |
137 | 2, 124, 125, 127, 135, 136 | xkoopn 20652 |
. . . . . . . . . . . . 13
    
           
      |
138 | 123, 137 | eqeltrd 2539 |
. . . . . . . . . . . 12
    
                          |
139 | | ineq1 3638 |
. . . . . . . . . . . . 13
                                       |
140 | 139 | eleq1d 2523 |
. . . . . . . . . . . 12
                       
                         |
141 | 138, 140 | syl5ibrcom 230 |
. . . . . . . . . . 11
    
                 
          |
142 | 141 | rexlimdvva 2897 |
. . . . . . . . . 10
 
                             |
143 | 142 | imp 435 |
. . . . . . . . 9
     
  
 
          
         |
144 | 88, 143 | sylan2b 482 |
. . . . . . . 8
   
 
               
          |
145 | 85, 144 | jaodan 799 |
. . . . . . 7
         
 
                
          |
146 | 66, 145 | sylan2b 482 |
. . . . . 6
   
       
                 
         |
147 | | eqid 2461 |
. . . . . 6
        
                             
                      |
148 | 146, 147 | fmptd 6068 |
. . . . 5
 
         
                              
                        |
149 | | frn 5757 |
. . . . 5
         
                              
                      
       
                     
     |
150 | 148, 149 | syl 17 |
. . . 4
 
         
                    
      |
151 | 65, 150 | eqsstrd 3477 |
. . 3
 
         
                ↾t          |
152 | | tgfiss 20055 |
. . 3
              
                ↾t                       
                ↾t            |
153 | 56, 151, 152 | syl2anc 671 |
. 2
 
               
                ↾t            |
154 | 55, 153 | eqsstrd 3477 |
1
 
 
↾t    
     |