Step | Hyp | Ref
| Expression |
1 | | simpr 467 |
. . . . 5
         |
2 | | dfss1 3649 |
. . . . 5

    |
3 | 1, 2 | sylib 201 |
. . . 4
           |
4 | | simpl 463 |
. . . . 5
             |
5 | | id 22 |
. . . . . 6
   |
6 | | filtop 20925 |
. . . . . 6
    
  |
7 | | ssexg 4565 |
. . . . . 6
 
   |
8 | 5, 6, 7 | syl2anr 485 |
. . . . 5
         |
9 | 6 | adantr 471 |
. . . . 5
         |
10 | | elrestr 15382 |
. . . . 5
         
↾t    |
11 | 4, 8, 9, 10 | syl3anc 1276 |
. . . 4
         
↾t    |
12 | 3, 11 | eqeltrrd 2541 |
. . 3
       
↾t    |
13 | | elpwi 3972 |
. . . . 5
    |
14 | | vex 3060 |
. . . . . . . . . 10
 |
15 | 14 | inex1 4560 |
. . . . . . . . 9
   |
16 | 15 | a1i 11 |
. . . . . . . 8
       


 
   |
17 | | elrest 15381 |
. . . . . . . . . 10
         ↾t  
     |
18 | 8, 17 | syldan 477 |
. . . . . . . . 9
         ↾t  
     |
19 | 18 | adantr 471 |
. . . . . . . 8
       

 
↾t 


    |
20 | | simpr 467 |
. . . . . . . . 9
       



 

   |
21 | 20 | sseq1d 3471 |
. . . . . . . 8
       



 
      |
22 | 16, 19, 21 | rexxfr2d 4634 |
. . . . . . 7
       

 
 ↾t         |
23 | | indir 3703 |
. . . . . . . . . 10
       
   |
24 | | simplr 767 |
. . . . . . . . . . . . 13
       




     |
25 | | df-ss 3430 |
. . . . . . . . . . . . 13

    |
26 | 24, 25 | sylib 201 |
. . . . . . . . . . . 12
       




       |
27 | 26 | uneq2d 3600 |
. . . . . . . . . . 11
       




      
        |
28 | | simprr 771 |
. . . . . . . . . . . 12
       




    
  |
29 | | ssequn1 3616 |
. . . . . . . . . . . 12
  
 
    |
30 | 28, 29 | sylib 201 |
. . . . . . . . . . 11
       




         |
31 | 27, 30 | eqtrd 2496 |
. . . . . . . . . 10
       




      
    |
32 | 23, 31 | syl5eq 2508 |
. . . . . . . . 9
       




         |
33 | | simplll 773 |
. . . . . . . . . 10
       




  
      |
34 | | simpllr 774 |
. . . . . . . . . . 11
       




     |
35 | 33, 34, 8 | syl2anc 671 |
. . . . . . . . . 10
       




  
  |
36 | | simprl 769 |
. . . . . . . . . . 11
       




  
  |
37 | | filelss 20922 |
. . . . . . . . . . . . 13
         |
38 | 33, 36, 37 | syl2anc 671 |
. . . . . . . . . . . 12
       




     |
39 | 24, 34 | sstrd 3454 |
. . . . . . . . . . . 12
       




     |
40 | 38, 39 | unssd 3622 |
. . . . . . . . . . 11
       




    
  |
41 | | ssun1 3609 |
. . . . . . . . . . . 12

  |
42 | 41 | a1i 11 |
. . . . . . . . . . 11
       




       |
43 | | filss 20923 |
. . . . . . . . . . 11
       

        |
44 | 33, 36, 40, 42, 43 | syl13anc 1278 |
. . . . . . . . . 10
       




       |
45 | | elrestr 15382 |
. . . . . . . . . 10
           
 
↾t    |
46 | 33, 35, 44, 45 | syl3anc 1276 |
. . . . . . . . 9
       




        ↾t    |
47 | 32, 46 | eqeltrrd 2541 |
. . . . . . . 8
       




  
 ↾t    |
48 | 47 | rexlimdvaa 2892 |
. . . . . . 7
       

 



↾t     |
49 | 22, 48 | sylbid 223 |
. . . . . 6
       

 
 ↾t    ↾t     |
50 | 49 | ex 440 |
. . . . 5
       
   ↾t    ↾t      |
51 | 13, 50 | syl5 33 |
. . . 4
           
↾t    ↾t      |
52 | 51 | ralrimiv 2812 |
. . 3
            ↾t    ↾t     |
53 | | simpll 765 |
. . . . . 6
       

 
      |
54 | 8 | adantr 471 |
. . . . . 6
       

 
  |
55 | | filin 20924 |
. . . . . . . 8
     
 
   |
56 | 55 | 3expb 1216 |
. . . . . . 7
      
 
    |
57 | 56 | adantlr 726 |
. . . . . 6
       

      |
58 | | elrestr 15382 |
. . . . . 6
           
 
↾t    |
59 | 53, 54, 57, 58 | syl3anc 1276 |
. . . . 5
       

       ↾t    |
60 | 59 | ralrimivva 2821 |
. . . 4
       

 
   ↾t    |
61 | | vex 3060 |
. . . . . . 7
 |
62 | 61 | inex1 4560 |
. . . . . 6
   |
63 | 62 | a1i 11 |
. . . . 5
       
 
   |
64 | | elrest 15381 |
. . . . . 6
         ↾t  
     |
65 | 8, 64 | syldan 477 |
. . . . 5
         ↾t  
     |
66 | 15 | a1i 11 |
. . . . . 6
       

    
   |
67 | 18 | adantr 471 |
. . . . . 6
       
     ↾t  
     |
68 | | ineq12 3641 |
. . . . . . . . 9
   
             |
69 | | inindir 3662 |
. . . . . . . . 9
       
   |
70 | 68, 69 | syl6eqr 2514 |
. . . . . . . 8
   
           |
71 | 70 | adantll 725 |
. . . . . . 7
       

              |
72 | 71 | eleq1d 2524 |
. . . . . 6
       

          ↾t 
 
   ↾t     |
73 | 66, 67, 72 | ralxfr2d 4633 |
. . . . 5
       
    
 ↾t     
↾t 

 
   ↾t     |
74 | 63, 65, 73 | ralxfr2d 4633 |
. . . 4
        
 ↾t    
↾t     
↾t 


 
   ↾t     |
75 | 60, 74 | mpbird 240 |
. . 3
        
↾t    
↾t     
↾t    |
76 | | isfil2 20926 |
. . . . . 6
  ↾t         ↾t 
  ↾t  
↾t       
↾t    ↾t     ↾t    
↾t     
↾t     |
77 | | restsspw 15385 |
. . . . . . . 8
 ↾t 
  |
78 | | 3anass 995 |
. . . . . . . 8
  
↾t    ↾t  
↾t  
  ↾t     ↾t  
↾t      |
79 | 77, 78 | mpbiran 934 |
. . . . . . 7
  
↾t    ↾t  
↾t  
  ↾t   ↾t     |
80 | 79 | 3anbi1i 1205 |
. . . . . 6
    ↾t    ↾t   ↾t       
↾t    ↾t     ↾t    
↾t     
↾t  
   ↾t  
↾t       
↾t    ↾t     ↾t    
↾t     
↾t     |
81 | | 3anass 995 |
. . . . . 6
    ↾t  
↾t       
↾t    ↾t     ↾t    
↾t     
↾t  
   ↾t  
↾t        
↾t    ↾t     ↾t    
↾t     
↾t      |
82 | 76, 80, 81 | 3bitri 279 |
. . . . 5
  ↾t         ↾t  
↾t        
↾t    ↾t     ↾t    
↾t     
↾t      |
83 | | anass 659 |
. . . . 5
    ↾t  
↾t        
↾t    ↾t     ↾t    
↾t     
↾t      ↾t  
 ↾t 
 
   
↾t    ↾t     ↾t    
↾t     
↾t       |
84 | | ancom 456 |
. . . . 5
   ↾t    ↾t        ↾t    ↾t   
 ↾t    
↾t     
↾t        ↾t        ↾t    ↾t   
 ↾t    
↾t     
↾t     ↾t     |
85 | 82, 83, 84 | 3bitri 279 |
. . . 4
  ↾t        
↾t   
   
↾t    ↾t     ↾t    
↾t     
↾t     ↾t     |
86 | 85 | baib 919 |
. . 3
   ↾t   
   
↾t    ↾t     ↾t    
↾t     
↾t      ↾t     
 ↾t     |
87 | 12, 52, 75, 86 | syl12anc 1274 |
. 2
        
↾t       ↾t     |
88 | | nesym 2692 |
. . . 4
  
    |
89 | 88 | ralbii 2831 |
. . 3
 

      |
90 | | elrest 15381 |
. . . . . 6
         ↾t  
     |
91 | 8, 90 | syldan 477 |
. . . . 5
         ↾t  
     |
92 | | dfrex2 2850 |
. . . . 5
   

    |
93 | 91, 92 | syl6bb 269 |
. . . 4
         ↾t        |
94 | 93 | con2bid 335 |
. . 3
        
 
 ↾t     |
95 | 89, 94 | syl5bb 265 |
. 2
        
 
 ↾t     |
96 | 87, 95 | bitr4d 264 |
1
        
↾t      
     |