Step | Hyp | Ref
| Expression |
1 | | simpl 463 |
. . . 4
   UnifOn    unifTop  ↾t    UnifOn     |
2 | | fvex 5857 |
. . . . . . . 8
unifTop   |
3 | 2 | a1i 11 |
. . . . . . 7
  UnifOn   unifTop    |
4 | | elfvex 5874 |
. . . . . . . . 9
 UnifOn 
  |
5 | 4 | adantr 471 |
. . . . . . . 8
  UnifOn     |
6 | | simpr 467 |
. . . . . . . 8
  UnifOn     |
7 | 5, 6 | ssexd 4521 |
. . . . . . 7
  UnifOn     |
8 | | elrest 15336 |
. . . . . . 7
  unifTop     unifTop 
↾t 
 unifTop        |
9 | 3, 7, 8 | syl2anc 671 |
. . . . . 6
  UnifOn     unifTop 
↾t 
 unifTop        |
10 | 9 | biimpa 491 |
. . . . 5
   UnifOn    unifTop  ↾t   
unifTop       |
11 | | inss2 3620 |
. . . . . . 7
   |
12 | | sseq1 3420 |
. . . . . . 7
   
     |
13 | 11, 12 | mpbiri 241 |
. . . . . 6
     |
14 | 13 | rexlimivw 2849 |
. . . . 5
  unifTop       |
15 | 10, 14 | syl 17 |
. . . 4
   UnifOn    unifTop  ↾t  
  |
16 | | simp-5l 783 |
. . . . . . . . . 10
      UnifOn    unifTop  ↾t  

unifTop  
  
UnifOn    |
17 | 16 | ad2antrr 737 |
. . . . . . . . 9
        UnifOn 
  unifTop  ↾t    unifTop  
          
UnifOn    |
18 | 7 | ad6antr 747 |
. . . . . . . . . 10
        UnifOn 
  unifTop  ↾t    unifTop  
          
  |
19 | | xpexg 6580 |
. . . . . . . . . 10
 
     |
20 | 18, 18, 19 | syl2anc 671 |
. . . . . . . . 9
        UnifOn 
  unifTop  ↾t    unifTop  
          
    |
21 | | simplr 767 |
. . . . . . . . 9
        UnifOn 
  unifTop  ↾t    unifTop  
          
  |
22 | | elrestr 15337 |
. . . . . . . . 9
  UnifOn   
 
   
↾t      |
23 | 17, 20, 21, 22 | syl3anc 1271 |
. . . . . . . 8
        UnifOn 
  unifTop  ↾t    unifTop  
          
     ↾t      |
24 | | inss1 3619 |
. . . . . . . . . . . . 13
     |
25 | | imass1 5180 |
. . . . . . . . . . . . 13
              
        |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . 12
         
       |
27 | | sstr 3407 |
. . . . . . . . . . . 12
                                  
  |
28 | 26, 27 | mpan 681 |
. . . . . . . . . . 11
                   |
29 | | imassrn 5156 |
. . . . . . . . . . . . . . 15
         
     |
30 | | rnin 5222 |
. . . . . . . . . . . . . . 15

    
   |
31 | 29, 30 | sstri 3408 |
. . . . . . . . . . . . . 14
         

    |
32 | | inss2 3620 |
. . . . . . . . . . . . . 14
   
   |
33 | 31, 32 | sstri 3408 |
. . . . . . . . . . . . 13
         
   |
34 | | rnxpid 5247 |
. . . . . . . . . . . . 13
   |
35 | 33, 34 | sseqtri 3431 |
. . . . . . . . . . . 12
         
 |
36 | 35 | a1i 11 |
. . . . . . . . . . 11
                   |
37 | 28, 36 | ssind 3623 |
. . . . . . . . . 10
                     |
38 | 37 | adantl 472 |
. . . . . . . . 9
        UnifOn 
  unifTop  ↾t    unifTop  
          
 
            |
39 | | simpllr 774 |
. . . . . . . . 9
        UnifOn 
  unifTop  ↾t    unifTop  
          
    |
40 | 38, 39 | sseqtr4d 3436 |
. . . . . . . 8
        UnifOn 
  unifTop  ↾t    unifTop  
          
 
          |
41 | | imaeq1 5140 |
. . . . . . . . . 10
                       |
42 | 41 | sseq1d 3426 |
. . . . . . . . 9
                         |
43 | 42 | rspcev 3117 |
. . . . . . . 8
       ↾t               
 ↾t 
        
  |
44 | 23, 40, 43 | syl2anc 671 |
. . . . . . 7
        UnifOn 
  unifTop  ↾t    unifTop  
          
 
↾t             |
45 | | simplr 767 |
. . . . . . . 8
      UnifOn    unifTop  ↾t  

unifTop  
   unifTop    |
46 | | inss1 3619 |
. . . . . . . . 9
   |
47 | | simpllr 774 |
. . . . . . . . . 10
      UnifOn    unifTop  ↾t  

unifTop  
  
  |
48 | | simpr 467 |
. . . . . . . . . 10
      UnifOn    unifTop  ↾t  

unifTop  
       |
49 | 47, 48 | eleqtrd 2531 |
. . . . . . . . 9
      UnifOn    unifTop  ↾t  

unifTop  
  
    |
50 | 46, 49 | sseldi 3397 |
. . . . . . . 8
      UnifOn    unifTop  ↾t  

unifTop  
  
  |
51 | | elutop 21258 |
. . . . . . . . . 10
 UnifOn 
 unifTop  
 
          |
52 | 51 | simplbda 634 |
. . . . . . . . 9
  UnifOn  unifTop  


        |
53 | 52 | r19.21bi 2756 |
. . . . . . . 8
   UnifOn  unifTop  
 
        |
54 | 16, 45, 50, 53 | syl21anc 1270 |
. . . . . . 7
      UnifOn    unifTop  ↾t  

unifTop  
   
        |
55 | 44, 54 | r19.29a 2899 |
. . . . . 6
      UnifOn    unifTop  ↾t  

unifTop  
   
 ↾t 
        
  |
56 | 10 | adantr 471 |
. . . . . 6
    UnifOn 
  unifTop  ↾t     unifTop       |
57 | 55, 56 | r19.29a 2899 |
. . . . 5
    UnifOn 
  unifTop  ↾t     
↾t             |
58 | 57 | ralrimiva 2789 |
. . . 4
   UnifOn    unifTop  ↾t   

 ↾t 
        
  |
59 | | trust 21254 |
. . . . . 6
  UnifOn    ↾t 
  UnifOn    |
60 | | elutop 21258 |
. . . . . 6
  ↾t    UnifOn   unifTop  ↾t 
  
 
 
↾t               |
61 | 59, 60 | syl 17 |
. . . . 5
  UnifOn    unifTop  ↾t 
  
 
 
↾t               |
62 | 61 | biimpar 492 |
. . . 4
   UnifOn   
 
 ↾t             unifTop  ↾t 
     |
63 | 1, 15, 58, 62 | syl12anc 1269 |
. . 3
   UnifOn    unifTop  ↾t   unifTop  ↾t 
     |
64 | 63 | ex 440 |
. 2
  UnifOn     unifTop 
↾t  unifTop  ↾t        |
65 | 64 | ssrdv 3405 |
1
  UnifOn    unifTop  ↾t  unifTop  ↾t       |