Step | Hyp | Ref
| Expression |
1 | | nllytop 20481 |
. . 3
 𝑛Locally   |
2 | | resttop 20169 |
. . 3
 
     
↾t    |
3 | 1, 2 | sylan 474 |
. 2
 
𝑛Locally
    
 ↾t    |
4 | | elrest 15319 |
. . . 4
 
𝑛Locally
    
 
↾t 


    |
5 | | simpll 759 |
. . . . . . . . . 10
   𝑛Locally      
    𝑛Locally   |
6 | | simprl 763 |
. . . . . . . . . 10
   𝑛Locally      
      |
7 | | inss1 3651 |
. . . . . . . . . . 11
   |
8 | | simprr 765 |
. . . . . . . . . . 11
   𝑛Locally      
        |
9 | 7, 8 | sseldi 3429 |
. . . . . . . . . 10
   𝑛Locally      
      |
10 | | nlly2i 20484 |
. . . . . . . . . 10
 
𝑛Locally

  

 ↾t     |
11 | 5, 6, 9, 10 | syl3anc 1267 |
. . . . . . . . 9
   𝑛Locally      
       

↾t     |
12 | 3 | ad2antrr 731 |
. . . . . . . . . . . . . 14
    𝑛Locally
                ↾t     
↾t    |
13 | 1 | ad3antrrr 735 |
. . . . . . . . . . . . . . . 16
    𝑛Locally
                ↾t    
  |
14 | | simpllr 768 |
. . . . . . . . . . . . . . . 16
    𝑛Locally
                ↾t    
      |
15 | | simprlr 772 |
. . . . . . . . . . . . . . . 16
    𝑛Locally
                ↾t    
  |
16 | | elrestr 15320 |
. . . . . . . . . . . . . . . 16
 
     
 
↾t    |
17 | 13, 14, 15, 16 | syl3anc 1267 |
. . . . . . . . . . . . . . 15
    𝑛Locally
                ↾t        ↾t    |
18 | | simprr1 1055 |
. . . . . . . . . . . . . . . 16
    𝑛Locally
                ↾t       |
19 | | inss2 3652 |
. . . . . . . . . . . . . . . . 17
   |
20 | | simplrr 770 |
. . . . . . . . . . . . . . . . 17
    𝑛Locally
                ↾t         |
21 | 19, 20 | sseldi 3429 |
. . . . . . . . . . . . . . . 16
    𝑛Locally
                ↾t       |
22 | 18, 21 | elind 3617 |
. . . . . . . . . . . . . . 15
    𝑛Locally
                ↾t         |
23 | | opnneip 20128 |
. . . . . . . . . . . . . . 15
  
↾t     ↾t     
      ↾t          |
24 | 12, 17, 22, 23 | syl3anc 1267 |
. . . . . . . . . . . . . 14
    𝑛Locally
                ↾t            ↾t          |
25 | | simprr2 1056 |
. . . . . . . . . . . . . . 15
    𝑛Locally
                ↾t       |
26 | | ssrin 3656 |
. . . . . . . . . . . . . . 15
 
     |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
    𝑛Locally
                ↾t      
    |
28 | | inss2 3652 |
. . . . . . . . . . . . . . 15
   |
29 | | eqid 2450 |
. . . . . . . . . . . . . . . . . 18
   |
30 | 29 | cldss 20037 |
. . . . . . . . . . . . . . . . 17
    
   |
31 | 14, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
    𝑛Locally
                ↾t        |
32 | 29 | restuni 20171 |
. . . . . . . . . . . . . . . 16
     
↾t    |
33 | 13, 31, 32 | syl2anc 666 |
. . . . . . . . . . . . . . 15
    𝑛Locally
                ↾t    
  ↾t    |
34 | 28, 33 | syl5sseq 3479 |
. . . . . . . . . . . . . 14
    𝑛Locally
                ↾t      
  ↾t    |
35 | | eqid 2450 |
. . . . . . . . . . . . . . 15
  ↾t   
↾t   |
36 | 35 | ssnei2 20125 |
. . . . . . . . . . . . . 14
    ↾t  
      ↾t              
   ↾t    
      ↾t          |
37 | 12, 24, 27, 34, 36 | syl22anc 1268 |
. . . . . . . . . . . . 13
    𝑛Locally
                ↾t            ↾t          |
38 | | simprll 771 |
. . . . . . . . . . . . . . . 16
    𝑛Locally
                ↾t        |
39 | 38 | elpwid 3960 |
. . . . . . . . . . . . . . 15
    𝑛Locally
                ↾t    
  |
40 | | ssrin 3656 |
. . . . . . . . . . . . . . 15
 
     |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
    𝑛Locally
                ↾t      
    |
42 | | vex 3047 |
. . . . . . . . . . . . . . . 16
 |
43 | 42 | inex1 4543 |
. . . . . . . . . . . . . . 15
   |
44 | 43 | elpw 3956 |
. . . . . . . . . . . . . 14
     
  
   |
45 | 41, 44 | sylibr 216 |
. . . . . . . . . . . . 13
    𝑛Locally
                ↾t        
   |
46 | 37, 45 | elind 3617 |
. . . . . . . . . . . 12
    𝑛Locally
                ↾t             ↾t              |
47 | 28 | a1i 11 |
. . . . . . . . . . . . . . 15
    𝑛Locally
                ↾t      
  |
48 | | restabs 20174 |
. . . . . . . . . . . . . . 15
   
       ↾t  ↾t     ↾t      |
49 | 13, 47, 14, 48 | syl3anc 1267 |
. . . . . . . . . . . . . 14
    𝑛Locally
                ↾t       ↾t  ↾t     ↾t      |
50 | | inss1 3651 |
. . . . . . . . . . . . . . . 16
   |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . 15
    𝑛Locally
                ↾t      
  |
52 | | restabs 20174 |
. . . . . . . . . . . . . . 15
   
 
  ↾t 
↾t    
↾t      |
53 | 13, 51, 38, 52 | syl3anc 1267 |
. . . . . . . . . . . . . 14
    𝑛Locally
                ↾t       ↾t  ↾t     ↾t      |
54 | 49, 53 | eqtr4d 2487 |
. . . . . . . . . . . . 13
    𝑛Locally
                ↾t       ↾t  ↾t      ↾t 
↾t      |
55 | | simprr3 1057 |
. . . . . . . . . . . . . 14
    𝑛Locally
                ↾t     
↾t    |
56 | | incom 3624 |
. . . . . . . . . . . . . . 15
     |
57 | | eqid 2450 |
. . . . . . . . . . . . . . . . 17
     |
58 | | ineq1 3626 |
. . . . . . . . . . . . . . . . . . 19
 
     |
59 | 58 | eqeq2d 2460 |
. . . . . . . . . . . . . . . . . 18
     
       |
60 | 59 | rspcev 3149 |
. . . . . . . . . . . . . . . . 17
                       |
61 | 14, 57, 60 | sylancl 667 |
. . . . . . . . . . . . . . . 16
    𝑛Locally
                ↾t     
           |
62 | | simplrl 769 |
. . . . . . . . . . . . . . . . . . 19
    𝑛Locally
                ↾t    
  |
63 | | elssuni 4226 |
. . . . . . . . . . . . . . . . . . 19
    |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . 18
    𝑛Locally
                ↾t        |
65 | 39, 64 | sstrd 3441 |
. . . . . . . . . . . . . . . . 17
    𝑛Locally
                ↾t    
   |
66 | 29 | restcld 20181 |
. . . . . . . . . . . . . . . . 17
           ↾t  
             |
67 | 13, 65, 66 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
    𝑛Locally
                ↾t            ↾t  
             |
68 | 61, 67 | mpbird 236 |
. . . . . . . . . . . . . . 15
    𝑛Locally
                ↾t          
↾t     |
69 | 56, 68 | syl5eqel 2532 |
. . . . . . . . . . . . . 14
    𝑛Locally
                ↾t          
↾t     |
70 | | cmpcld 20410 |
. . . . . . . . . . . . . 14
  
↾t        ↾t      ↾t  ↾t      |
71 | 55, 69, 70 | syl2anc 666 |
. . . . . . . . . . . . 13
    𝑛Locally
                ↾t       ↾t  ↾t      |
72 | 54, 71 | eqeltrd 2528 |
. . . . . . . . . . . 12
    𝑛Locally
                ↾t       ↾t  ↾t      |
73 | | oveq2 6296 |
. . . . . . . . . . . . . 14
    
↾t 
↾t    ↾t  ↾t      |
74 | 73 | eleq1d 2512 |
. . . . . . . . . . . . 13
      ↾t  ↾t 
  ↾t 
↾t       |
75 | 74 | rspcev 3149 |
. . . . . . . . . . . 12
          ↾t              ↾t  ↾t            ↾t               ↾t  ↾t    |
76 | 46, 72, 75 | syl2anc 666 |
. . . . . . . . . . 11
    𝑛Locally
                ↾t     
      ↾t               ↾t  ↾t    |
77 | 76 | expr 619 |
. . . . . . . . . 10
    𝑛Locally
               

↾t         
↾t               ↾t  ↾t     |
78 | 77 | rexlimdvva 2885 |
. . . . . . . . 9
   𝑛Locally      
       

 ↾t          ↾t               ↾t  ↾t     |
79 | 11, 78 | mpd 15 |
. . . . . . . 8
   𝑛Locally      
           ↾t               ↾t  ↾t    |
80 | 79 | anassrs 653 |
. . . . . . 7
    𝑛Locally
     

 
      
↾t               ↾t  ↾t    |
81 | 80 | ralrimiva 2801 |
. . . . . 6
   𝑛Locally                 
↾t               ↾t  ↾t    |
82 | | pweq 3953 |
. . . . . . . . 9
   
 
   |
83 | 82 | ineq2d 3633 |
. . . . . . . 8
         ↾t                ↾t              |
84 | 83 | rexeqdv 2993 |
. . . . . . 7
    
      ↾t             ↾t  ↾t 
      
↾t               ↾t  ↾t     |
85 | 84 | raleqbi1dv 2994 |
. . . . . 6
    

      ↾t             ↾t  ↾t 
          
↾t               ↾t  ↾t     |
86 | 81, 85 | syl5ibrcom 226 |
. . . . 5
   𝑛Locally          

      ↾t             ↾t  ↾t     |
87 | 86 | rexlimdva 2878 |
. . . 4
 
𝑛Locally
    
 
  
      
↾t             ↾t  ↾t     |
88 | 4, 87 | sylbid 219 |
. . 3
 
𝑛Locally
    
 
↾t  
      
↾t             ↾t  ↾t     |
89 | 88 | ralrimiv 2799 |
. 2
 
𝑛Locally
    
 
↾t   
      
↾t             ↾t  ↾t    |
90 | | isnlly 20477 |
. 2
  ↾t  𝑛Locally
  ↾t    ↾t   
      
↾t             ↾t  ↾t     |
91 | 3, 89, 90 | sylanbrc 669 |
1
 
𝑛Locally
    
 ↾t 
𝑛Locally   |