Step | Hyp | Ref
| Expression |
1 | | ufilfil 20974 |
. . . 4
  ↾t      
↾t        |
2 | | ufilfil 20974 |
. . . . 5
    
      |
3 | | trfil3 20958 |
. . . . 5
        
↾t           |
4 | 2, 3 | sylan 478 |
. . . 4
        
↾t           |
5 | 1, 4 | syl5ib 227 |
. . 3
        
↾t           |
6 | 4 | biimprd 231 |
. . . . 5
          
↾t         |
7 | | elpwi 3972 |
. . . . . . 7
    |
8 | | simpll 765 |
. . . . . . . . 9
      
 
      |
9 | | simpr 467 |
. . . . . . . . . 10
      
 
  |
10 | | simplr 767 |
. . . . . . . . . 10
      
 
  |
11 | 9, 10 | sstrd 3454 |
. . . . . . . . 9
      
 
  |
12 | | ufilss 20975 |
. . . . . . . . 9
        
    |
13 | 8, 11, 12 | syl2anc 671 |
. . . . . . . 8
      
 

     |
14 | | id 22 |
. . . . . . . . . . . . 13
   |
15 | | elfvdm 5918 |
. . . . . . . . . . . . 13
    
  |
16 | | ssexg 4565 |
. . . . . . . . . . . . 13
 
   |
17 | 14, 15, 16 | syl2anr 485 |
. . . . . . . . . . . 12
         |
18 | | elrestr 15382 |
. . . . . . . . . . . . 13
       
 
↾t    |
19 | 18 | 3expia 1217 |
. . . . . . . . . . . 12
           ↾t     |
20 | 17, 19 | syldan 477 |
. . . . . . . . . . 11
           ↾t     |
21 | 20 | adantr 471 |
. . . . . . . . . 10
      
 

  
↾t     |
22 | | df-ss 3430 |
. . . . . . . . . . . 12

    |
23 | 9, 22 | sylib 201 |
. . . . . . . . . . 11
      
 
    |
24 | 23 | eleq1d 2524 |
. . . . . . . . . 10
      
 
 
 
↾t 

↾t     |
25 | 21, 24 | sylibd 222 |
. . . . . . . . 9
      
 


↾t     |
26 | | indif1 3699 |
. . . . . . . . . . . 12
         |
27 | | simplr 767 |
. . . . . . . . . . . . . 14
      
        |
28 | | dfss1 3649 |
. . . . . . . . . . . . . 14

    |
29 | 27, 28 | sylib 201 |
. . . . . . . . . . . . 13
      
          |
30 | 29 | difeq1d 3562 |
. . . . . . . . . . . 12
      
        
     |
31 | 26, 30 | syl5eq 2508 |
. . . . . . . . . . 11
      
        
     |
32 | | simpll 765 |
. . . . . . . . . . . 12
      
            |
33 | 17 | adantr 471 |
. . . . . . . . . . . 12
      
        |
34 | | simprr 771 |
. . . . . . . . . . . 12
      
          |
35 | | elrestr 15382 |
. . . . . . . . . . . 12
           
 
↾t    |
36 | 32, 33, 34, 35 | syl3anc 1276 |
. . . . . . . . . . 11
      
        
 
↾t    |
37 | 31, 36 | eqeltrrd 2541 |
. . . . . . . . . 10
      
        
↾t    |
38 | 37 | expr 624 |
. . . . . . . . 9
      
 
  
   ↾t     |
39 | 25, 38 | orim12d 854 |
. . . . . . . 8
      
 
  
   
↾t    
↾t      |
40 | 13, 39 | mpd 15 |
. . . . . . 7
      
 
 
↾t    
↾t     |
41 | 7, 40 | sylan2 481 |
. . . . . 6
      
     ↾t    
↾t     |
42 | 41 | ralrimiva 2814 |
. . . . 5
           ↾t     ↾t     |
43 | 6, 42 | jctird 551 |
. . . 4
            ↾t     
    ↾t     ↾t       |
44 | | isufil 20973 |
. . . 4
  ↾t       
↾t          ↾t     ↾t      |
45 | 43, 44 | syl6ibr 235 |
. . 3
          
↾t         |
46 | 5, 45 | impbid 195 |
. 2
        
↾t           |
47 | | ufilb 20976 |
. . 3
       
     |
48 | 47 | con1bid 336 |
. 2
         
   |
49 | 46, 48 | bitrd 261 |
1
        
↾t         |