Step | Hyp | Ref
| Expression |
1 | | metucn.u |
. . . . . 6
metUnif   |
2 | | metucn.c |
. . . . . . 7
 PsMet    |
3 | | metuval 21564 |
. . . . . . 7
 PsMet 
metUnif                     |
4 | 2, 3 | syl 17 |
. . . . . 6
 metUnif                     |
5 | 1, 4 | syl5eq 2497 |
. . . . 5
                    |
6 | | metucn.v |
. . . . . 6
metUnif   |
7 | | metucn.d |
. . . . . . 7
 PsMet    |
8 | | metuval 21564 |
. . . . . . 7
 PsMet 
metUnif                     |
9 | 7, 8 | syl 17 |
. . . . . 6
 metUnif                     |
10 | 6, 9 | syl5eq 2497 |
. . . . 5
                    |
11 | 5, 10 | oveq12d 6308 |
. . . 4
 
Cnu                  
Cnu                    |
12 | 11 | eleq2d 2514 |
. . 3
   Cnu
                 
Cnu                     |
13 | | eqid 2451 |
. . . 4
                                   |
14 | | eqid 2451 |
. . . 4
                                   |
15 | | metucn.x |
. . . . 5
   |
16 | | oveq2 6298 |
. . . . . . . . 9
           |
17 | 16 | imaeq2d 5168 |
. . . . . . . 8
                     |
18 | 17 | cbvmptv 4495 |
. . . . . . 7

          
           |
19 | 18 | rneqi 5061 |
. . . . . 6
                       |
20 | 19 | metust 21573 |
. . . . 5
  PsMet  
                 UnifOn    |
21 | 15, 2, 20 | syl2anc 667 |
. . . 4
                  UnifOn    |
22 | | metucn.y |
. . . . 5
   |
23 | | oveq2 6298 |
. . . . . . . . 9
           |
24 | 23 | imaeq2d 5168 |
. . . . . . . 8
                     |
25 | 24 | cbvmptv 4495 |
. . . . . . 7

          
           |
26 | 25 | rneqi 5061 |
. . . . . 6
                       |
27 | 26 | metust 21573 |
. . . . 5
  PsMet  
                 UnifOn    |
28 | 22, 7, 27 | syl2anc 667 |
. . . 4
                  UnifOn    |
29 | | oveq2 6298 |
. . . . . . . . 9
           |
30 | 29 | imaeq2d 5168 |
. . . . . . . 8
                     |
31 | 30 | cbvmptv 4495 |
. . . . . . 7

          
           |
32 | 31 | rneqi 5061 |
. . . . . 6
                       |
33 | 32 | metustfbas 21572 |
. . . . 5
  PsMet  

                  |
34 | 15, 2, 33 | syl2anc 667 |
. . . 4
                    |
35 | | oveq2 6298 |
. . . . . . . . 9
           |
36 | 35 | imaeq2d 5168 |
. . . . . . . 8
                     |
37 | 36 | cbvmptv 4495 |
. . . . . . 7

          
           |
38 | 37 | rneqi 5061 |
. . . . . 6
                       |
39 | 38 | metustfbas 21572 |
. . . . 5
  PsMet  

                  |
40 | 22, 7, 39 | syl2anc 667 |
. . . 4
                    |
41 | 13, 14, 21, 28, 34, 40 | isucn2 21294 |
. . 3
                   
Cnu                 
     

                        

                  |
42 | 12, 41 | bitrd 257 |
. 2
   Cnu
     

                        

                  |
43 | | eqid 2451 |
. . . . . . . . . 10
                   |
44 | | oveq2 6298 |
. . . . . . . . . . . . 13
           |
45 | 44 | imaeq2d 5168 |
. . . . . . . . . . . 12
                     |
46 | 45 | eqeq2d 2461 |
. . . . . . . . . . 11
                                         |
47 | 46 | rspcev 3150 |
. . . . . . . . . 10
                     
                    |
48 | 43, 47 | mpan2 677 |
. . . . . . . . 9

                     |
49 | 48 | adantl 468 |
. . . . . . . 8
 

                     |
50 | 38 | metustel 21565 |
. . . . . . . . . 10
 PsMet 
          
                                |
51 | 7, 50 | syl 17 |
. . . . . . . . 9
                                            |
52 | 51 | adantr 467 |
. . . . . . . 8
 

          
                                |
53 | 49, 52 | mpbird 236 |
. . . . . . 7
 

                      |
54 | 26 | metustel 21565 |
. . . . . . . 8
 PsMet 
           
             |
55 | 7, 54 | syl 17 |
. . . . . . 7
             
            |
56 | | simpr 463 |
. . . . . . . . . . 11
 
         
           |
57 | 56 | breqd 4413 |
. . . . . . . . . 10
 
         
          
                      |
58 | 57 | imbi2d 318 |
. . . . . . . . 9
 
         
                                         |
59 | 58 | ralbidv 2827 |
. . . . . . . 8
 
         
 
              
                          |
60 | 59 | rexralbidv 2909 |
. . . . . . 7
 
         
 

               
                            
                       |
61 | 53, 55, 60 | ralxfr2d 4616 |
. . . . . 6
                                
                             
                       |
62 | | eqid 2451 |
. . . . . . . . . . 11
                   |
63 | | oveq2 6298 |
. . . . . . . . . . . . . 14
           |
64 | 63 | imaeq2d 5168 |
. . . . . . . . . . . . 13
                     |
65 | 64 | eqeq2d 2461 |
. . . . . . . . . . . 12
                                         |
66 | 65 | rspcev 3150 |
. . . . . . . . . . 11
                     
                    |
67 | 62, 66 | mpan2 677 |
. . . . . . . . . 10

                     |
68 | 67 | adantl 468 |
. . . . . . . . 9
 

                     |
69 | 32 | metustel 21565 |
. . . . . . . . . . 11
 PsMet 
          
                                |
70 | 2, 69 | syl 17 |
. . . . . . . . . 10
                                            |
71 | 70 | adantr 467 |
. . . . . . . . 9
 

          
                                |
72 | 68, 71 | mpbird 236 |
. . . . . . . 8
 

                      |
73 | 19 | metustel 21565 |
. . . . . . . . 9
 PsMet 
           
             |
74 | 2, 73 | syl 17 |
. . . . . . . 8
             
            |
75 | | simpr 463 |
. . . . . . . . . . 11
 
         
           |
76 | 75 | breqd 4413 |
. . . . . . . . . 10
 
         
  
              |
77 | 76 | imbi1d 319 |
. . . . . . . . 9
 
         
                                   
                       |
78 | 77 | 2ralbidv 2832 |
. . . . . . . 8
 
         
 

                       

           
                       |
79 | 72, 74, 78 | rexxfr2d 4617 |
. . . . . . 7
               

                       


                                   |
80 | 79 | ralbidv 2827 |
. . . . . 6
                    
                   
   
           
                       |
81 | 61, 80 | bitrd 257 |
. . . . 5
                                
             

                                   |
82 | 81 | adantr 467 |
. . . 4
 
      
                         

              
              
                       |
83 | 2 | ad4antr 738 |
. . . . . . . . 9
              
PsMet    |
84 | | simplr 762 |
. . . . . . . . 9
                 |
85 | | simprr 766 |
. . . . . . . . 9
                 |
86 | | simprl 764 |
. . . . . . . . 9
              
  |
87 | | elbl4 21578 |
. . . . . . . . . 10
   PsMet   
 
                       |
88 | | rpxr 11309 |
. . . . . . . . . . 11

  |
89 | | elbl3ps 21406 |
. . . . . . . . . . 11
   PsMet   
 
                |
90 | 88, 89 | sylanl2 657 |
. . . . . . . . . 10
   PsMet   
 
                |
91 | 87, 90 | bitr3d 259 |
. . . . . . . . 9
   PsMet   
 
           
       |
92 | 83, 84, 85, 86, 91 | syl22anc 1269 |
. . . . . . . 8
                                  |
93 | 7 | ad4antr 738 |
. . . . . . . . 9
              
PsMet    |
94 | | simpllr 769 |
. . . . . . . . 9
                 |
95 | | simp-4r 777 |
. . . . . . . . . 10
                     |
96 | 95, 85 | ffvelrnd 6023 |
. . . . . . . . 9
                     |
97 | 95, 86 | ffvelrnd 6023 |
. . . . . . . . 9
                     |
98 | | elbl4 21578 |
. . . . . . . . . 10
   PsMet                                                     |
99 | | rpxr 11309 |
. . . . . . . . . . 11

  |
100 | | elbl3ps 21406 |
. . . . . . . . . . 11
   PsMet                                              |
101 | 99, 100 | sylanl2 657 |
. . . . . . . . . 10
   PsMet                                              |
102 | 98, 101 | bitr3d 259 |
. . . . . . . . 9
   PsMet                                                 |
103 | 93, 94, 96, 97, 102 | syl22anc 1269 |
. . . . . . . 8
                                                  |
104 | 92, 103 | imbi12d 322 |
. . . . . . 7
                           
                   
                     |
105 | 104 | 2ralbidva 2830 |
. . . . . 6
            

                                

                     |
106 | 105 | rexbidva 2898 |
. . . . 5
       
    
           
                   
       
                |
107 | 106 | ralbidva 2824 |
. . . 4
 
      
              
                   
   
                     |
108 | 82, 107 | bitrd 257 |
. . 3
 
      
                         

              
       
                |
109 | 108 | pm5.32da 647 |
. 2
                                     
           
     
       
                 |
110 | 42, 109 | bitrd 257 |
1
   Cnu
     
       
                 |