Step | Hyp | Ref
| Expression |
1 | | simp1 1030 |
. . . 4
  PsMet 
   |
2 | | psmetres2 21408 |
. . . . 5
  PsMet       PsMet    |
3 | 2 | 3adant1 1048 |
. . . 4
  PsMet 
  
  PsMet    |
4 | | oveq2 6316 |
. . . . . . . 8
           |
5 | 4 | imaeq2d 5174 |
. . . . . . 7
    
                        |
6 | 5 | cbvmptv 4488 |
. . . . . 6

                 
            |
7 | 6 | rneqi 5067 |
. . . . 5
               
               |
8 | 7 | metustfbas 21650 |
. . . 4
      PsMet  

                      |
9 | 1, 3, 8 | syl2anc 673 |
. . 3
  PsMet 

   
                   |
10 | | fgval 20963 |
. . 3
     
                                          
                   |
11 | 9, 10 | syl 17 |
. 2
  PsMet 
          
             
      
               |
12 | | metuval 21642 |
. . 3
 
   PsMet  metUnif                             |
13 | 3, 12 | syl 17 |
. 2
  PsMet 
 metUnif                             |
14 | | fvex 5889 |
. . . 4
metUnif   |
15 | 3 | elfvexd 5907 |
. . . . 5
  PsMet 
   |
16 | | xpexg 6612 |
. . . . 5
 
     |
17 | 15, 15, 16 | syl2anc 673 |
. . . 4
  PsMet 
     |
18 | | restval 15403 |
. . . 4
  metUnif      metUnif  ↾t     metUnif         |
19 | 14, 17, 18 | sylancr 676 |
. . 3
  PsMet 
  metUnif  ↾t     metUnif         |
20 | | inss2 3644 |
. . . . . . . . . . 11
    
  |
21 | | sseq1 3439 |
. . . . . . . . . . 11
     
 
         |
22 | 20, 21 | mpbiri 241 |
. . . . . . . . . 10
         |
23 | | vex 3034 |
. . . . . . . . . . 11
 |
24 | 23 | elpw 3948 |
. . . . . . . . . 10
   
    |
25 | 22, 24 | sylibr 217 |
. . . . . . . . 9
          |
26 | 25 | rexlimivw 2869 |
. . . . . . . 8
  metUnif        
   |
27 | 26 | adantl 473 |
. . . . . . 7
   PsMet 
  metUnif         
   |
28 | | nfv 1769 |
. . . . . . . . . . . 12
     PsMet 
 metUnif  
      |
29 | | nfmpt1 4485 |
. . . . . . . . . . . . . 14
              |
30 | 29 | nfrn 5083 |
. . . . . . . . . . . . 13
              |
31 | 30 | nfcri 2606 |
. . . . . . . . . . . 12
             |
32 | 28, 31 | nfan 2031 |
. . . . . . . . . . 11
      PsMet 
 metUnif  
    

            |
33 | | nfv 1769 |
. . . . . . . . . . 11

 |
34 | 32, 33 | nfan 2031 |
. . . . . . . . . 10
       PsMet 
 metUnif  
    

             |
35 | | nfmpt1 4485 |
. . . . . . . . . . . . 13
      
           |
36 | 35 | nfrn 5083 |
. . . . . . . . . . . 12
      
           |
37 | | nfcv 2612 |
. . . . . . . . . . . 12
    |
38 | 36, 37 | nfin 3630 |
. . . . . . . . . . 11
  
   
              |
39 | | nfcv 2612 |
. . . . . . . . . . 11
   |
40 | 38, 39 | nfne 2742 |
. . . . . . . . . 10
   
                 |
41 | | simplr 770 |
. . . . . . . . . . . . 13
        PsMet   metUnif  
                 
             |
42 | | ineq1 3618 |
. . . . . . . . . . . . . . 15
          
                  |
43 | 42 | adantl 473 |
. . . . . . . . . . . . . 14
        PsMet   metUnif  
                 
                              |
44 | | simp2 1031 |
. . . . . . . . . . . . . . . 16
  PsMet 
 PsMet    |
45 | | psmetf 21400 |
. . . . . . . . . . . . . . . 16
 PsMet 
        |
46 | | ffun 5742 |
. . . . . . . . . . . . . . . 16
         |
47 | | respreima 6024 |
. . . . . . . . . . . . . . . 16

  
                         |
48 | 44, 45, 46, 47 | 4syl 19 |
. . . . . . . . . . . . . . 15
  PsMet 
   
                         |
49 | 48 | ad6antr 750 |
. . . . . . . . . . . . . 14
        PsMet   metUnif  
                 
                                       |
50 | 43, 49 | eqtr4d 2508 |
. . . . . . . . . . . . 13
        PsMet   metUnif  
                 
                 
            |
51 | | rspe 2844 |
. . . . . . . . . . . . 13
  
                         
           |
52 | 41, 50, 51 | syl2anc 673 |
. . . . . . . . . . . 12
        PsMet   metUnif  
                 
           

                  |
53 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
54 | 53 | inex1 4537 |
. . . . . . . . . . . . 13
     |
55 | | eqid 2471 |
. . . . . . . . . . . . . 14

                 
            |
56 | 55 | elrnmpt 5087 |
. . . . . . . . . . . . 13
          
              

                   |
57 | 54, 56 | ax-mp 5 |
. . . . . . . . . . . 12
     
              

                  |
58 | 52, 57 | sylibr 217 |
. . . . . . . . . . 11
        PsMet   metUnif  
                 
               
                |
59 | | simpllr 777 |
. . . . . . . . . . . . 13
        PsMet   metUnif  
                 
             |
60 | | ssinss1 3651 |
. . . . . . . . . . . . 13
 
     |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . 12
        PsMet   metUnif  
                 
                 |
62 | | inss2 3644 |
. . . . . . . . . . . . 13
    
  |
63 | 62 | a1i 11 |
. . . . . . . . . . . 12
        PsMet   metUnif  
                 
                   |
64 | | pweq 3945 |
. . . . . . . . . . . . . . . 16
     
 
     |
65 | 64 | eleq2d 2534 |
. . . . . . . . . . . . . . 15
          
            |
66 | 54 | elpw 3948 |
. . . . . . . . . . . . . . 15
         
    
     |
67 | 65, 66 | syl6bb 269 |
. . . . . . . . . . . . . 14
          
    
      |
68 | | ssin 3645 |
. . . . . . . . . . . . . 14
      
   
 
    
     |
69 | 67, 68 | syl6bbr 271 |
. . . . . . . . . . . . 13
          
 
             |
70 | 69 | ad5antlr 749 |
. . . . . . . . . . . 12
        PsMet   metUnif  
                 
                                |
71 | 61, 63, 70 | mpbir2and 936 |
. . . . . . . . . . 11
        PsMet   metUnif  
                 
                  |
72 | | inelcm 3823 |
. . . . . . . . . . 11
      
                         
              |
73 | 58, 71, 72 | syl2anc 673 |
. . . . . . . . . 10
        PsMet   metUnif  
                 
           
   
               |
74 | | simplr 770 |
. . . . . . . . . . 11
      PsMet 
 metUnif  
    

                         |
75 | | eqid 2471 |
. . . . . . . . . . . . 13

          
           |
76 | 75 | elrnmpt 5087 |
. . . . . . . . . . . 12
             
            |
77 | 53, 76 | ax-mp 5 |
. . . . . . . . . . 11
 
          
           |
78 | 74, 77 | sylib 201 |
. . . . . . . . . 10
      PsMet 
 metUnif  
    

                        |
79 | 34, 40, 73, 78 | r19.29af2 2915 |
. . . . . . . . 9
      PsMet 
 metUnif  
    

                 
              |
80 | | ssn0 3770 |
. . . . . . . . . . . . . 14
 
   |
81 | 80 | ancoms 460 |
. . . . . . . . . . . . 13
     |
82 | 81 | 3adant2 1049 |
. . . . . . . . . . . 12
  PsMet 
   |
83 | | metuel 21657 |
. . . . . . . . . . . 12
  PsMet  
 metUnif  
  

               |
84 | 82, 44, 83 | syl2anc 673 |
. . . . . . . . . . 11
  PsMet 
  metUnif  
  

               |
85 | 84 | simplbda 636 |
. . . . . . . . . 10
   PsMet 
 metUnif   
              |
86 | 85 | adantr 472 |
. . . . . . . . 9
    PsMet   metUnif  
    
               |
87 | 79, 86 | r19.29a 2918 |
. . . . . . . 8
    PsMet   metUnif  
    
     
              |
88 | 87 | r19.29an 2917 |
. . . . . . 7
   PsMet 
  metUnif                            |
89 | 27, 88 | jca 541 |
. . . . . 6
   PsMet 
  metUnif                 
               |
90 | | simprl 772 |
. . . . . . . . . . 11
   PsMet 
          
               
   |
91 | 90 | elpwid 3952 |
. . . . . . . . . 10
   PsMet 
          
                  |
92 | | simpl3 1035 |
. . . . . . . . . . 11
   PsMet 
          
                |
93 | | xpss12 4945 |
. . . . . . . . . . 11
 
  
    |
94 | 92, 92, 93 | syl2anc 673 |
. . . . . . . . . 10
   PsMet 
          
                    |
95 | 91, 94 | sstrd 3428 |
. . . . . . . . 9
   PsMet 
          
                  |
96 | | difssd 3550 |
. . . . . . . . 9
   PsMet 
          
                        |
97 | 95, 96 | unssd 3601 |
. . . . . . . 8
   PsMet 
          
                     
    |
98 | | simplr 770 |
. . . . . . . . . . . 12
      PsMet 
          
                   
             |
99 | | eqidd 2472 |
. . . . . . . . . . . 12
      PsMet 
          
                   
                               |
100 | 4 | imaeq2d 5174 |
. . . . . . . . . . . . . 14
                     |
101 | 100 | eqeq2d 2481 |
. . . . . . . . . . . . 13
                                         |
102 | 101 | rspcev 3136 |
. . . . . . . . . . . 12
                     
                    |
103 | 98, 99, 102 | syl2anc 673 |
. . . . . . . . . . 11
      PsMet 
          
                   
           
                    |
104 | 44 | ad4antr 746 |
. . . . . . . . . . . 12
      PsMet 
          
                   
          
PsMet    |
105 | | cnvexg 6758 |
. . . . . . . . . . . 12
 PsMet 
   |
106 | | imaexg 6749 |
. . . . . . . . . . . 12
             |
107 | 75 | elrnmpt 5087 |
. . . . . . . . . . . 12
                                                     |
108 | 104, 105,
106, 107 | 4syl 19 |
. . . . . . . . . . 11
      PsMet 
          
                   
                                                      |
109 | 103, 108 | mpbird 240 |
. . . . . . . . . 10
      PsMet 
          
                   
                                 |
110 | | cnvimass 5194 |
. . . . . . . . . . . . . . . 16
        
 |
111 | | fdm 5745 |
. . . . . . . . . . . . . . . . 17
           |
112 | 45, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
 PsMet 
    |
113 | 110, 112 | syl5sseq 3466 |
. . . . . . . . . . . . . . 15
 PsMet 
         
   |
114 | 104, 113 | syl 17 |
. . . . . . . . . . . . . 14
      PsMet 
          
                   
                        |
115 | | ssdif0 3741 |
. . . . . . . . . . . . . 14
           
               |
116 | 114, 115 | sylib 201 |
. . . . . . . . . . . . 13
      PsMet 
          
                   
                          |
117 | | 0ss 3766 |
. . . . . . . . . . . . 13
 |
118 | 116, 117 | syl6eqss 3468 |
. . . . . . . . . . . 12
      PsMet 
          
                   
                          |
119 | | respreima 6024 |
. . . . . . . . . . . . . 14

  
                         |
120 | 104, 45, 46, 119 | 4syl 19 |
. . . . . . . . . . . . 13
      PsMet 
          
                   
                                       |
121 | | simpr 468 |
. . . . . . . . . . . . . 14
      PsMet 
          
                   
                          |
122 | | simpllr 777 |
. . . . . . . . . . . . . . 15
      PsMet 
          
                   
              |
123 | 122 | elpwid 3952 |
. . . . . . . . . . . . . 14
      PsMet 
          
                   
          
  |
124 | 121, 123 | eqsstr3d 3453 |
. . . . . . . . . . . . 13
      PsMet 
          
                   
                       
  |
125 | 120, 124 | eqsstr3d 3453 |
. . . . . . . . . . . 12
      PsMet 
          
                   
                          |
126 | 118, 125 | unssd 3601 |
. . . . . . . . . . 11
      PsMet 
          
                   
                                      
  |
127 | | ssundif 3842 |
. . . . . . . . . . . 12
                                     |
128 | | difcom 3843 |
. . . . . . . . . . . 12
           
     
                   |
129 | | difdif2 3691 |
. . . . . . . . . . . . 13
                                              |
130 | 129 | sseq1i 3442 |
. . . . . . . . . . . 12
             
   
                              |
131 | 127, 128,
130 | 3bitri 279 |
. . . . . . . . . . 11
                                             
  |
132 | 126, 131 | sylibr 217 |
. . . . . . . . . 10
      PsMet 
          
                   
                              |
133 | | sseq1 3439 |
. . . . . . . . . . 11
          
                            |
134 | 133 | rspcev 3136 |
. . . . . . . . . 10
                                                               |
135 | 109, 132,
134 | syl2anc 673 |
. . . . . . . . 9
      PsMet 
          
                   
           
                      |
136 | | elin 3608 |
. . . . . . . . . . . . . 14
                        
              |
137 | | vex 3034 |
. . . . . . . . . . . . . . . 16
 |
138 | 6 | elrnmpt 5087 |
. . . . . . . . . . . . . . . 16
                 
  
             |
139 | 137, 138 | ax-mp 5 |
. . . . . . . . . . . . . . 15
 
              
  
            |
140 | 139 | anbi1i 709 |
. . . . . . . . . . . . . 14
                  
 
                 |
141 | | ancom 457 |
. . . . . . . . . . . . . 14
  
  
         
    
                |
142 | 136, 140,
141 | 3bitri 279 |
. . . . . . . . . . . . 13
                     
   
            |
143 | 142 | exbii 1726 |
. . . . . . . . . . . 12
      
            
    
   
            |
144 | | n0 3732 |
. . . . . . . . . . . 12
     
               
                  |
145 | | df-rex 2762 |
. . . . . . . . . . . 12
   
  
         
    
   
            |
146 | 143, 144,
145 | 3bitr4i 285 |
. . . . . . . . . . 11
     
               
  
            |
147 | 146 | biimpi 199 |
. . . . . . . . . 10
     
               
  
            |
148 | 147 | ad2antll 743 |
. . . . . . . . 9
   PsMet 
          
                
  
            |
149 | 135, 148 | r19.29vva 2920 |
. . . . . . . 8
   PsMet 
          
                                     |
150 | 82 | adantr 472 |
. . . . . . . . 9
   PsMet 
          
                |
151 | 44 | adantr 472 |
. . . . . . . . 9
   PsMet 
          
              PsMet    |
152 | | metuel 21657 |
. . . . . . . . 9
  PsMet  
         metUnif           

                         |
153 | 150, 151,
152 | syl2anc 673 |
. . . . . . . 8
   PsMet 
          
                       metUnif      
      

                       |
154 | 97, 149, 153 | mpbir2and 936 |
. . . . . . 7
   PsMet 
          
                      metUnif    |
155 | | indir 3682 |
. . . . . . . . 9
                             |
156 | | incom 3616 |
. . . . . . . . . . 11
                     |
157 | | disjdif 3830 |
. . . . . . . . . . 11
           |
158 | 156, 157 | eqtr3i 2495 |
. . . . . . . . . 10
   
       |
159 | 158 | uneq2i 3576 |
. . . . . . . . 9
                       |
160 | | un0 3762 |
. . . . . . . . 9
           |
161 | 155, 159,
160 | 3eqtri 2497 |
. . . . . . . 8
                 |
162 | | df-ss 3404 |
. . . . . . . . 9
  
      |
163 | 91, 162 | sylib 201 |
. . . . . . . 8
   PsMet 
          
                    |
164 | 161, 163 | syl5req 2518 |
. . . . . . 7
   PsMet 
          
                  
         |
165 | | ineq1 3618 |
. . . . . . . . 9
        
        
         |
166 | 165 | eqeq2d 2481 |
. . . . . . . 8
        
    
               |
167 | 166 | rspcev 3136 |
. . . . . . 7
     
    metUnif 
            
 metUnif         |
168 | 154, 164,
167 | syl2anc 673 |
. . . . . 6
   PsMet 
          
               metUnif         |
169 | 89, 168 | impbida 850 |
. . . . 5
  PsMet 
   metUnif      
         
                |
170 | | eqid 2471 |
. . . . . . 7
 metUnif        metUnif        |
171 | 170 | elrnmpt 5087 |
. . . . . 6
   metUnif      
 metUnif          |
172 | 23, 171 | ax-mp 5 |
. . . . 5
  metUnif      
 metUnif         |
173 | | pweq 3945 |
. . . . . . . 8
 
   |
174 | 173 | ineq2d 3625 |
. . . . . . 7
      
                
               |
175 | 174 | neeq1d 2702 |
. . . . . 6
  
   
              
                   |
176 | 175 | elrab 3184 |
. . . . 5
         
                       
               |
177 | 169, 172,
176 | 3bitr4g 296 |
. . . 4
  PsMet 
   metUnif      
     
                    |
178 | 177 | eqrdv 2469 |
. . 3
  PsMet 

 metUnif            
                   |
179 | 19, 178 | eqtrd 2505 |
. 2
  PsMet 
  metUnif  ↾t         
                   |
180 | 11, 13, 179 | 3eqtr4rd 2516 |
1
  PsMet 
  metUnif  ↾t    metUnif        |