Step | Hyp | Ref
| Expression |
1 | | llytop 20499 |
. . 3
 Locally
  |
2 | | resttop 20188 |
. . 3
 
 
↾t    |
3 | 1, 2 | sylan 474 |
. 2
  Locally
 
↾t    |
4 | | restopn2 20205 |
. . . . 5
 
   ↾t 

    |
5 | 1, 4 | sylan 474 |
. . . 4
  Locally
   ↾t 

    |
6 | | simp1l 1033 |
. . . . . . . . 9
   Locally
 
 
Locally   |
7 | | simp2l 1035 |
. . . . . . . . 9
   Locally
 
 
  |
8 | | simp3 1011 |
. . . . . . . . 9
   Locally
 
 
  |
9 | | llyi 20501 |
. . . . . . . . 9
  Locally
  

↾t     |
10 | 6, 7, 8, 9 | syl3anc 1269 |
. . . . . . . 8
   Locally
 
 

  ↾t     |
11 | | simprl 765 |
. . . . . . . . . . . . 13
    Locally 

   

↾t       |
12 | | simprr1 1057 |
. . . . . . . . . . . . . 14
    Locally 

   

↾t       |
13 | | simpl2r 1063 |
. . . . . . . . . . . . . 14
    Locally 

   

↾t       |
14 | 12, 13 | sstrd 3444 |
. . . . . . . . . . . . 13
    Locally 

   

↾t       |
15 | 6, 1 | syl 17 |
. . . . . . . . . . . . . . 15
   Locally
 
 
  |
16 | 15 | adantr 467 |
. . . . . . . . . . . . . 14
    Locally 

   

↾t       |
17 | | simpl1r 1061 |
. . . . . . . . . . . . . 14
    Locally 

   

↾t       |
18 | | restopn2 20205 |
. . . . . . . . . . . . . 14
 
   ↾t 

    |
19 | 16, 17, 18 | syl2anc 667 |
. . . . . . . . . . . . 13
    Locally 

   

↾t      
↾t 

    |
20 | 11, 14, 19 | mpbir2and 934 |
. . . . . . . . . . . 12
    Locally 

   

↾t      ↾t    |
21 | | selpw 3960 |
. . . . . . . . . . . . 13
 
  |
22 | 12, 21 | sylibr 216 |
. . . . . . . . . . . 12
    Locally 

   

↾t        |
23 | 20, 22 | elind 3620 |
. . . . . . . . . . 11
    Locally 

   

↾t      
↾t      |
24 | | simprr2 1058 |
. . . . . . . . . . 11
    Locally 

   

↾t       |
25 | | restabs 20193 |
. . . . . . . . . . . . 13
    
↾t 
↾t  
↾t    |
26 | 16, 14, 17, 25 | syl3anc 1269 |
. . . . . . . . . . . 12
    Locally 

   

↾t       ↾t  ↾t   ↾t    |
27 | | simprr3 1059 |
. . . . . . . . . . . 12
    Locally 

   

↾t      ↾t    |
28 | 26, 27 | eqeltrd 2531 |
. . . . . . . . . . 11
    Locally 

   

↾t       ↾t  ↾t    |
29 | 23, 24, 28 | jca32 538 |
. . . . . . . . . 10
    Locally 

   

↾t        ↾t       ↾t 
↾t      |
30 | 29 | ex 436 |
. . . . . . . . 9
   Locally
 
 
  

↾t      
↾t       ↾t  ↾t       |
31 | 30 | reximdv2 2860 |
. . . . . . . 8
   Locally
 
 
 


↾t      ↾t        ↾t  ↾t      |
32 | 10, 31 | mpd 15 |
. . . . . . 7
   Locally
 
 
   ↾t        ↾t  ↾t     |
33 | 32 | 3expa 1209 |
. . . . . 6
    Locally 

 
   
↾t       
↾t 
↾t     |
34 | 33 | ralrimiva 2804 |
. . . . 5
   Locally
 
 

   ↾t        ↾t  ↾t     |
35 | 34 | ex 436 |
. . . 4
  Locally
    
   ↾t        ↾t  ↾t      |
36 | 5, 35 | sylbid 219 |
. . 3
  Locally
   ↾t  
   ↾t        ↾t  ↾t      |
37 | 36 | ralrimiv 2802 |
. 2
  Locally
   ↾t   
   ↾t        ↾t  ↾t     |
38 | | islly 20495 |
. 2
  ↾t  Locally
  ↾t    ↾t   
   ↾t        ↾t  ↾t      |
39 | 3, 37, 38 | sylanbrc 671 |
1
  Locally
 
↾t  Locally   |