Step | Hyp | Ref
| Expression |
1 | | metuust 21575 |
. . . . . . . . . . . 12
  PsMet  
metUnif  UnifOn    |
2 | | utopval 21247 |
. . . . . . . . . . . 12
 metUnif  UnifOn  unifTop metUnif     

metUnif        
   |
3 | 1, 2 | syl 17 |
. . . . . . . . . . 11
  PsMet  
unifTop metUnif    

 metUnif            |
4 | 3 | eleq2d 2514 |
. . . . . . . . . 10
  PsMet  
 unifTop metUnif  
    metUnif        
    |
5 | | rabid 2967 |
. . . . . . . . . 10
   

metUnif         
  

metUnif            |
6 | 4, 5 | syl6bb 265 |
. . . . . . . . 9
  PsMet  
 unifTop metUnif  
  

metUnif             |
7 | 6 | biimpa 487 |
. . . . . . . 8
   PsMet  
unifTop metUnif        metUnif            |
8 | 7 | simpld 461 |
. . . . . . 7
   PsMet  
unifTop metUnif       |
9 | 8 | elpwid 3961 |
. . . . . 6
   PsMet  
unifTop metUnif   
  |
10 | | unirnblps 21434 |
. . . . . . 7
 PsMet 
       |
11 | 10 | ad2antlr 733 |
. . . . . 6
   PsMet  
unifTop metUnif           |
12 | 9, 11 | sseqtr4d 3469 |
. . . . 5
   PsMet  
unifTop metUnif   
       |
13 | | simpr 463 |
. . . . . . . 8
      PsMet  
unifTop metUnif   

metUnif                  |
14 | | simp-5r 779 |
. . . . . . . . 9
      PsMet  
unifTop metUnif   

metUnif          PsMet    |
15 | | simplr 762 |
. . . . . . . . 9
      PsMet  
unifTop metUnif   

metUnif          metUnif    |
16 | 9 | ad3antrrr 736 |
. . . . . . . . . 10
      PsMet  
unifTop metUnif   

metUnif            |
17 | | simpllr 769 |
. . . . . . . . . 10
      PsMet  
unifTop metUnif   

metUnif            |
18 | 16, 17 | sseldd 3433 |
. . . . . . . . 9
      PsMet  
unifTop metUnif   

metUnif            |
19 | | metustbl 21581 |
. . . . . . . . 9
  PsMet  metUnif 

                |
20 | 14, 15, 18, 19 | syl3anc 1268 |
. . . . . . . 8
      PsMet  
unifTop metUnif   

metUnif                          |
21 | | sstr 3440 |
. . . . . . . . . . 11
 
            
  |
22 | 21 | expcom 437 |
. . . . . . . . . 10
                 |
23 | 22 | anim2d 569 |
. . . . . . . . 9
                     |
24 | 23 | reximdv 2861 |
. . . . . . . 8
                                 |
25 | 13, 20, 24 | sylc 62 |
. . . . . . 7
      PsMet  
unifTop metUnif   

metUnif                    |
26 | 7 | simprd 465 |
. . . . . . . 8
   PsMet  
unifTop metUnif    

metUnif        
  |
27 | 26 | r19.21bi 2757 |
. . . . . . 7
    PsMet  
unifTop metUnif    
 metUnif           |
28 | 25, 27 | r19.29a 2932 |
. . . . . 6
    PsMet  
unifTop metUnif    
          |
29 | 28 | ralrimiva 2802 |
. . . . 5
   PsMet  
unifTop metUnif    

         |
30 | 12, 29 | jca 535 |
. . . 4
   PsMet  
unifTop metUnif                      |
31 | | fvex 5875 |
. . . . . 6
     |
32 | 31 | rnex 6727 |
. . . . 5
     |
33 | | eltg2 19973 |
. . . . 5
             
 
    

           |
34 | 32, 33 | mp1i 13 |
. . . 4
   PsMet  
unifTop metUnif            
 
    

           |
35 | 30, 34 | mpbird 236 |
. . 3
   PsMet  
unifTop metUnif              |
36 | 32, 33 | mp1i 13 |
. . . . . . . . 9
  PsMet  
        
 
    

           |
37 | 36 | biimpa 487 |
. . . . . . . 8
   PsMet  
              

           |
38 | 37 | simpld 461 |
. . . . . . 7
   PsMet  
                |
39 | 10 | ad2antlr 733 |
. . . . . . 7
   PsMet  
                |
40 | 38, 39 | sseqtrd 3468 |
. . . . . 6
   PsMet  
           |
41 | | elpwg 3959 |
. . . . . . 7
        
 
   |
42 | 41 | adantl 468 |
. . . . . 6
   PsMet  
          
   |
43 | 40, 42 | mpbird 236 |
. . . . 5
   PsMet  
            |
44 | | simpllr 769 |
. . . . . . . . 9
    PsMet  
        
 PsMet    |
45 | 40 | sselda 3432 |
. . . . . . . . 9
    PsMet  
        
   |
46 | 37 | simprd 465 |
. . . . . . . . . . 11
   PsMet  
                    |
47 | 46 | r19.21bi 2757 |
. . . . . . . . . 10
    PsMet  
        
           |
48 | | blssexps 21441 |
. . . . . . . . . . 11
  PsMet    
                   |
49 | 44, 45, 48 | syl2anc 667 |
. . . . . . . . . 10
    PsMet  
        
         
            |
50 | 47, 49 | mpbid 214 |
. . . . . . . . 9
    PsMet  
        
            |
51 | | blval2 21577 |
. . . . . . . . . . . . 13
  PsMet 
                          |
52 | 51 | 3expa 1208 |
. . . . . . . . . . . 12
   PsMet                             |
53 | 52 | sseq1d 3459 |
. . . . . . . . . . 11
   PsMet            
              
   |
54 | 53 | rexbidva 2898 |
. . . . . . . . . 10
  PsMet    
                           |
55 | 54 | biimpa 487 |
. . . . . . . . 9
   PsMet   
                        
  |
56 | 44, 45, 50, 55 | syl21anc 1267 |
. . . . . . . 8
    PsMet  
        
                   |
57 | | cnvexg 6739 |
. . . . . . . . . . 11
 PsMet 
   |
58 | | imaexg 6730 |
. . . . . . . . . . 11
             |
59 | 57, 58 | syl 17 |
. . . . . . . . . 10
 PsMet 
           |
60 | 59 | ralrimivw 2803 |
. . . . . . . . 9
 PsMet 
            |
61 | | eqid 2451 |
. . . . . . . . . 10

          
           |
62 | | imaeq1 5163 |
. . . . . . . . . . 11
                                 |
63 | 62 | sseq1d 3459 |
. . . . . . . . . 10
                                   |
64 | 61, 63 | rexrnmpt 6032 |
. . . . . . . . 9
 
          
                 
               
   |
65 | 44, 60, 64 | 3syl 18 |
. . . . . . . 8
    PsMet  
        
                                        |
66 | 56, 65 | mpbird 236 |
. . . . . . 7
    PsMet  
        
                      |
67 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
           |
68 | 67 | imaeq2d 5168 |
. . . . . . . . . . . . . 14
                     |
69 | 68 | cbvmptv 4495 |
. . . . . . . . . . . . 13

          
           |
70 | 69 | rneqi 5061 |
. . . . . . . . . . . 12
                       |
71 | 70 | metustfbas 21572 |
. . . . . . . . . . 11
  PsMet  

                  |
72 | | ssfg 20887 |
. . . . . . . . . . 11
                            
                   |
73 | 71, 72 | syl 17 |
. . . . . . . . . 10
  PsMet  

         
                   |
74 | | metuval 21564 |
. . . . . . . . . . 11
 PsMet 
metUnif                     |
75 | 74 | adantl 468 |
. . . . . . . . . 10
  PsMet  
metUnif                     |
76 | 73, 75 | sseqtr4d 3469 |
. . . . . . . . 9
  PsMet  

         
metUnif    |
77 | | ssrexv 3494 |
. . . . . . . . 9
           
metUnif 
 

                  metUnif            |
78 | 76, 77 | syl 17 |
. . . . . . . 8
  PsMet  
 

                  metUnif            |
79 | 78 | ad2antrr 732 |
. . . . . . 7
    PsMet  
        
                      metUnif        
   |
80 | 66, 79 | mpd 15 |
. . . . . 6
    PsMet  
        
  metUnif        
  |
81 | 80 | ralrimiva 2802 |
. . . . 5
   PsMet  
           metUnif        
  |
82 | 43, 81 | jca 535 |
. . . 4
   PsMet  
           

metUnif            |
83 | 6 | biimpar 488 |
. . . 4
   PsMet  
  

metUnif           unifTop metUnif     |
84 | 82, 83 | syldan 473 |
. . 3
   PsMet  
         unifTop metUnif     |
85 | 35, 84 | impbida 843 |
. 2
  PsMet  
 unifTop metUnif  
           |
86 | 85 | eqrdv 2449 |
1
  PsMet  
unifTop metUnif             |