Step | Hyp | Ref
| Expression |
1 | | simp1 1014 |
. . . . 5
  UnifOn  
CauFilu 
 ↾t   
UnifOn    |
2 | | simp2l 1040 |
. . . . 5
  UnifOn  
CauFilu 
 ↾t   
CauFilu    |
3 | | iscfilu 21352 |
. . . . . 6
 UnifOn 
 CauFilu 
    


      |
4 | 3 | biimpa 491 |
. . . . 5
  UnifOn  CauFilu       


     |
5 | 1, 2, 4 | syl2anc 671 |
. . . 4
  UnifOn  
CauFilu 
 ↾t          
 
   |
6 | 5 | simpld 465 |
. . 3
  UnifOn  
CauFilu 
 ↾t   
      |
7 | | simp3 1016 |
. . 3
  UnifOn  
CauFilu 
 ↾t      |
8 | | simp2r 1041 |
. . 3
  UnifOn  
CauFilu 
 ↾t     ↾t    |
9 | | trfbas2 20907 |
. . . 4
        
↾t       ↾t     |
10 | 9 | biimpar 492 |
. . 3
      
  ↾t   
↾t        |
11 | 6, 7, 8, 10 | syl21anc 1275 |
. 2
  UnifOn  
CauFilu 
 ↾t    
↾t        |
12 | 2 | ad5antr 745 |
. . . . . . 7
       UnifOn  
CauFilu 
 ↾t   
 ↾t          
  
 CauFilu    |
13 | 1 | adantr 471 |
. . . . . . . . . 10
   UnifOn  
CauFilu 
 ↾t   
 ↾t    
UnifOn    |
14 | 13 | elfvexd 5916 |
. . . . . . . . 9
   UnifOn  
CauFilu 
 ↾t   
 ↾t    
  |
15 | 7 | adantr 471 |
. . . . . . . . 9
   UnifOn  
CauFilu 
 ↾t   
 ↾t    
  |
16 | 14, 15 | ssexd 4564 |
. . . . . . . 8
   UnifOn  
CauFilu 
 ↾t   
 ↾t    
  |
17 | 16 | ad4antr 743 |
. . . . . . 7
       UnifOn  
CauFilu 
 ↾t   
 ↾t          
  
   |
18 | | simplr 767 |
. . . . . . 7
       UnifOn  
CauFilu 
 ↾t   
 ↾t          
  
   |
19 | | elrestr 15376 |
. . . . . . 7
  CauFilu 

   ↾t    |
20 | 12, 17, 18, 19 | syl3anc 1276 |
. . . . . 6
       UnifOn  
CauFilu 
 ↾t   
 ↾t          
  
    ↾t    |
21 | | inxp 4986 |
. . . . . . 7
         
   |
22 | | simpr 467 |
. . . . . . . . 9
       UnifOn  
CauFilu 
 ↾t   
 ↾t          
  
  
  |
23 | | ssrin 3669 |
. . . . . . . . 9
     
         |
24 | 22, 23 | syl 17 |
. . . . . . . 8
       UnifOn  
CauFilu 
 ↾t   
 ↾t          
  
             |
25 | | simpllr 774 |
. . . . . . . 8
       UnifOn  
CauFilu 
 ↾t   
 ↾t          
  
       |
26 | 24, 25 | sseqtr4d 3481 |
. . . . . . 7
       UnifOn  
CauFilu 
 ↾t   
 ↾t          
  
         |
27 | 21, 26 | syl5eqssr 3489 |
. . . . . 6
       UnifOn  
CauFilu 
 ↾t   
 ↾t          
  
    
 
  |
28 | | id 22 |
. . . . . . . . 9
       |
29 | 28 | sqxpeqd 4879 |
. . . . . . . 8
             |
30 | 29 | sseq1d 3471 |
. . . . . . 7
     
 
       |
31 | 30 | rspcev 3162 |
. . . . . 6
     ↾t          
↾t       |
32 | 20, 27, 31 | syl2anc 671 |
. . . . 5
       UnifOn  
CauFilu 
 ↾t   
 ↾t          
  
   ↾t       |
33 | 5 | simprd 469 |
. . . . . . . 8
  UnifOn  
CauFilu 
 ↾t    

 
  |
34 | 33 | r19.21bi 2769 |
. . . . . . 7
   UnifOn  
CauFilu 
 ↾t   
   
  |
35 | 34 | 3ad2antr2 1180 |
. . . . . 6
   UnifOn  
CauFilu 
 ↾t    
 ↾t 
 
        
  |
36 | 35 | 3anassrs 1240 |
. . . . 5
     UnifOn 
 CauFilu   ↾t    
↾t     
    

    |
37 | 32, 36 | r19.29a 2944 |
. . . 4
     UnifOn 
 CauFilu   ↾t    
↾t     
    
 
↾t       |
38 | | xpexg 6620 |
. . . . . 6
 
     |
39 | 16, 16, 38 | syl2anc 671 |
. . . . 5
   UnifOn  
CauFilu 
 ↾t   
 ↾t    
    |
40 | | simpr 467 |
. . . . 5
   UnifOn  
CauFilu 
 ↾t   
 ↾t    

↾t      |
41 | | elrest 15375 |
. . . . . 6
  UnifOn       ↾t    
       |
42 | 41 | biimpa 491 |
. . . . 5
   UnifOn     
↾t     
      |
43 | 13, 39, 40, 42 | syl21anc 1275 |
. . . 4
   UnifOn  
CauFilu 
 ↾t   
 ↾t    

      |
44 | 37, 43 | r19.29a 2944 |
. . 3
   UnifOn  
CauFilu 
 ↾t   
 ↾t    
 
↾t       |
45 | 44 | ralrimiva 2814 |
. 2
  UnifOn  
CauFilu 
 ↾t    
 ↾t 
    
↾t       |
46 | | trust 21293 |
. . . 4
  UnifOn    ↾t 
  UnifOn    |
47 | 1, 7, 46 | syl2anc 671 |
. . 3
  UnifOn  
CauFilu 
 ↾t    
↾t    UnifOn    |
48 | | iscfilu 21352 |
. . 3
  ↾t    UnifOn   
↾t  CauFilu 
↾t       ↾t     
 
↾t       ↾t         |
49 | 47, 48 | syl 17 |
. 2
  UnifOn  
CauFilu 
 ↾t      ↾t  CauFilu  ↾t       ↾t      
 ↾t       ↾t         |
50 | 11, 45, 49 | mpbir2and 938 |
1
  UnifOn  
CauFilu 
 ↾t    
↾t  CauFilu 
↾t       |