Step | Hyp | Ref
| Expression |
1 | | simp1 1008 |
. . . . . 6
  TopOn     
 TopOn    |
2 | | filelss 20867 |
. . . . . . 7
         |
3 | 2 | 3adant1 1026 |
. . . . . 6
  TopOn     
   |
4 | | resttopon 20177 |
. . . . . 6
  TopOn    ↾t  TopOn    |
5 | 1, 3, 4 | syl2anc 667 |
. . . . 5
  TopOn     
  ↾t  TopOn    |
6 | | filfbas 20863 |
. . . . . . . 8
    
      |
7 | 6 | 3ad2ant2 1030 |
. . . . . . 7
  TopOn     
       |
8 | | simp3 1010 |
. . . . . . 7
  TopOn     
   |
9 | | fbncp 20854 |
. . . . . . 7
       
   |
10 | 7, 8, 9 | syl2anc 667 |
. . . . . 6
  TopOn     
 
   |
11 | | simp2 1009 |
. . . . . . 7
  TopOn     
       |
12 | | trfil3 20903 |
. . . . . . 7
        
↾t           |
13 | 11, 3, 12 | syl2anc 667 |
. . . . . 6
  TopOn     
  
↾t           |
14 | 10, 13 | mpbird 236 |
. . . . 5
  TopOn     
  ↾t        |
15 | | fclsopn 21029 |
. . . . 5
  
↾t  TopOn   ↾t      
   ↾t  
↾t  

 
↾t     
↾t          |
16 | 5, 14, 15 | syl2anc 667 |
. . . 4
  TopOn     
    ↾t   ↾t  

 
↾t     
↾t          |
17 | | in32 3644 |
. . . . . . . . . . . . . 14
         |
18 | | ineq2 3628 |
. . . . . . . . . . . . . 14
   
       |
19 | 17, 18 | syl5eq 2497 |
. . . . . . . . . . . . 13
   
       |
20 | 19 | neeq1d 2683 |
. . . . . . . . . . . 12
     
 
     |
21 | 20 | rspccv 3147 |
. . . . . . . . . . 11
 
  


       |
22 | | inss1 3652 |
. . . . . . . . . . . . 13
   |
23 | | ssrin 3657 |
. . . . . . . . . . . . 13
     
     |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . 12
    
  |
25 | | ssn0 3767 |
. . . . . . . . . . . 12
     
    
  
   |
26 | 24, 25 | mpan 676 |
. . . . . . . . . . 11
   

    |
27 | 21, 26 | syl6 34 |
. . . . . . . . . 10
 
  


     |
28 | 27 | ralrimiv 2800 |
. . . . . . . . 9
 
  


    |
29 | 11 | ad3antrrr 736 |
. . . . . . . . . . . 12
     TopOn 
    
         |
30 | | simpr 463 |
. . . . . . . . . . . 12
     TopOn 
    
     |
31 | 8 | ad3antrrr 736 |
. . . . . . . . . . . 12
     TopOn 
    
     |
32 | | filin 20869 |
. . . . . . . . . . . 12
     
 
   |
33 | 29, 30, 31, 32 | syl3anc 1268 |
. . . . . . . . . . 11
     TopOn 
    
   
   |
34 | | ineq2 3628 |
. . . . . . . . . . . . . 14
   
       |
35 | | inass 3642 |
. . . . . . . . . . . . . 14
     
   |
36 | 34, 35 | syl6eqr 2503 |
. . . . . . . . . . . . 13
   
       |
37 | 36 | neeq1d 2683 |
. . . . . . . . . . . 12
     
 
     |
38 | 37 | rspcv 3146 |
. . . . . . . . . . 11
    

   
    |
39 | 33, 38 | syl 17 |
. . . . . . . . . 10
     TopOn 
    
    

   
    |
40 | 39 | ralrimdva 2806 |
. . . . . . . . 9
    TopOn 
   


  

 
 
     |
41 | 28, 40 | impbid2 208 |
. . . . . . . 8
    TopOn 
   


  
   

     |
42 | 41 | imbi2d 318 |
. . . . . . 7
    TopOn 
   


        


      |
43 | 42 | ralbidva 2824 |
. . . . . 6
   TopOn     
   

     



      |
44 | | vex 3048 |
. . . . . . . . 9
 |
45 | 44 | inex1 4544 |
. . . . . . . 8
   |
46 | 45 | a1i 11 |
. . . . . . 7
    TopOn 
   


 
   |
47 | | elrest 15326 |
. . . . . . . . 9
  TopOn     ↾t  
     |
48 | 47 | 3adant2 1027 |
. . . . . . . 8
  TopOn     
   ↾t  
     |
49 | 48 | adantr 467 |
. . . . . . 7
   TopOn     
    ↾t  
     |
50 | | eleq2 2518 |
. . . . . . . . 9
   

    |
51 | | elin 3617 |
. . . . . . . . . . 11
  

   |
52 | 51 | rbaib 917 |
. . . . . . . . . 10
   
   |
53 | 52 | adantl 468 |
. . . . . . . . 9
   TopOn     
    
   |
54 | 50, 53 | sylan9bbr 707 |
. . . . . . . 8
    TopOn 
   



 

   |
55 | | vex 3048 |
. . . . . . . . . . . 12
 |
56 | 55 | inex1 4544 |
. . . . . . . . . . 11
   |
57 | 56 | a1i 11 |
. . . . . . . . . 10
    TopOn 
   


 
   |
58 | | elrest 15326 |
. . . . . . . . . . . 12
         ↾t  
     |
59 | 58 | 3adant1 1026 |
. . . . . . . . . . 11
  TopOn     
   ↾t  
     |
60 | 59 | adantr 467 |
. . . . . . . . . 10
   TopOn     
    ↾t  
     |
61 | | ineq2 3628 |
. . . . . . . . . . . 12
   
       |
62 | 61 | adantl 468 |
. . . . . . . . . . 11
    TopOn 
   


   
       |
63 | 62 | neeq1d 2683 |
. . . . . . . . . 10
    TopOn 
   


     
       |
64 | 57, 60, 63 | ralxfr2d 4616 |
. . . . . . . . 9
   TopOn     
   
 ↾t       
     |
65 | | ineq1 3627 |
. . . . . . . . . . . 12
   
      
    |
66 | | inindir 3650 |
. . . . . . . . . . . 12
       
   |
67 | 65, 66 | syl6eqr 2503 |
. . . . . . . . . . 11
   
         |
68 | 67 | neeq1d 2683 |
. . . . . . . . . 10
     
 
 
     |
69 | 68 | ralbidv 2827 |
. . . . . . . . 9
    
 
 

 
     |
70 | 64, 69 | sylan9bb 706 |
. . . . . . . 8
    TopOn 
   



 
 
 ↾t    

 
     |
71 | 54, 70 | imbi12d 322 |
. . . . . . 7
    TopOn 
   



 
  
 ↾t     


 
      |
72 | 46, 49, 71 | ralxfr2d 4616 |
. . . . . 6
   TopOn     
   
 ↾t     
↾t     
 
         |
73 | 1 | adantr 467 |
. . . . . . 7
   TopOn     
  TopOn    |
74 | 11 | adantr 467 |
. . . . . . 7
   TopOn     
        |
75 | 3 | sselda 3432 |
. . . . . . 7
   TopOn     
    |
76 | | fclsopn 21029 |
. . . . . . . 8
  TopOn         




       |
77 | 76 | baibd 920 |
. . . . . . 7
   TopOn          



      |
78 | 73, 74, 75, 77 | syl21anc 1267 |
. . . . . 6
   TopOn     
    



      |
79 | 43, 72, 78 | 3bitr4d 289 |
. . . . 5
   TopOn     
   
 ↾t     
↾t     
     |
80 | 79 | pm5.32da 647 |
. . . 4
  TopOn     
     ↾t     
↾t      

      |
81 | 16, 80 | bitrd 257 |
. . 3
  TopOn     
    ↾t   ↾t  

      |
82 | | elin 3617 |
. . . 4
           |
83 | | ancom 452 |
. . . 4
    

     |
84 | 82, 83 | bitri 253 |
. . 3
           |
85 | 81, 84 | syl6bbr 267 |
. 2
  TopOn     
    ↾t   ↾t  
       |
86 | 85 | eqrdv 2449 |
1
  TopOn     
  
↾t   ↾t         |