Step | Hyp | Ref
| Expression |
1 | | llytop 20487 |
. . . 4
 Locally
  |
2 | 1 | adantl 468 |
. . 3
 
Locally 
  |
3 | | simplr 762 |
. . . . . 6
   Locally   Locally   |
4 | 2 | adantr 467 |
. . . . . . 7
   Locally     |
5 | | islly2.2 |
. . . . . . . 8
  |
6 | 5 | topopn 19936 |
. . . . . . 7
   |
7 | 4, 6 | syl 17 |
. . . . . 6
   Locally     |
8 | | simpr 463 |
. . . . . 6
   Locally     |
9 | | llyi 20489 |
. . . . . 6
  Locally
  

↾t     |
10 | 3, 7, 8, 9 | syl3anc 1268 |
. . . . 5
   Locally   
  ↾t     |
11 | | 3simpc 1007 |
. . . . . 6
 

↾t  

 ↾t     |
12 | 11 | reximi 2855 |
. . . . 5
  

↾t  


 ↾t     |
13 | 10, 12 | syl 17 |
. . . 4
   Locally   

 ↾t     |
14 | 13 | ralrimiva 2802 |
. . 3
 
Locally 



 ↾t     |
15 | 2, 14 | jca 535 |
. 2
 
Locally 
 


 ↾t      |
16 | | simprl 764 |
. . 3
 
 


 ↾t    
  |
17 | | elssuni 4227 |
. . . . . . . . 9
    |
18 | 17, 5 | syl6sseqr 3479 |
. . . . . . . 8
   |
19 | 18 | adantl 468 |
. . . . . . 7
       |
20 | | ssralv 3493 |
. . . . . . 7
  

 
↾t  



 ↾t      |
21 | 19, 20 | syl 17 |
. . . . . 6
      

 
↾t  



 ↾t      |
22 | | simpllr 769 |
. . . . . . . . . . . 12
   
 
    
↾t    
  |
23 | | simplrl 770 |
. . . . . . . . . . . 12
   
 
    
↾t       |
24 | | simprl 764 |
. . . . . . . . . . . 12
   
 
    
↾t    
  |
25 | | inopn 19929 |
. . . . . . . . . . . 12
 
     |
26 | 22, 23, 24, 25 | syl3anc 1268 |
. . . . . . . . . . 11
   
 
    
↾t         |
27 | | inss1 3652 |
. . . . . . . . . . . . 13
   |
28 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
29 | 28 | elpw2 4567 |
. . . . . . . . . . . . 13
   
    |
30 | 27, 29 | mpbir 213 |
. . . . . . . . . . . 12
    |
31 | 30 | a1i 11 |
. . . . . . . . . . 11
   
 
    
↾t          |
32 | 26, 31 | elind 3618 |
. . . . . . . . . 10
   
 
    
↾t            |
33 | | simplrr 771 |
. . . . . . . . . . 11
   
 
    
↾t       |
34 | | simprrl 774 |
. . . . . . . . . . 11
   
 
    
↾t       |
35 | 33, 34 | elind 3618 |
. . . . . . . . . 10
   
 
    
↾t         |
36 | | inss2 3653 |
. . . . . . . . . . . . 13
   |
37 | 36 | a1i 11 |
. . . . . . . . . . . 12
   
 
    
↾t      
  |
38 | | restabs 20181 |
. . . . . . . . . . . 12
   
   ↾t  ↾t     ↾t      |
39 | 22, 37, 24, 38 | syl3anc 1268 |
. . . . . . . . . . 11
   
 
    
↾t       ↾t  ↾t     ↾t      |
40 | | elrestr 15327 |
. . . . . . . . . . . . 13
 
    ↾t    |
41 | 22, 24, 23, 40 | syl3anc 1268 |
. . . . . . . . . . . 12
   
 
    
↾t        ↾t    |
42 | | simprrr 775 |
. . . . . . . . . . . . 13
   
 
    
↾t     
↾t    |
43 | | restlly.1 |
. . . . . . . . . . . . . . 15
 

  
↾t    |
44 | 43 | ralrimivva 2809 |
. . . . . . . . . . . . . 14
  

↾t    |
45 | 44 | ad3antrrr 736 |
. . . . . . . . . . . . 13
   
 
    
↾t     


↾t    |
46 | | oveq1 6297 |
. . . . . . . . . . . . . . . 16
  ↾t   ↾t    ↾t  ↾t    |
47 | 46 | eleq1d 2513 |
. . . . . . . . . . . . . . 15
  ↾t    ↾t 
  ↾t 
↾t     |
48 | 47 | raleqbi1dv 2995 |
. . . . . . . . . . . . . 14
  ↾t   
 ↾t 
 
↾t     ↾t 
↾t     |
49 | 48 | rspcv 3146 |
. . . . . . . . . . . . 13
  ↾t      ↾t   
↾t     ↾t 
↾t     |
50 | 42, 45, 49 | sylc 62 |
. . . . . . . . . . . 12
   
 
    
↾t     
 ↾t     ↾t 
↾t    |
51 | | oveq2 6298 |
. . . . . . . . . . . . . 14
    
↾t 
↾t   
↾t 
↾t      |
52 | 51 | eleq1d 2513 |
. . . . . . . . . . . . 13
      ↾t  ↾t 
  ↾t 
↾t       |
53 | 52 | rspcv 3146 |
. . . . . . . . . . . 12
    ↾t    
↾t     ↾t 
↾t    ↾t  ↾t       |
54 | 41, 50, 53 | sylc 62 |
. . . . . . . . . . 11
   
 
    
↾t       ↾t  ↾t      |
55 | 39, 54 | eqeltrrd 2530 |
. . . . . . . . . 10
   
 
    
↾t     
↾t      |
56 | | eleq2 2518 |
. . . . . . . . . . . 12
   
     |
57 | | oveq2 6298 |
. . . . . . . . . . . . 13
    ↾t   ↾t      |
58 | 57 | eleq1d 2513 |
. . . . . . . . . . . 12
    
↾t   ↾t       |
59 | 56, 58 | anbi12d 717 |
. . . . . . . . . . 11
      ↾t  
  
 ↾t 
      |
60 | 59 | rspcev 3150 |
. . . . . . . . . 10
         
 ↾t 
   
       ↾t     |
61 | 32, 35, 55, 60 | syl12anc 1266 |
. . . . . . . . 9
   
 
    
↾t     
      ↾t     |
62 | 61 | rexlimdvaa 2880 |
. . . . . . . 8
    
 
 
 
↾t  
       ↾t      |
63 | 62 | anassrs 654 |
. . . . . . 7
   


  
 
↾t  
       ↾t      |
64 | 63 | ralimdva 2796 |
. . . . . 6
      

 
↾t  

       ↾t      |
65 | 21, 64 | syld 45 |
. . . . 5
      

 
↾t  

       ↾t      |
66 | 65 | ralrimdva 2806 |
. . . 4
 

 

 
↾t  


       ↾t      |
67 | 66 | impr 625 |
. . 3
 
 


 ↾t     


      ↾t     |
68 | | islly 20483 |
. . 3
 Locally



       ↾t      |
69 | 16, 67, 68 | sylanbrc 670 |
. 2
 
 


 ↾t    
Locally   |
70 | 15, 69 | impbida 843 |
1
  Locally
 


 ↾t       |