Step | Hyp | Ref
| Expression |
1 | | simp1 1008 |
. . . 4
  PsMet 
   |
2 | | psmetres2 21330 |
. . . . 5
  PsMet       PsMet    |
3 | 2 | 3adant1 1026 |
. . . 4
  PsMet 
  
  PsMet    |
4 | | oveq2 6298 |
. . . . . . . 8
           |
5 | 4 | imaeq2d 5168 |
. . . . . . 7
    
                        |
6 | 5 | cbvmptv 4495 |
. . . . . 6

                 
            |
7 | 6 | rneqi 5061 |
. . . . 5
               
               |
8 | 7 | metustfbas 21572 |
. . . 4
      PsMet  

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

   
                   |
10 | | fgval 20885 |
. . 3
     
                                          
                   |
11 | 9, 10 | syl 17 |
. 2
  PsMet 
          
             
      
               |
12 | | metuval 21564 |
. . 3
 
   PsMet  metUnif                             |
13 | 3, 12 | syl 17 |
. 2
  PsMet 
 metUnif                             |
14 | | fvex 5875 |
. . . 4
metUnif   |
15 | 3 | elfvexd 5893 |
. . . . 5
  PsMet 
   |
16 | | xpexg 6593 |
. . . . 5
 
     |
17 | 15, 15, 16 | syl2anc 667 |
. . . 4
  PsMet 
     |
18 | | restval 15325 |
. . . 4
  metUnif      metUnif  ↾t     metUnif         |
19 | 14, 17, 18 | sylancr 669 |
. . 3
  PsMet 
  metUnif  ↾t     metUnif         |
20 | | inss2 3653 |
. . . . . . . . . . 11
    
  |
21 | | sseq1 3453 |
. . . . . . . . . . 11
     
 
         |
22 | 20, 21 | mpbiri 237 |
. . . . . . . . . 10
         |
23 | | vex 3048 |
. . . . . . . . . . 11
 |
24 | 23 | elpw 3957 |
. . . . . . . . . 10
   
    |
25 | 22, 24 | sylibr 216 |
. . . . . . . . 9
          |
26 | 25 | rexlimivw 2876 |
. . . . . . . 8
  metUnif        
   |
27 | 26 | adantl 468 |
. . . . . . 7
   PsMet 
  metUnif         
   |
28 | | nfv 1761 |
. . . . . . . . . . . 12
     PsMet 
 metUnif  
      |
29 | | nfmpt1 4492 |
. . . . . . . . . . . . . 14
              |
30 | 29 | nfrn 5077 |
. . . . . . . . . . . . 13
              |
31 | 30 | nfcri 2586 |
. . . . . . . . . . . 12
             |
32 | 28, 31 | nfan 2011 |
. . . . . . . . . . 11
      PsMet 
 metUnif  
    

            |
33 | | nfv 1761 |
. . . . . . . . . . 11

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

             |
35 | | nfmpt1 4492 |
. . . . . . . . . . . . 13
      
           |
36 | 35 | nfrn 5077 |
. . . . . . . . . . . 12
      
           |
37 | | nfcv 2592 |
. . . . . . . . . . . 12
    |
38 | 36, 37 | nfin 3639 |
. . . . . . . . . . 11
  
   
              |
39 | | nfcv 2592 |
. . . . . . . . . . 11
   |
40 | 38, 39 | nfne 2723 |
. . . . . . . . . 10
   
                 |
41 | | simplr 762 |
. . . . . . . . . . . . 13
        PsMet   metUnif  
                 
             |
42 | | ineq1 3627 |
. . . . . . . . . . . . . . 15
          
                  |
43 | 42 | adantl 468 |
. . . . . . . . . . . . . 14
        PsMet   metUnif  
                 
                              |
44 | | simp2 1009 |
. . . . . . . . . . . . . . . 16
  PsMet 
 PsMet    |
45 | | psmetf 21322 |
. . . . . . . . . . . . . . . 16
 PsMet 
        |
46 | | ffun 5731 |
. . . . . . . . . . . . . . . 16
         |
47 | | respreima 6009 |
. . . . . . . . . . . . . . . 16

  
                         |
48 | 44, 45, 46, 47 | 4syl 19 |
. . . . . . . . . . . . . . 15
  PsMet 
   
                         |
49 | 48 | ad6antr 742 |
. . . . . . . . . . . . . 14
        PsMet   metUnif  
                 
                                       |
50 | 43, 49 | eqtr4d 2488 |
. . . . . . . . . . . . 13
        PsMet   metUnif  
                 
                 
            |
51 | | rspe 2845 |
. . . . . . . . . . . . 13
  
                         
           |
52 | 41, 50, 51 | syl2anc 667 |
. . . . . . . . . . . 12
        PsMet   metUnif  
                 
           

                  |
53 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
54 | 53 | inex1 4544 |
. . . . . . . . . . . . 13
     |
55 | | eqid 2451 |
. . . . . . . . . . . . . 14

                 
            |
56 | 55 | elrnmpt 5081 |
. . . . . . . . . . . . 13
          
              

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

                  |
58 | 52, 57 | sylibr 216 |
. . . . . . . . . . 11
        PsMet   metUnif  
                 
               
                |
59 | | simpllr 769 |
. . . . . . . . . . . . 13
        PsMet   metUnif  
                 
             |
60 | | ssinss1 3660 |
. . . . . . . . . . . . 13
 
     |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . 12
        PsMet   metUnif  
                 
                 |
62 | | inss2 3653 |
. . . . . . . . . . . . 13
    
  |
63 | 62 | a1i 11 |
. . . . . . . . . . . 12
        PsMet   metUnif  
                 
                   |
64 | | pweq 3954 |
. . . . . . . . . . . . . . . 16
     
 
     |
65 | 64 | eleq2d 2514 |
. . . . . . . . . . . . . . 15
          
            |
66 | 54 | elpw 3957 |
. . . . . . . . . . . . . . 15
         
    
     |
67 | 65, 66 | syl6bb 265 |
. . . . . . . . . . . . . 14
          
    
      |
68 | | ssin 3654 |
. . . . . . . . . . . . . 14
      
   
 
    
     |
69 | 67, 68 | syl6bbr 267 |
. . . . . . . . . . . . 13
          
 
             |
70 | 69 | ad5antlr 741 |
. . . . . . . . . . . 12
        PsMet   metUnif  
                 
                                |
71 | 61, 63, 70 | mpbir2and 933 |
. . . . . . . . . . 11
        PsMet   metUnif  
                 
                  |
72 | | inelcm 3819 |
. . . . . . . . . . 11
      
                         
              |
73 | 58, 71, 72 | syl2anc 667 |
. . . . . . . . . 10
        PsMet   metUnif  
                 
           
   
               |
74 | | simplr 762 |
. . . . . . . . . . 11
      PsMet 
 metUnif  
    

                         |
75 | | eqid 2451 |
. . . . . . . . . . . . 13

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

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

                 
              |
80 | | ssn0 3767 |
. . . . . . . . . . . . . 14
 
   |
81 | 80 | ancoms 455 |
. . . . . . . . . . . . 13
     |
82 | 81 | 3adant2 1027 |
. . . . . . . . . . . 12
  PsMet 
   |
83 | | metuel 21579 |
. . . . . . . . . . . 12
  PsMet  
 metUnif  
  

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

               |
85 | 84 | simplbda 630 |
. . . . . . . . . 10
   PsMet 
 metUnif   
              |
86 | 85 | adantr 467 |
. . . . . . . . 9
    PsMet   metUnif  
    
               |
87 | 79, 86 | r19.29a 2932 |
. . . . . . . 8
    PsMet   metUnif  
    
     
              |
88 | 87 | r19.29an 2931 |
. . . . . . 7
   PsMet 
  metUnif                            |
89 | 27, 88 | jca 535 |
. . . . . 6
   PsMet 
  metUnif                 
               |
90 | | simprl 764 |
. . . . . . . . . . 11
   PsMet 
          
               
   |
91 | 90 | elpwid 3961 |
. . . . . . . . . 10
   PsMet 
          
                  |
92 | | simpl3 1013 |
. . . . . . . . . . 11
   PsMet 
          
                |
93 | | xpss12 4940 |
. . . . . . . . . . 11
 
  
    |
94 | 92, 92, 93 | syl2anc 667 |
. . . . . . . . . 10
   PsMet 
          
                    |
95 | 91, 94 | sstrd 3442 |
. . . . . . . . 9
   PsMet 
          
                  |
96 | | difssd 3561 |
. . . . . . . . 9
   PsMet 
          
                        |
97 | 95, 96 | unssd 3610 |
. . . . . . . 8
   PsMet 
          
                     
    |
98 | | simplr 762 |
. . . . . . . . . . . 12
      PsMet 
          
                   
             |
99 | | eqidd 2452 |
. . . . . . . . . . . 12
      PsMet 
          
                   
                               |
100 | 4 | imaeq2d 5168 |
. . . . . . . . . . . . . 14
                     |
101 | 100 | eqeq2d 2461 |
. . . . . . . . . . . . 13
                                         |
102 | 101 | rspcev 3150 |
. . . . . . . . . . . 12
                     
                    |
103 | 98, 99, 102 | syl2anc 667 |
. . . . . . . . . . 11
      PsMet 
          
                   
           
                    |
104 | 44 | ad4antr 738 |
. . . . . . . . . . . 12
      PsMet 
          
                   
          
PsMet    |
105 | | cnvexg 6739 |
. . . . . . . . . . . 12
 PsMet 
   |
106 | | imaexg 6730 |
. . . . . . . . . . . 12
             |
107 | 75 | elrnmpt 5081 |
. . . . . . . . . . . 12
                                                     |
108 | 104, 105,
106, 107 | 4syl 19 |
. . . . . . . . . . 11
      PsMet 
          
                   
                                                      |
109 | 103, 108 | mpbird 236 |
. . . . . . . . . 10
      PsMet 
          
                   
                                 |
110 | | cnvimass 5188 |
. . . . . . . . . . . . . . . 16
        
 |
111 | | fdm 5733 |
. . . . . . . . . . . . . . . . 17
           |
112 | 45, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
 PsMet 
    |
113 | 110, 112 | syl5sseq 3480 |
. . . . . . . . . . . . . . 15
 PsMet 
         
   |
114 | 104, 113 | syl 17 |
. . . . . . . . . . . . . 14
      PsMet 
          
                   
                        |
115 | | ssdif0 3823 |
. . . . . . . . . . . . . 14
           
               |
116 | 114, 115 | sylib 200 |
. . . . . . . . . . . . 13
      PsMet 
          
                   
                          |
117 | | 0ss 3763 |
. . . . . . . . . . . . 13
 |
118 | 116, 117 | syl6eqss 3482 |
. . . . . . . . . . . 12
      PsMet 
          
                   
                          |
119 | | respreima 6009 |
. . . . . . . . . . . . . 14

  
                         |
120 | 104, 45, 46, 119 | 4syl 19 |
. . . . . . . . . . . . 13
      PsMet 
          
                   
                                       |
121 | | simpr 463 |
. . . . . . . . . . . . . 14
      PsMet 
          
                   
                          |
122 | | simpllr 769 |
. . . . . . . . . . . . . . 15
      PsMet 
          
                   
              |
123 | 122 | elpwid 3961 |
. . . . . . . . . . . . . 14
      PsMet 
          
                   
          
  |
124 | 121, 123 | eqsstr3d 3467 |
. . . . . . . . . . . . 13
      PsMet 
          
                   
                       
  |
125 | 120, 124 | eqsstr3d 3467 |
. . . . . . . . . . . 12
      PsMet 
          
                   
                          |
126 | 118, 125 | unssd 3610 |
. . . . . . . . . . 11
      PsMet 
          
                   
                                      
  |
127 | | ssundif 3851 |
. . . . . . . . . . . 12
                                     |
128 | | difcom 3852 |
. . . . . . . . . . . 12
           
     
                   |
129 | | difdif2 3700 |
. . . . . . . . . . . . 13
                                              |
130 | 129 | sseq1i 3456 |
. . . . . . . . . . . 12
             
   
                              |
131 | 127, 128,
130 | 3bitri 275 |
. . . . . . . . . . 11
                                             
  |
132 | 126, 131 | sylibr 216 |
. . . . . . . . . 10
      PsMet 
          
                   
                              |
133 | | sseq1 3453 |
. . . . . . . . . . 11
          
                            |
134 | 133 | rspcev 3150 |
. . . . . . . . . 10
                                                               |
135 | 109, 132,
134 | syl2anc 667 |
. . . . . . . . 9
      PsMet 
          
                   
           
                      |
136 | | elin 3617 |
. . . . . . . . . . . . . 14
                        
              |
137 | | vex 3048 |
. . . . . . . . . . . . . . . 16
 |
138 | 6 | elrnmpt 5081 |
. . . . . . . . . . . . . . . 16
                 
  
             |
139 | 137, 138 | ax-mp 5 |
. . . . . . . . . . . . . . 15
 
              
  
            |
140 | 139 | anbi1i 701 |
. . . . . . . . . . . . . 14
                  
 
                 |
141 | | ancom 452 |
. . . . . . . . . . . . . 14
  
  
         
    
                |
142 | 136, 140,
141 | 3bitri 275 |
. . . . . . . . . . . . 13
                     
   
            |
143 | 142 | exbii 1718 |
. . . . . . . . . . . 12
      
            
    
   
            |
144 | | n0 3741 |
. . . . . . . . . . . 12
     
               
                  |
145 | | df-rex 2743 |
. . . . . . . . . . . 12
   
  
         
    
   
            |
146 | 143, 144,
145 | 3bitr4i 281 |
. . . . . . . . . . 11
     
               
  
            |
147 | 146 | biimpi 198 |
. . . . . . . . . 10
     
               
  
            |
148 | 147 | ad2antll 735 |
. . . . . . . . 9
   PsMet 
          
                
  
            |
149 | 135, 148 | r19.29vva 2934 |
. . . . . . . 8
   PsMet 
          
                                     |
150 | 82 | adantr 467 |
. . . . . . . . 9
   PsMet 
          
                |
151 | 44 | adantr 467 |
. . . . . . . . 9
   PsMet 
          
              PsMet    |
152 | | metuel 21579 |
. . . . . . . . 9
  PsMet  
         metUnif           

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

                       |
154 | 97, 149, 153 | mpbir2and 933 |
. . . . . . 7
   PsMet 
          
                      metUnif    |
155 | | indir 3691 |
. . . . . . . . 9
                             |
156 | | incom 3625 |
. . . . . . . . . . 11
                     |
157 | | disjdif 3839 |
. . . . . . . . . . 11
           |
158 | 156, 157 | eqtr3i 2475 |
. . . . . . . . . 10
   
       |
159 | 158 | uneq2i 3585 |
. . . . . . . . 9
                       |
160 | | un0 3759 |
. . . . . . . . 9
           |
161 | 155, 159,
160 | 3eqtri 2477 |
. . . . . . . 8
                 |
162 | | df-ss 3418 |
. . . . . . . . 9
  
      |
163 | 91, 162 | sylib 200 |
. . . . . . . 8
   PsMet 
          
                    |
164 | 161, 163 | syl5req 2498 |
. . . . . . 7
   PsMet 
          
                  
         |
165 | | ineq1 3627 |
. . . . . . . . 9
        
        
         |
166 | 165 | eqeq2d 2461 |
. . . . . . . 8
        
    
               |
167 | 166 | rspcev 3150 |
. . . . . . 7
     
    metUnif 
            
 metUnif         |
168 | 154, 164,
167 | syl2anc 667 |
. . . . . 6
   PsMet 
          
               metUnif         |
169 | 89, 168 | impbida 843 |
. . . . 5
  PsMet 
   metUnif      
         
                |
170 | | eqid 2451 |
. . . . . . 7
 metUnif        metUnif        |
171 | 170 | elrnmpt 5081 |
. . . . . 6
   metUnif      
 metUnif          |
172 | 23, 171 | ax-mp 5 |
. . . . 5
  metUnif      
 metUnif         |
173 | | pweq 3954 |
. . . . . . . 8
 
   |
174 | 173 | ineq2d 3634 |
. . . . . . 7
      
                
               |
175 | 174 | neeq1d 2683 |
. . . . . 6
  
   
              
                   |
176 | 175 | elrab 3196 |
. . . . 5
         
                       
               |
177 | 169, 172,
176 | 3bitr4g 292 |
. . . 4
  PsMet 
   metUnif      
     
                    |
178 | 177 | eqrdv 2449 |
. . 3
  PsMet 

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