Step | Hyp | Ref
| Expression |
1 | | elutop 21248 |
. . . 4
 UnifOn 
 unifTop  
 
          |
2 | 1 | simprbda 629 |
. . 3
  UnifOn  unifTop  
  |
3 | | restutop 21252 |
. . 3
  UnifOn    unifTop  ↾t  unifTop  ↾t       |
4 | 2, 3 | syldan 473 |
. 2
  UnifOn  unifTop  
 unifTop 
↾t  unifTop 
↾t       |
5 | | trust 21244 |
. . . . . . . . . . 11
  UnifOn    ↾t 
  UnifOn    |
6 | 2, 5 | syldan 473 |
. . . . . . . . . 10
  UnifOn  unifTop  
 ↾t    UnifOn    |
7 | | elutop 21248 |
. . . . . . . . . 10
  ↾t    UnifOn   unifTop  ↾t 
  
 
 
↾t               |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
  UnifOn  unifTop  
 unifTop  ↾t        
↾t               |
9 | 8 | simprbda 629 |
. . . . . . . 8
   UnifOn  unifTop  
unifTop  ↾t        |
10 | 2 | adantr 467 |
. . . . . . . 8
   UnifOn  unifTop  
unifTop  ↾t        |
11 | 9, 10 | sstrd 3442 |
. . . . . . 7
   UnifOn  unifTop  
unifTop  ↾t        |
12 | | simp-9l 786 |
. . . . . . . . . . . . 13
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
      
UnifOn    |
13 | | simplr 762 |
. . . . . . . . . . . . 13
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
         |
14 | | simp-4r 777 |
. . . . . . . . . . . . 13
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
      
  |
15 | | ustincl 21222 |
. . . . . . . . . . . . 13
  UnifOn 
 
   |
16 | 12, 13, 14, 15 | syl3anc 1268 |
. . . . . . . . . . . 12
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
           |
17 | | inimass 5252 |
. . . . . . . . . . . . 13
       
               |
18 | | ssrin 3657 |
. . . . . . . . . . . . . . . 16
                    
          |
19 | 18 | adantl 468 |
. . . . . . . . . . . . . . 15
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
                    
          |
20 | | simpllr 769 |
. . . . . . . . . . . . . . . . 17
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
      
      |
21 | 20 | imaeq1d 5167 |
. . . . . . . . . . . . . . . 16
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
                         |
22 | 9 | ad5antr 740 |
. . . . . . . . . . . . . . . . . . 19
        UnifOn 
unifTop  
unifTop  ↾t 
     
↾t           


      |
23 | | simp-5r 779 |
. . . . . . . . . . . . . . . . . . 19
        UnifOn 
unifTop  
unifTop  ↾t 
     
↾t           


      |
24 | 22, 23 | sseldd 3433 |
. . . . . . . . . . . . . . . . . 18
        UnifOn 
unifTop  
unifTop  ↾t 
     
↾t           


      |
25 | 24 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
      
  |
26 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . 20
 |
27 | | inimasn 5253 |
. . . . . . . . . . . . . . . . . . . 20
                             |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
                           |
29 | | xpimasn 5282 |
. . . . . . . . . . . . . . . . . . . 20
           |
30 | 29 | ineq2d 3634 |
. . . . . . . . . . . . . . . . . . 19
                       
   |
31 | 28, 30 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . 18
                     |
32 | | incom 3625 |
. . . . . . . . . . . . . . . . . 18
                 |
33 | 31, 32 | syl6eq 2501 |
. . . . . . . . . . . . . . . . 17
                     |
34 | 25, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
                           |
35 | 21, 34 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
                       |
36 | 19, 35 | sseqtr4d 3469 |
. . . . . . . . . . . . . 14
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
                    
        |
37 | | simp-5r 779 |
. . . . . . . . . . . . . 14
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
               |
38 | 36, 37 | sstrd 3442 |
. . . . . . . . . . . . 13
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
                    
  |
39 | 17, 38 | syl5ss 3443 |
. . . . . . . . . . . 12
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
                 |
40 | | imaeq1 5163 |
. . . . . . . . . . . . . 14
                   |
41 | 40 | sseq1d 3459 |
. . . . . . . . . . . . 13
                     |
42 | 41 | rspcev 3150 |
. . . . . . . . . . . 12
             
        |
43 | 16, 39, 42 | syl2anc 667 |
. . . . . . . . . . 11
          UnifOn  unifTop  
unifTop  ↾t       
↾t           


    
       
        |
44 | | simp-4l 776 |
. . . . . . . . . . . . 13
      UnifOn  unifTop  
unifTop  ↾t       
↾t             UnifOn  unifTop     |
45 | 44 | ad2antrr 732 |
. . . . . . . . . . . 12
        UnifOn 
unifTop  
unifTop  ↾t 
     
↾t           


     UnifOn 
unifTop     |
46 | 1 | simplbda 630 |
. . . . . . . . . . . . 13
  UnifOn  unifTop  


        |
47 | 46 | r19.21bi 2757 |
. . . . . . . . . . . 12
   UnifOn  unifTop  
 
        |
48 | 45, 24, 47 | syl2anc 667 |
. . . . . . . . . . 11
        UnifOn 
unifTop  
unifTop  ↾t 
     
↾t           


             |
49 | 43, 48 | r19.29a 2932 |
. . . . . . . . . 10
        UnifOn 
unifTop  
unifTop  ↾t 
     
↾t           


             |
50 | | simplr 762 |
. . . . . . . . . . 11
      UnifOn  unifTop  
unifTop  ↾t       
↾t           
 ↾t      |
51 | | sqxpexg 6596 |
. . . . . . . . . . . . 13
 unifTop 
    |
52 | | elrest 15326 |
. . . . . . . . . . . . 13
  UnifOn       ↾t    
       |
53 | 51, 52 | sylan2 477 |
. . . . . . . . . . . 12
  UnifOn  unifTop  
 
↾t   


      |
54 | 53 | biimpa 487 |
. . . . . . . . . . 11
   UnifOn  unifTop  

↾t     
      |
55 | 44, 50, 54 | syl2anc 667 |
. . . . . . . . . 10
      UnifOn  unifTop  
unifTop  ↾t       
↾t            
      |
56 | 49, 55 | r19.29a 2932 |
. . . . . . . . 9
      UnifOn  unifTop  
unifTop  ↾t       
↾t            
        |
57 | 8 | simplbda 630 |
. . . . . . . . . 10
   UnifOn  unifTop  
unifTop  ↾t      
 
↾t             |
58 | 57 | r19.21bi 2757 |
. . . . . . . . 9
    UnifOn 
unifTop  
unifTop  ↾t 
    
 
↾t             |
59 | 56, 58 | r19.29a 2932 |
. . . . . . . 8
    UnifOn 
unifTop  
unifTop  ↾t 
    

        |
60 | 59 | ralrimiva 2802 |
. . . . . . 7
   UnifOn  unifTop  
unifTop  ↾t      

        |
61 | | elutop 21248 |
. . . . . . . 8
 UnifOn 
 unifTop  
 
          |
62 | 61 | ad2antrr 732 |
. . . . . . 7
   UnifOn  unifTop  
unifTop  ↾t       unifTop               |
63 | 11, 60, 62 | mpbir2and 933 |
. . . . . 6
   UnifOn  unifTop  
unifTop  ↾t      unifTop    |
64 | | df-ss 3418 |
. . . . . . . 8

    |
65 | 9, 64 | sylib 200 |
. . . . . . 7
   UnifOn  unifTop  
unifTop  ↾t      
   |
66 | 65 | eqcomd 2457 |
. . . . . 6
   UnifOn  unifTop  
unifTop  ↾t          |
67 | | ineq1 3627 |
. . . . . . . 8
 
     |
68 | 67 | eqeq2d 2461 |
. . . . . . 7
   
     |
69 | 68 | rspcev 3150 |
. . . . . 6
  unifTop 
    unifTop       |
70 | 63, 66, 69 | syl2anc 667 |
. . . . 5
   UnifOn  unifTop  
unifTop  ↾t       unifTop       |
71 | | fvex 5875 |
. . . . . . 7
unifTop   |
72 | | elrest 15326 |
. . . . . . 7
  unifTop  unifTop  
  unifTop  ↾t 
 unifTop        |
73 | 71, 72 | mpan 676 |
. . . . . 6
 unifTop 
  unifTop  ↾t 
 unifTop        |
74 | 73 | ad2antlr 733 |
. . . . 5
   UnifOn  unifTop  
unifTop  ↾t        unifTop 
↾t 
 unifTop        |
75 | 70, 74 | mpbird 236 |
. . . 4
   UnifOn  unifTop  
unifTop  ↾t       unifTop  ↾t    |
76 | 75 | ex 436 |
. . 3
  UnifOn  unifTop  
 unifTop  ↾t    
 unifTop  ↾t     |
77 | 76 | ssrdv 3438 |
. 2
  UnifOn  unifTop  
unifTop  ↾t 
    unifTop  ↾t    |
78 | 4, 77 | eqssd 3449 |
1
  UnifOn  unifTop  
 unifTop 
↾t  unifTop 
↾t       |