Step | Hyp | Ref
| Expression |
1 | | nllytop 20481 |
. . . . . 6
 𝑛Locally
  |
2 | 1 | adantl 468 |
. . . . 5
 
𝑛Locally 
  |
3 | | nlly2i 20484 |
. . . . . . . . 9
 
𝑛Locally
   

 ↾t     |
4 | 3 | 3adant1l 1259 |
. . . . . . . 8
   𝑛Locally 
   

 ↾t     |
5 | | simprl 763 |
. . . . . . . . . . . . 13
    
𝑛Locally 

   

↾t       |
6 | | simprr2 1056 |
. . . . . . . . . . . . . . 15
    
𝑛Locally 

   

↾t       |
7 | | simplr 761 |
. . . . . . . . . . . . . . . 16
    
𝑛Locally 

   

↾t        |
8 | 7 | elpwid 3960 |
. . . . . . . . . . . . . . 15
    
𝑛Locally 

   

↾t       |
9 | 6, 8 | sstrd 3441 |
. . . . . . . . . . . . . 14
    
𝑛Locally 

   

↾t       |
10 | | selpw 3957 |
. . . . . . . . . . . . . 14
 
  |
11 | 9, 10 | sylibr 216 |
. . . . . . . . . . . . 13
    
𝑛Locally 

   

↾t        |
12 | 5, 11 | elind 3617 |
. . . . . . . . . . . 12
    
𝑛Locally 

   

↾t          |
13 | | simprr1 1055 |
. . . . . . . . . . . 12
    
𝑛Locally 

   

↾t       |
14 | | simpll1 1046 |
. . . . . . . . . . . . . . . 16
    
𝑛Locally 

   

↾t     
𝑛Locally    |
15 | 14 | simprd 465 |
. . . . . . . . . . . . . . 15
    
𝑛Locally 

   

↾t     𝑛Locally   |
16 | 15, 1 | syl 17 |
. . . . . . . . . . . . . 14
    
𝑛Locally 

   

↾t       |
17 | | restabs 20174 |
. . . . . . . . . . . . . 14
      ↾t  ↾t   ↾t    |
18 | 16, 6, 7, 17 | syl3anc 1267 |
. . . . . . . . . . . . 13
    
𝑛Locally 

   

↾t       ↾t  ↾t   ↾t    |
19 | | simprr3 1057 |
. . . . . . . . . . . . . 14
    
𝑛Locally 

   

↾t      ↾t    |
20 | 14 | simpld 461 |
. . . . . . . . . . . . . . 15
    
𝑛Locally 

   

↾t       |
21 | | restlly.1 |
. . . . . . . . . . . . . . . . 17
 

  
↾t    |
22 | 21 | expr 619 |
. . . . . . . . . . . . . . . 16
 
  
↾t     |
23 | 22 | ralrimiva 2801 |
. . . . . . . . . . . . . . 15
  

↾t     |
24 | 20, 23 | syl 17 |
. . . . . . . . . . . . . 14
    
𝑛Locally 

   

↾t      

↾t     |
25 | | df-ss 3417 |
. . . . . . . . . . . . . . . 16

    |
26 | 6, 25 | sylib 200 |
. . . . . . . . . . . . . . 15
    
𝑛Locally 

   

↾t         |
27 | | elrestr 15320 |
. . . . . . . . . . . . . . . 16
 


   ↾t    |
28 | 16, 7, 5, 27 | syl3anc 1267 |
. . . . . . . . . . . . . . 15
    
𝑛Locally 

   

↾t        ↾t    |
29 | 26, 28 | eqeltrrd 2529 |
. . . . . . . . . . . . . 14
    
𝑛Locally 

   

↾t      ↾t    |
30 | | eleq2 2517 |
. . . . . . . . . . . . . . . 16
  ↾t  
 ↾t     |
31 | | oveq1 6295 |
. . . . . . . . . . . . . . . . 17
  ↾t   ↾t    ↾t  ↾t    |
32 | 31 | eleq1d 2512 |
. . . . . . . . . . . . . . . 16
  ↾t    ↾t 
  ↾t 
↾t     |
33 | 30, 32 | imbi12d 322 |
. . . . . . . . . . . . . . 15
  ↾t     ↾t    
↾t    ↾t  ↾t      |
34 | 33 | rspcv 3145 |
. . . . . . . . . . . . . 14
  ↾t    
 ↾t    
↾t    ↾t  ↾t      |
35 | 19, 24, 29, 34 | syl3c 63 |
. . . . . . . . . . . . 13
    
𝑛Locally 

   

↾t       ↾t  ↾t    |
36 | 18, 35 | eqeltrrd 2529 |
. . . . . . . . . . . 12
    
𝑛Locally 

   

↾t      ↾t    |
37 | 12, 13, 36 | jca32 538 |
. . . . . . . . . . 11
    
𝑛Locally 

   

↾t          
↾t      |
38 | 37 | ex 436 |
. . . . . . . . . 10
   
𝑛Locally 

      ↾t         
↾t       |
39 | 38 | reximdv2 2857 |
. . . . . . . . 9
   
𝑛Locally 

   


↾t          ↾t      |
40 | 39 | rexlimdva 2878 |
. . . . . . . 8
   𝑛Locally 
  
  

↾t          ↾t      |
41 | 4, 40 | mpd 15 |
. . . . . . 7
   𝑛Locally 
        ↾t     |
42 | 41 | 3expb 1208 |
. . . . . 6
   𝑛Locally  
 
       ↾t     |
43 | 42 | ralrimivva 2808 |
. . . . 5
 
𝑛Locally 


       ↾t     |
44 | | islly 20476 |
. . . . 5
 Locally



       ↾t      |
45 | 2, 43, 44 | sylanbrc 669 |
. . . 4
 
𝑛Locally 
Locally   |
46 | 45 | ex 436 |
. . 3
  𝑛Locally
Locally    |
47 | 46 | ssrdv 3437 |
. 2
 𝑛Locally Locally   |
48 | | llyssnlly 20486 |
. . 3
Locally 𝑛Locally  |
49 | 48 | a1i 11 |
. 2
 Locally
𝑛Locally   |
50 | 47, 49 | eqssd 3448 |
1
 𝑛Locally Locally   |