Step | Hyp | Ref
| Expression |
1 | | simpr 463 |
. . . . . . 7
  UnifOn  unifTop  
unifTop    |
2 | | utopval 21247 |
. . . . . . . . 9
 UnifOn 
unifTop    

         |
3 | | ssrab2 3514 |
. . . . . . . . 9
  

      
  |
4 | 2, 3 | syl6eqss 3482 |
. . . . . . . 8
 UnifOn 
unifTop 
   |
5 | 4 | adantr 467 |
. . . . . . 7
  UnifOn  unifTop  
unifTop 
   |
6 | 1, 5 | sstrd 3442 |
. . . . . 6
  UnifOn  unifTop  
   |
7 | | sspwuni 4367 |
. . . . . 6
 
   |
8 | 6, 7 | sylib 200 |
. . . . 5
  UnifOn  unifTop  
   |
9 | | simp-4l 776 |
. . . . . . . . 9
     UnifOn 
unifTop  
 
  UnifOn    |
10 | | simp-4r 777 |
. . . . . . . . . 10
     UnifOn 
unifTop  
 
  unifTop    |
11 | | simplr 762 |
. . . . . . . . . 10
     UnifOn 
unifTop  
 
    |
12 | 10, 11 | sseldd 3433 |
. . . . . . . . 9
     UnifOn 
unifTop  
 
  unifTop    |
13 | | simpr 463 |
. . . . . . . . 9
     UnifOn 
unifTop  
 
    |
14 | | elutop 21248 |
. . . . . . . . . . . 12
 UnifOn 
 unifTop  
 
          |
15 | 14 | biimpa 487 |
. . . . . . . . . . 11
  UnifOn  unifTop  
 

         |
16 | 15 | simprd 465 |
. . . . . . . . . 10
  UnifOn  unifTop  


        |
17 | 16 | r19.21bi 2757 |
. . . . . . . . 9
   UnifOn  unifTop  
 
        |
18 | 9, 12, 13, 17 | syl21anc 1267 |
. . . . . . . 8
     UnifOn 
unifTop  
 
  
        |
19 | | r19.41v 2942 |
. . . . . . . . 9
           
         |
20 | | ssuni 4220 |
. . . . . . . . . 10
        
         |
21 | 20 | reximi 2855 |
. . . . . . . . 9
         

         |
22 | 19, 21 | sylbir 217 |
. . . . . . . 8
         

         |
23 | 18, 11, 22 | syl2anc 667 |
. . . . . . 7
     UnifOn 
unifTop  
 
  
         |
24 | | eluni2 4202 |
. . . . . . . . 9
 

  |
25 | 24 | biimpi 198 |
. . . . . . . 8
  
  |
26 | 25 | adantl 468 |
. . . . . . 7
   UnifOn  unifTop  
  
  |
27 | 23, 26 | r19.29a 2932 |
. . . . . 6
   UnifOn  unifTop  
  
         |
28 | 27 | ralrimiva 2802 |
. . . . 5
  UnifOn  unifTop  
   
         |
29 | | elutop 21248 |
. . . . . 6
 UnifOn 
 
unifTop       
           |
30 | 29 | adantr 467 |
. . . . 5
  UnifOn  unifTop  
 
unifTop       
           |
31 | 8, 28, 30 | mpbir2and 933 |
. . . 4
  UnifOn  unifTop  
 unifTop    |
32 | 31 | ex 436 |
. . 3
 UnifOn 
 unifTop   unifTop     |
33 | 32 | alrimiv 1773 |
. 2
 UnifOn 
   unifTop   unifTop     |
34 | | elutop 21248 |
. . . . . . . 8
 UnifOn 
 unifTop  
 
          |
35 | 34 | biimpa 487 |
. . . . . . 7
  UnifOn  unifTop  
 

         |
36 | 35 | simpld 461 |
. . . . . 6
  UnifOn  unifTop  
  |
37 | 36 | adantrr 723 |
. . . . 5
  UnifOn   unifTop 
unifTop   
  |
38 | | ssinss1 3660 |
. . . . 5
 
   |
39 | 37, 38 | syl 17 |
. . . 4
  UnifOn   unifTop 
unifTop   
    |
40 | | simpl 459 |
. . . . . . . . . 10
  UnifOn    unifTop  unifTop  



                 UnifOn    |
41 | | simpr31 1098 |
. . . . . . . . . 10
  UnifOn    unifTop  unifTop  



                   |
42 | | simpr32 1099 |
. . . . . . . . . 10
  UnifOn    unifTop  unifTop  



                   |
43 | | ustincl 21222 |
. . . . . . . . . 10
  UnifOn 
 
   |
44 | 40, 41, 42, 43 | syl3anc 1268 |
. . . . . . . . 9
  UnifOn    unifTop  unifTop  



                 
   |
45 | | inss1 3652 |
. . . . . . . . . . . 12
   |
46 | | imass1 5203 |
. . . . . . . . . . . 12
                   |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . 11
       
       |
48 | | simpr33 1100 |
. . . . . . . . . . . 12
  UnifOn    unifTop  unifTop  



                                 |
49 | 48 | simpld 461 |
. . . . . . . . . . 11
  UnifOn    unifTop  unifTop  



                         |
50 | 47, 49 | syl5ss 3443 |
. . . . . . . . . 10
  UnifOn    unifTop  unifTop  



                           |
51 | | inss2 3653 |
. . . . . . . . . . . 12
   |
52 | | imass1 5203 |
. . . . . . . . . . . 12
                   |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . 11
       
       |
54 | 48 | simprd 465 |
. . . . . . . . . . 11
  UnifOn    unifTop  unifTop  



                         |
55 | 53, 54 | syl5ss 3443 |
. . . . . . . . . 10
  UnifOn    unifTop  unifTop  



                           |
56 | 50, 55 | ssind 3656 |
. . . . . . . . 9
  UnifOn    unifTop  unifTop  



                         
   |
57 | | imaeq1 5163 |
. . . . . . . . . . 11
                   |
58 | 57 | sseq1d 3459 |
. . . . . . . . . 10
          
              |
59 | 58 | rspcev 3150 |
. . . . . . . . 9
            
  
          |
60 | 44, 56, 59 | syl2anc 667 |
. . . . . . . 8
  UnifOn    unifTop  unifTop  



                 
          |
61 | 60 | 3anassrs 1232 |
. . . . . . 7
    UnifOn   unifTop  unifTop       
                
      
   |
62 | 61 | 3anassrs 1232 |
. . . . . 6
      UnifOn   unifTop 
unifTop                               
   |
63 | | simpll 760 |
. . . . . . . 8
   UnifOn   unifTop 
unifTop       UnifOn    |
64 | | simplrl 770 |
. . . . . . . 8
   UnifOn   unifTop 
unifTop       unifTop    |
65 | | simpr 463 |
. . . . . . . . . 10
   UnifOn   unifTop 
unifTop           |
66 | | elin 3617 |
. . . . . . . . . 10
  

   |
67 | 65, 66 | sylib 200 |
. . . . . . . . 9
   UnifOn   unifTop 
unifTop       
   |
68 | 67 | simpld 461 |
. . . . . . . 8
   UnifOn   unifTop 
unifTop         |
69 | 35 | simprd 465 |
. . . . . . . . 9
  UnifOn  unifTop  


        |
70 | 69 | r19.21bi 2757 |
. . . . . . . 8
   UnifOn  unifTop  
 
        |
71 | 63, 64, 68, 70 | syl21anc 1267 |
. . . . . . 7
   UnifOn   unifTop 
unifTop       
        |
72 | | simplrr 771 |
. . . . . . . 8
   UnifOn   unifTop 
unifTop       unifTop    |
73 | 67 | simprd 465 |
. . . . . . . 8
   UnifOn   unifTop 
unifTop         |
74 | 63, 72, 73, 17 | syl21anc 1267 |
. . . . . . 7
   UnifOn   unifTop 
unifTop       
        |
75 | | reeanv 2958 |
. . . . . . 7
  
             
 
                |
76 | 71, 74, 75 | sylanbrc 670 |
. . . . . 6
   UnifOn   unifTop 
unifTop       

                |
77 | 62, 76 | r19.29vva 2934 |
. . . . 5
   UnifOn   unifTop 
unifTop       
          |
78 | 77 | ralrimiva 2802 |
. . . 4
  UnifOn   unifTop 
unifTop   
               |
79 | | elutop 21248 |
. . . . 5
 UnifOn 
 
 unifTop    
           
     |
80 | 79 | adantr 467 |
. . . 4
  UnifOn   unifTop 
unifTop   
 
 unifTop    
           
     |
81 | 39, 78, 80 | mpbir2and 933 |
. . 3
  UnifOn   unifTop 
unifTop   
  unifTop    |
82 | 81 | ralrimivva 2809 |
. 2
 UnifOn 
 unifTop   
unifTop     unifTop    |
83 | | fvex 5875 |
. . 3
unifTop   |
84 | | istopg 19925 |
. . 3
 unifTop   unifTop 
    unifTop  
unifTop    unifTop    unifTop     unifTop      |
85 | 83, 84 | ax-mp 5 |
. 2
 unifTop      unifTop  
unifTop    unifTop    unifTop     unifTop     |
86 | 33, 82, 85 | sylanbrc 670 |
1
 UnifOn 
unifTop    |