Step | Hyp | Ref
| Expression |
1 | | inss1 3243 |
. . . . . . . . . 10
   |
2 | | metrest.3 |
. . . . . . . . . . . . 13
     |
3 | 2 | elmopn2 12377 |
. . . . . . . . . . . 12
      
 
             |
4 | 3 | simplbda 379 |
. . . . . . . . . . 11
       

           |
5 | 4 | adantlr 464 |
. . . . . . . . . 10
       

 
           |
6 | | ssralv 3108 |
. . . . . . . . . 10
    

                        |
7 | 1, 5, 6 | mpsyl 65 |
. . . . . . . . 9
       

                |
8 | | ssrin 3248 |
. . . . . . . . . . 11
                   
   |
9 | 8 | reximi 2488 |
. . . . . . . . . 10
                    
    |
10 | 9 | ralimi 2454 |
. . . . . . . . 9
 
                          
    |
11 | 7, 10 | syl 14 |
. . . . . . . 8
       

               
    |
12 | | inss2 3244 |
. . . . . . . 8
   |
13 | 11, 12 | jctil 308 |
. . . . . . 7
       

   
               
    |
14 | | sseq1 3070 |
. . . . . . . 8
   
     |
15 | | sseq2 3071 |
. . . . . . . . . 10
             
          
    |
16 | 15 | rexbidv 2397 |
. . . . . . . . 9
    
                    
     |
17 | 16 | raleqbi1dv 2592 |
. . . . . . . 8
    

                        
     |
18 | 14, 17 | anbi12d 460 |
. . . . . . 7
      
          
 
               
      |
19 | 13, 18 | syl5ibrcom 156 |
. . . . . 6
       

      
              |
20 | 19 | rexlimdva 2508 |
. . . . 5
       
 
  
 
              |
21 | 2 | mopntop 12372 |
. . . . . . . . 9
        |
22 | 21 | ad2antrr 475 |
. . . . . . . 8
       

 
               |
23 | | ssel2 3042 |
. . . . . . . . . . . . . 14
 
   |
24 | | ssel2 3042 |
. . . . . . . . . . . . . . . 16
 
   |
25 | | rpxr 9298 |
. . . . . . . . . . . . . . . . . 18

  |
26 | 2 | blopn 12418 |
. . . . . . . . . . . . . . . . . . . 20
      
           |
27 | | eleq1a 2171 |
. . . . . . . . . . . . . . . . . . . 20
        
            |
28 | 26, 27 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
      
             |
29 | 28 | 3expa 1149 |
. . . . . . . . . . . . . . . . . 18
       
              |
30 | 25, 29 | sylan2 282 |
. . . . . . . . . . . . . . . . 17
       
              |
31 | 30 | rexlimdva 2508 |
. . . . . . . . . . . . . . . 16
       
 
           |
32 | 24, 31 | sylan2 282 |
. . . . . . . . . . . . . . 15
           
           |
33 | 32 | anassrs 395 |
. . . . . . . . . . . . . 14
       

  
           |
34 | 23, 33 | sylan2 282 |
. . . . . . . . . . . . 13
       

    
           |
35 | 34 | anassrs 395 |
. . . . . . . . . . . 12
             
           |
36 | 35 | rexlimdva 2508 |
. . . . . . . . . . 11
       


 

           |
37 | 36 | adantrd 275 |
. . . . . . . . . 10
       


  

        
     |
38 | 37 | adantrr 466 |
. . . . . . . . 9
       

 
                
         
    |
39 | 38 | abssdv 3118 |
. . . . . . . 8
       

 
               
          
    |
40 | | uniopn 11950 |
. . . . . . . 8
     
            
   
          
 
  |
41 | 22, 39, 40 | syl2anc 406 |
. . . . . . 7
       

 
                 
              |
42 | | oveq1 5713 |
. . . . . . . . . . . . . . . . . 18
                   |
43 | 42 | ineq1d 3223 |
. . . . . . . . . . . . . . . . 17
                       |
44 | 43 | sseq1d 3076 |
. . . . . . . . . . . . . . . 16
           
             |
45 | 44 | rexbidv 2397 |
. . . . . . . . . . . . . . 15
  
                    
   |
46 | 45 | rspccv 2741 |
. . . . . . . . . . . . . 14
 

                     
   |
47 | 46 | ad2antll 478 |
. . . . . . . . . . . . 13
       

 
              
             |
48 | | ssel 3041 |
. . . . . . . . . . . . . . 15
 
   |
49 | | ssel 3041 |
. . . . . . . . . . . . . . . 16
 
   |
50 | | blcntr 12344 |
. . . . . . . . . . . . . . . . . . . . 21
      
           |
51 | 50 | a1d 22 |
. . . . . . . . . . . . . . . . . . . 20
      
                       |
52 | 51 | ancld 321 |
. . . . . . . . . . . . . . . . . . 19
      
                      
            |
53 | 52 | 3expa 1149 |
. . . . . . . . . . . . . . . . . 18
       
            
          
            |
54 | 53 | reximdva 2493 |
. . . . . . . . . . . . . . . . 17
       
 
                     
            |
55 | 54 | ex 114 |
. . . . . . . . . . . . . . . 16
                  
           
             |
56 | 49, 55 | sylan9r 405 |
. . . . . . . . . . . . . . 15
       

                       
             |
57 | 48, 56 | sylan9r 405 |
. . . . . . . . . . . . . 14
       



                       
             |
58 | 57 | adantrr 466 |
. . . . . . . . . . . . 13
       

 
                         
           
             |
59 | 47, 58 | mpdd 41 |
. . . . . . . . . . . 12
       

 
              
          
            |
60 | 42 | eleq2d 2169 |
. . . . . . . . . . . . . . . 16
         
           |
61 | 44, 60 | anbi12d 460 |
. . . . . . . . . . . . . . 15
            
                   
            |
62 | 61 | rexbidv 2397 |
. . . . . . . . . . . . . 14
  
          
        
           
            |
63 | 62 | rspcev 2744 |
. . . . . . . . . . . . 13
             
           
          
           |
64 | 63 | ex 114 |
. . . . . . . . . . . 12
  
          
         

          
            |
65 | 59, 64 | sylcom 28 |
. . . . . . . . . . 11
       

 
              

          
            |
66 | | simprl 501 |
. . . . . . . . . . . 12
       

 
               |
67 | 66 | sseld 3046 |
. . . . . . . . . . 11
       

 
             
   |
68 | 65, 67 | jcad 303 |
. . . . . . . . . 10
       

 
                           
             |
69 | | elin 3206 |
. . . . . . . . . . . . . . 15
          
            |
70 | | ssel2 3042 |
. . . . . . . . . . . . . . 15
           
          
  |
71 | 69, 70 | sylan2br 284 |
. . . . . . . . . . . . . 14
           

       
 
  |
72 | 71 | expr 370 |
. . . . . . . . . . . . 13
           
             |
73 | 72 | rexlimivw 2504 |
. . . . . . . . . . . 12
            
             |
74 | 73 | rexlimivw 2504 |
. . . . . . . . . . 11
  
                    
   |
75 | 74 | imp 123 |
. . . . . . . . . 10
   
          
        
   |
76 | 68, 75 | impbid1 141 |
. . . . . . . . 9
       

 
             
 

                        |
77 | | elin 3206 |
. . . . . . . . . . 11
      
                  
         
     |
78 | | eluniab 3695 |
. . . . . . . . . . . . . 14
    
          
      

        
     |
79 | | ancom 264 |
. . . . . . . . . . . . . . . 16
    
        
  
  

        
     |
80 | | anass 396 |
. . . . . . . . . . . . . . . 16
    
         

  
           
    |
81 | | r19.41v 2545 |
. . . . . . . . . . . . . . . . . 18
             
 
 
               |
82 | 81 | rexbii 2401 |
. . . . . . . . . . . . . . . . 17
  
           
    
          
    |
83 | | r19.41v 2545 |
. . . . . . . . . . . . . . . . 17
   
          
   
           
    |
84 | 82, 83 | bitr2i 184 |
. . . . . . . . . . . . . . . 16
   
          
   
           
    |
85 | 79, 80, 84 | 3bitri 205 |
. . . . . . . . . . . . . . 15
    
        
  

                 |
86 | 85 | exbii 1552 |
. . . . . . . . . . . . . 14
      
           
  

           
    |
87 | 78, 86 | bitri 183 |
. . . . . . . . . . . . 13
    
          
    
                 |
88 | | rexcom4 2664 |
. . . . . . . . . . . . . . . 16
               
 
  
           
    |
89 | | vex 2644 |
. . . . . . . . . . . . . . . . . . 19
 |
90 | | blex 12315 |
. . . . . . . . . . . . . . . . . . 19
            |
91 | | vex 2644 |
. . . . . . . . . . . . . . . . . . . 20
 |
92 | 91 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
       
  |
93 | | ovexg 5737 |
. . . . . . . . . . . . . . . . . . 19
                 |
94 | 89, 90, 92, 93 | mp3an2ani 1290 |
. . . . . . . . . . . . . . . . . 18
       
          |
95 | | ineq1 3217 |
. . . . . . . . . . . . . . . . . . . . 21
         
             |
96 | 95 | sseq1d 3076 |
. . . . . . . . . . . . . . . . . . . 20
           
             |
97 | | eleq2 2163 |
. . . . . . . . . . . . . . . . . . . 20
         
           |
98 | 96, 97 | anbi12d 460 |
. . . . . . . . . . . . . . . . . . 19
            
           
            |
99 | 98 | ceqsexgv 2768 |
. . . . . . . . . . . . . . . . . 18
                       
 
                       |
100 | 94, 99 | syl 14 |
. . . . . . . . . . . . . . . . 17
       
                
                       |
101 | 100 | rexbidv 2397 |
. . . . . . . . . . . . . . . 16
       
 
             
 
           
            |
102 | 88, 101 | syl5rbbr 194 |
. . . . . . . . . . . . . . 15
       
 
                                  
     |
103 | 102 | rexbidv 2397 |
. . . . . . . . . . . . . 14
       
 

                    
              
     |
104 | | rexcom4 2664 |
. . . . . . . . . . . . . 14
                
 
  

           
    |
105 | 103, 104 | syl6rbb 196 |
. . . . . . . . . . . . 13
       
    
           
 

           
            |
106 | 87, 105 | syl5bb 191 |
. . . . . . . . . . . 12
       
     
         
   
          
            |
107 | 106 | anbi1d 456 |
. . . . . . . . . . 11
       
      
            
 

                        |
108 | 77, 107 | syl5rbb 192 |
. . . . . . . . . 10
       
  

          
        
      
                |
109 | 108 | adantr 272 |
. . . . . . . . 9
       

 
                           
         
     
        
       |
110 | 76, 109 | bitrd 187 |
. . . . . . . 8
       

 
             
     
         
      |
111 | 110 | eqrdv 2098 |
. . . . . . 7
       

 
                  
               |
112 | | ineq1 3217 |
. . . . . . . 8
    
          
         
         
     |
113 | 112 | rspceeqv 2761 |
. . . . . . 7
      
         
 
     
        
     

   |
114 | 41, 111, 113 | syl2anc 406 |
. . . . . 6
       

 
             

   |
115 | 114 | ex 114 |
. . . . 5
       
 
 
          


    |
116 | 20, 115 | impbid 128 |
. . . 4
       
 
 
 
               |
117 | | simpr 109 |
. . . . . . . . . . 11
 
   |
118 | 24, 117 | elind 3208 |
. . . . . . . . . 10
 
     |
119 | | metrest.1 |
. . . . . . . . . . . . . . 15
     |
120 | 119 | blres 12362 |
. . . . . . . . . . . . . 14
                              |
121 | 120 | sseq1d 3076 |
. . . . . . . . . . . . 13
                            
   |
122 | 121 | 3expa 1149 |
. . . . . . . . . . . 12
       

           
             |
123 | 25, 122 | sylan2 282 |
. . . . . . . . . . 11
       

  
                  
   |
124 | 123 | rexbidva 2393 |
. . . . . . . . . 10
         
 
                  
   |
125 | 118, 124 | sylan2 282 |
. . . . . . . . 9
           
                  
   |
126 | 125 | anassrs 395 |
. . . . . . . 8
       

  
                  
   |
127 | 23, 126 | sylan2 282 |
. . . . . . 7
       

            
              |
128 | 127 | anassrs 395 |
. . . . . 6
             
                  
   |
129 | 128 | ralbidva 2392 |
. . . . 5
       


 

         
             |
130 | 129 | pm5.32da 443 |
. . . 4
       
 
 
        
 
               |
131 | 116, 130 | bitr4d 190 |
. . 3
       
 
 
 
             |
132 | 21 | adantr 272 |
. . . 4
       
  |
133 | | id 19 |
. . . . 5
   |
134 | 2 | mopnm 12376 |
. . . . 5
        |
135 | | ssexg 4007 |
. . . . 5
 
   |
136 | 133, 134,
135 | syl2anr 286 |
. . . 4
       
  |
137 | | elrest 11909 |
. . . 4
 
   ↾t 


    |
138 | 132, 136,
137 | syl2anc 406 |
. . 3
       
 
↾t 


    |
139 | | xmetres2 12307 |
. . . . 5
       
           |
140 | 119, 139 | syl5eqel 2186 |
. . . 4
       
       |
141 | | metrest.4 |
. . . . 5
     |
142 | 141 | elmopn2 12377 |
. . . 4
      
 
             |
143 | 140, 142 | syl 14 |
. . 3
       

               |
144 | 131, 138,
143 | 3bitr4d 219 |
. 2
       
 
↾t 
   |
145 | 144 | eqrdv 2098 |
1
       
 ↾t    |