Step | Hyp | Ref
| Expression |
1 | | simpl1 1000 |
. . . . . . . . 9
    
             
  |
2 | | simpl3 1002 |
. . . . . . . . 9
    
             
  |
3 | | cnprest.1 |
. . . . . . . . . 10
  |
4 | 3 | ntrss2 13591 |
. . . . . . . . 9
             |
5 | 1, 2, 4 | syl2anc 411 |
. . . . . . . 8
    
             
          |
6 | | simprl 529 |
. . . . . . . 8
    
             
          |
7 | 5, 6 | sseldd 3156 |
. . . . . . 7
    
             
  |
8 | | fvres 5539 |
. . . . . . 7
             |
9 | 7, 8 | syl 14 |
. . . . . 6
    
             
            |
10 | 9 | eqcomd 2183 |
. . . . 5
    
             
            |
11 | 10 | eleq1d 2246 |
. . . 4
    
             
    
         |
12 | | inss1 3355 |
. . . . . . . . 9
   |
13 | | imass2 5004 |
. . . . . . . . 9
               |
14 | | sstr2 3162 |
. . . . . . . . 9
               
         |
15 | 12, 13, 14 | mp2b 8 |
. . . . . . . 8
             |
16 | 15 | anim2i 342 |
. . . . . . 7
           
 
   |
17 | 16 | reximi 2574 |
. . . . . 6
        

   
 
   |
18 | 3 | ntropn 13587 |
. . . . . . . . . . . . 13
             |
19 | 1, 2, 18 | syl2anc 411 |
. . . . . . . . . . . 12
    
             
          |
20 | | inopn 13473 |
. . . . . . . . . . . . . 14
 
         
           |
21 | 20 | 3com23 1209 |
. . . . . . . . . . . . 13
         
 
           |
22 | 21 | 3expia 1205 |
. . . . . . . . . . . 12
                         |
23 | 1, 19, 22 | syl2anc 411 |
. . . . . . . . . . 11
    
             

             |
24 | | elin 3318 |
. . . . . . . . . . . . . 14
                       |
25 | 24 | simplbi2com 1444 |
. . . . . . . . . . . . 13
        

             |
26 | 6, 25 | syl 14 |
. . . . . . . . . . . 12
    
             

             |
27 | | sslin 3361 |
. . . . . . . . . . . . . 14
        
         
    |
28 | | imass2 5004 |
. . . . . . . . . . . . . 14
                                   |
29 | 5, 27, 28 | 3syl 17 |
. . . . . . . . . . . . 13
    
             
                      |
30 | | sstr2 3162 |
. . . . . . . . . . . . 13
                                             |
31 | 29, 30 | syl 14 |
. . . . . . . . . . . 12
    
             
                        |
32 | 26, 31 | anim12d 335 |
. . . . . . . . . . 11
    
             
 
                                    |
33 | 23, 32 | anim12d 335 |
. . . . . . . . . 10
    
             
  
   
 
 
 
                   
                   |
34 | | eleq2 2241 |
. . . . . . . . . . . 12
          


            |
35 | | imaeq2 4966 |
. . . . . . . . . . . . 13
          
                    |
36 | 35 | sseq1d 3184 |
. . . . . . . . . . . 12
          
        
             |
37 | 34, 36 | anbi12d 473 |
. . . . . . . . . . 11
          
 
    
          
                  |
38 | 37 | rspcev 2841 |
. . . . . . . . . 10
            

                         

   
   |
39 | 33, 38 | syl6 33 |
. . . . . . . . 9
    
             
  
   
 
 


        |
40 | 39 | expdimp 259 |
. . . . . . . 8
   

                     
 
  
   
    |
41 | 40 | rexlimdva 2594 |
. . . . . . 7
    
             
 

       

   
    |
42 | | eleq2 2241 |
. . . . . . . . 9
 
   |
43 | | imaeq2 4966 |
. . . . . . . . . 10
           |
44 | 43 | sseq1d 3184 |
. . . . . . . . 9
     
       |
45 | 42, 44 | anbi12d 473 |
. . . . . . . 8
                 |
46 | 45 | cbvrexv 2704 |
. . . . . . 7
       


       |
47 | 41, 46 | imbitrdi 161 |
. . . . . 6
    
             
 

       

   
    |
48 | 17, 47 | impbid2 143 |
. . . . 5
    
             
 

    


          |
49 | | vex 2740 |
. . . . . . . 8
 |
50 | 49 | inex1 4137 |
. . . . . . 7
   |
51 | 50 | a1i 9 |
. . . . . 6
   

                
   |
52 | | uniexg 4439 |
. . . . . . . . 9
    |
53 | 1, 52 | syl 14 |
. . . . . . . 8
    
             
   |
54 | 2, 3 | sseqtrdi 3203 |
. . . . . . . 8
    
             
   |
55 | 53, 54 | ssexd 4143 |
. . . . . . 7
    
             
  |
56 | | elrest 12694 |
. . . . . . 7
 
   ↾t 


    |
57 | 1, 55, 56 | syl2anc 411 |
. . . . . 6
    
             
 
↾t 


    |
58 | | eleq2 2241 |
. . . . . . . 8
   

    |
59 | | elin 3318 |
. . . . . . . . . 10
  

   |
60 | 59 | rbaib 921 |
. . . . . . . . 9
 
 
   |
61 | 7, 60 | syl 14 |
. . . . . . . 8
    
             
  
   |
62 | 58, 61 | sylan9bbr 463 |
. . . . . . 7
   

                  
   |
63 | | simpr 110 |
. . . . . . . . . 10
   

                      |
64 | 63 | imaeq2d 4970 |
. . . . . . . . 9
   

                             
    |
65 | | inss2 3356 |
. . . . . . . . . 10
   |
66 | | resima2 4941 |
. . . . . . . . . 10
              
    |
67 | 65, 66 | ax-mp 5 |
. . . . . . . . 9
 
         
   |
68 | 64, 67 | eqtrdi 2226 |
. . . . . . . 8
   

                           
    |
69 | 68 | sseq1d 3184 |
. . . . . . 7
   

                        
         |
70 | 62, 69 | anbi12d 473 |
. . . . . 6
   

                         
            |
71 | 51, 57, 70 | rexxfr2d 4465 |
. . . . 5
    
             
 
 ↾t     
    


          |
72 | 48, 71 | bitr4d 191 |
. . . 4
    
             
 

    
 
↾t              |
73 | 11, 72 | imbi12d 234 |
. . 3
    
             
      

   
    
      ↾t               |
74 | 73 | ralbidv 2477 |
. 2
    
             
 
     

   
          
 ↾t               |
75 | 3 | toptopon 13488 |
. . . . 5

TopOn    |
76 | 1, 75 | sylib 122 |
. . . 4
    
             
TopOn    |
77 | | simpl2 1001 |
. . . . 5
    
             
  |
78 | | cnprest.2 |
. . . . . 6
  |
79 | 78 | toptopon 13488 |
. . . . 5

TopOn    |
80 | 77, 79 | sylib 122 |
. . . 4
    
             
TopOn    |
81 | 2, 7 | sseldd 3156 |
. . . 4
    
             
  |
82 | | iscnp 13669 |
. . . 4
  TopOn  TopOn 

                 


          |
83 | 76, 80, 81, 82 | syl3anc 1238 |
. . 3
    
             
                 


          |
84 | | simprr 531 |
. . . 4
    
             
      |
85 | 84 | biantrurd 305 |
. . 3
    
             
 
     

   
       
    


          |
86 | 83, 85 | bitr4d 191 |
. 2
    
             
       
      
   
     |
87 | | simp1l 1021 |
. . . . . . 7
  
                  |
88 | 87, 75 | sylib 122 |
. . . . . 6
  
                TopOn    |
89 | | simp1r 1022 |
. . . . . 6
  
                  |
90 | | resttopon 13641 |
. . . . . 6
  TopOn    ↾t  TopOn    |
91 | 88, 89, 90 | syl2anc 411 |
. . . . 5
  
                 ↾t  TopOn    |
92 | | simp3 999 |
. . . . . 6
  
                  |
93 | 92, 79 | sylib 122 |
. . . . 5
  
                TopOn    |
94 | 4 | 3ad2ant1 1018 |
. . . . . 6
  
                       
  |
95 | | simp2l 1023 |
. . . . . 6
  
                          |
96 | 94, 95 | sseldd 3156 |
. . . . 5
  
                  |
97 | | iscnp 13669 |
. . . . 5
  
↾t  TopOn  TopOn 

      ↾t     
       
       
 ↾t                |
98 | 91, 93, 96, 97 | syl3anc 1238 |
. . . 4
  
                      ↾t     
       
       
 ↾t                |
99 | | simp2r 1024 |
. . . . . 6
  
                      |
100 | 99, 89 | fssresd 5392 |
. . . . 5
  
                        |
101 | 100 | biantrurd 305 |
. . . 4
  
                 
      
 
↾t           
       
       
 ↾t                |
102 | 98, 101 | bitr4d 191 |
. . 3
  
                      ↾t     

      
 
↾t               |
103 | 1, 2, 6, 84, 77, 102 | syl221anc 1249 |
. 2
    
             
      ↾t     

      
 
↾t               |
104 | 74, 86, 103 | 3bitr4d 220 |
1
    
             
            ↾t         |