Step | Hyp | Ref
| Expression |
1 | | simpl1 952 |
. . . . . . . . 9
    
             
  |
2 | | simpl3 954 |
. . . . . . . . 9
    
             
  |
3 | | cnprest.1 |
. . . . . . . . . 10
  |
4 | 3 | ntrss2 12072 |
. . . . . . . . 9
             |
5 | 1, 2, 4 | syl2anc 406 |
. . . . . . . 8
    
             
          |
6 | | simprl 501 |
. . . . . . . 8
    
             
          |
7 | 5, 6 | sseldd 3048 |
. . . . . . 7
    
             
  |
8 | | fvres 5377 |
. . . . . . 7
             |
9 | 7, 8 | syl 14 |
. . . . . 6
    
             
            |
10 | 9 | eqcomd 2105 |
. . . . 5
    
             
            |
11 | 10 | eleq1d 2168 |
. . . 4
    
             
    
         |
12 | | inss1 3243 |
. . . . . . . . 9
   |
13 | | imass2 4851 |
. . . . . . . . 9
               |
14 | | sstr2 3054 |
. . . . . . . . 9
               
         |
15 | 12, 13, 14 | mp2b 8 |
. . . . . . . 8
             |
16 | 15 | anim2i 337 |
. . . . . . 7
           
 
   |
17 | 16 | reximi 2488 |
. . . . . 6
        

   
 
   |
18 | 3 | ntropn 12068 |
. . . . . . . . . . . . 13
             |
19 | 1, 2, 18 | syl2anc 406 |
. . . . . . . . . . . 12
    
             
          |
20 | | inopn 11952 |
. . . . . . . . . . . . . 14
 
         
           |
21 | 20 | 3com23 1155 |
. . . . . . . . . . . . 13
         
 
           |
22 | 21 | 3expia 1151 |
. . . . . . . . . . . 12
                         |
23 | 1, 19, 22 | syl2anc 406 |
. . . . . . . . . . 11
    
             

             |
24 | | elin 3206 |
. . . . . . . . . . . . . 14
                       |
25 | 24 | simplbi2com 1388 |
. . . . . . . . . . . . 13
        

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

             |
27 | | sslin 3249 |
. . . . . . . . . . . . . 14
        
         
    |
28 | | imass2 4851 |
. . . . . . . . . . . . . 14
                                   |
29 | 5, 27, 28 | 3syl 17 |
. . . . . . . . . . . . 13
    
             
                      |
30 | | sstr2 3054 |
. . . . . . . . . . . . 13
                                             |
31 | 29, 30 | syl 14 |
. . . . . . . . . . . 12
    
             
                        |
32 | 26, 31 | anim12d 331 |
. . . . . . . . . . 11
    
             
 
                                    |
33 | 23, 32 | anim12d 331 |
. . . . . . . . . 10
    
             
  
   
 
 
 
                   
                   |
34 | | eleq2 2163 |
. . . . . . . . . . . 12
          


            |
35 | | imaeq2 4813 |
. . . . . . . . . . . . 13
          
                    |
36 | 35 | sseq1d 3076 |
. . . . . . . . . . . 12
          
        
             |
37 | 34, 36 | anbi12d 460 |
. . . . . . . . . . 11
          
 
    
          
                  |
38 | 37 | rspcev 2744 |
. . . . . . . . . 10
            

                         

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


        |
40 | 39 | expdimp 257 |
. . . . . . . 8
   

                     
 
  
   
    |
41 | 40 | rexlimdva 2508 |
. . . . . . 7
    
             
 

       

   
    |
42 | | eleq2 2163 |
. . . . . . . . 9
 
   |
43 | | imaeq2 4813 |
. . . . . . . . . 10
           |
44 | 43 | sseq1d 3076 |
. . . . . . . . 9
     
       |
45 | 42, 44 | anbi12d 460 |
. . . . . . . 8
                 |
46 | 45 | cbvrexv 2613 |
. . . . . . 7
       


       |
47 | 41, 46 | syl6ib 160 |
. . . . . 6
    
             
 

       

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

    


          |
49 | | vex 2644 |
. . . . . . . 8
 |
50 | 49 | inex1 4002 |
. . . . . . 7
   |
51 | 50 | a1i 9 |
. . . . . 6
   

                
   |
52 | | uniexg 4299 |
. . . . . . . . 9
    |
53 | 1, 52 | syl 14 |
. . . . . . . 8
    
             
   |
54 | 2, 3 | syl6sseq 3095 |
. . . . . . . 8
    
             
   |
55 | 53, 54 | ssexd 4008 |
. . . . . . 7
    
             
  |
56 | | elrest 11909 |
. . . . . . 7
 
   ↾t 


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


    |
58 | | eleq2 2163 |
. . . . . . . 8
   

    |
59 | | elin 3206 |
. . . . . . . . . 10
  

   |
60 | 59 | rbaib 874 |
. . . . . . . . 9
 
 
   |
61 | 7, 60 | syl 14 |
. . . . . . . 8
    
             
  
   |
62 | 58, 61 | sylan9bbr 454 |
. . . . . . 7
   

                  
   |
63 | | simpr 109 |
. . . . . . . . . 10
   

                      |
64 | 63 | imaeq2d 4817 |
. . . . . . . . 9
   

                             
    |
65 | | inss2 3244 |
. . . . . . . . . 10
   |
66 | | resima2 4789 |
. . . . . . . . . 10
              
    |
67 | 65, 66 | ax-mp 7 |
. . . . . . . . 9
 
         
   |
68 | 64, 67 | syl6eq 2148 |
. . . . . . . 8
   

                           
    |
69 | 68 | sseq1d 3076 |
. . . . . . 7
   

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

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


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

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

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

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

TopOn    |
76 | 1, 75 | sylib 121 |
. . . 4
    
             
TopOn    |
77 | | simpl2 953 |
. . . . 5
    
             
  |
78 | | cnprest.2 |
. . . . . 6
  |
79 | 78 | toptopon 11967 |
. . . . 5

TopOn    |
80 | 77, 79 | sylib 121 |
. . . 4
    
             
TopOn    |
81 | 2, 7 | sseldd 3048 |
. . . 4
    
             
  |
82 | | iscnp 12149 |
. . . 4
  TopOn  TopOn 

                 


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


          |
84 | | simprr 502 |
. . . 4
    
             
      |
85 | 84 | biantrurd 301 |
. . 3
    
             
 
     

   
       
    


          |
86 | 83, 85 | bitr4d 190 |
. 2
    
             
       
      
   
     |
87 | | simp1l 973 |
. . . . . . 7
  
                  |
88 | 87, 75 | sylib 121 |
. . . . . 6
  
                TopOn    |
89 | | simp1r 974 |
. . . . . 6
  
                  |
90 | | resttopon 12122 |
. . . . . 6
  TopOn    ↾t  TopOn    |
91 | 88, 89, 90 | syl2anc 406 |
. . . . 5
  
                 ↾t  TopOn    |
92 | | simp3 951 |
. . . . . 6
  
                  |
93 | 92, 79 | sylib 121 |
. . . . 5
  
                TopOn    |
94 | 4 | 3ad2ant1 970 |
. . . . . 6
  
                       
  |
95 | | simp2l 975 |
. . . . . 6
  
                          |
96 | 94, 95 | sseldd 3048 |
. . . . 5
  
                  |
97 | | iscnp 12149 |
. . . . 5
  
↾t  TopOn  TopOn 

      ↾t     
       
       
 ↾t                |
98 | 91, 93, 96, 97 | syl3anc 1184 |
. . . 4
  
                      ↾t     
       
       
 ↾t                |
99 | | simp2r 976 |
. . . . . 6
  
                      |
100 | 99, 89 | fssresd 5235 |
. . . . 5
  
                        |
101 | 100 | biantrurd 301 |
. . . 4
  
                 
      
 
↾t           
       
       
 ↾t                |
102 | 98, 101 | bitr4d 190 |
. . 3
  
                      ↾t     

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

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