Step | Hyp | Ref
| Expression |
1 | | ltso 9732 |
. . . 4
 |
2 | 1 | a1i 11 |
. . 3
         
  |
3 | | simplr 770 |
. . 3
         
       |
4 | | vex 3034 |
. . . . . . 7
 |
5 | | eqeq1 2475 |
. . . . . . . . 9
     
       |
6 | 5 | anbi2d 718 |
. . . . . . . 8
  
     
        |
7 | 6 | rexbidv 2892 |
. . . . . . 7
  
              
      
            |
8 | 4, 7 | elab 3173 |
. . . . . 6
            
      
                 |
9 | | simprl 772 |
. . . . . . . . 9
         
      
  |
10 | | ovolss 22516 |
. . . . . . . . . . 11
 
             |
11 | | sstr 3426 |
. . . . . . . . . . . . 13
 

  |
12 | | ovolcl 22509 |
. . . . . . . . . . . . 13

       |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . 12
 
        |
14 | | ovolcl 22509 |
. . . . . . . . . . . . 13

       |
15 | 14 | adantl 473 |
. . . . . . . . . . . 12
 
        |
16 | | xrlenlt 9717 |
. . . . . . . . . . . 12
                       
             |
17 | 13, 15, 16 | syl2anc 673 |
. . . . . . . . . . 11
 
                         |
18 | 10, 17 | mpbid 215 |
. . . . . . . . . 10
 
             |
19 | 18 | ancoms 460 |
. . . . . . . . 9
 
     
       |
20 | 9, 19 | sylan2 482 |
. . . . . . . 8
 
        
       
            |
21 | | simprrr 783 |
. . . . . . . . . 10
 
        
              |
22 | | uniretop 21861 |
. . . . . . . . . . . . . . 15
      |
23 | 22 | cldss 20121 |
. . . . . . . . . . . . . 14
      
 
  |
24 | | dfss4 3668 |
. . . . . . . . . . . . . 14

      |
25 | 23, 24 | sylib 201 |
. . . . . . . . . . . . 13
      
 
      |
26 | | rembl 22572 |
. . . . . . . . . . . . . 14
 |
27 | 22 | cldopn 20123 |
. . . . . . . . . . . . . . 15
      
 
        |
28 | | opnmbl 22639 |
. . . . . . . . . . . . . . 15
      
    |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . 14
      
 
    |
30 | | difmbl 22575 |
. . . . . . . . . . . . . 14
           |
31 | 26, 29, 30 | sylancr 676 |
. . . . . . . . . . . . 13
      
 
      |
32 | 25, 31 | eqeltrrd 2550 |
. . . . . . . . . . . 12
      
 
  |
33 | | mblvol 22562 |
. . . . . . . . . . . 12
            |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
      
 
           |
35 | 34 | ad2antrl 742 |
. . . . . . . . . 10
 
        
                   |
36 | 21, 35 | eqtrd 2505 |
. . . . . . . . 9
 
        
               |
37 | 36 | breq2d 4407 |
. . . . . . . 8
 
        
                           |
38 | 20, 37 | mtbird 308 |
. . . . . . 7
 
        
       
       |
39 | 38 | rexlimdvaa 2872 |
. . . . . 6

                
        |
40 | 8, 39 | syl5bi 225 |
. . . . 5

            
     
        |
41 | 40 | ad2antrr 740 |
. . . 4
         
  
                    
   |
42 | 41 | imp 436 |
. . 3
            
                        |
43 | | 1rp 11329 |
. . . . . . . . 9
 |
44 | | eqid 2471 |
. . . . . . . . . 10
   
     
   |
45 | 44 | ovolgelb 22511 |
. . . . . . . . 9
 
        
                 
          |
46 | 43, 45 | mp3an3 1379 |
. . . . . . . 8
 
      

     
        
              |
47 | | elmapi 7511 |
. . . . . . . . . . 11
         
     |
48 | | ssid 3437 |
. . . . . . . . . . . . . . 15
       |
49 | 44 | ovollb 22510 |
. . . . . . . . . . . . . . 15
           
                 
      |
50 | 48, 49 | mpan2 685 |
. . . . . . . . . . . . . 14
               
     
   
  |
51 | 50 | adantl 473 |
. . . . . . . . . . . . 13
                            
      |
52 | | eqid 2471 |
. . . . . . . . . . . . . . . 16
    
  |
53 | 52, 44 | ovolsf 22503 |
. . . . . . . . . . . . . . 15
           
           |
54 | | frn 5747 |
. . . . . . . . . . . . . . . 16
   
        
   
 
     |
55 | | icossxr 11744 |
. . . . . . . . . . . . . . . 16
    |
56 | 54, 55 | syl6ss 3430 |
. . . . . . . . . . . . . . 15
   
        
   
 
  |
57 | | supxrcl 11625 |
. . . . . . . . . . . . . . 15
    
       
      |
58 | 53, 56, 57 | 3syl 18 |
. . . . . . . . . . . . . 14
                 
  |
59 | | peano2re 9824 |
. . . . . . . . . . . . . . 15
               |
60 | 59 | rexrd 9708 |
. . . . . . . . . . . . . 14
               |
61 | | rncoss 5101 |
. . . . . . . . . . . . . . . . . 18
   |
62 | 61 | unissi 4213 |
. . . . . . . . . . . . . . . . 17
     |
63 | | unirnioo 11759 |
. . . . . . . . . . . . . . . . 17
  |
64 | 62, 63 | sseqtr4i 3451 |
. . . . . . . . . . . . . . . 16
    |
65 | | ovolcl 22509 |
. . . . . . . . . . . . . . . 16
   
          |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . . 15
         |
67 | | xrletr 11478 |
. . . . . . . . . . . . . . 15
         
     
   
                       
             
               
          |
68 | 66, 67 | mp3an1 1377 |
. . . . . . . . . . . . . 14
       
                           
             
               
          |
69 | 58, 60, 68 | syl2anr 486 |
. . . . . . . . . . . . 13
                              
             
               
          |
70 | 51, 69 | mpand 689 |
. . . . . . . . . . . 12
                     
   
      
                  |
71 | 70 | adantll 728 |
. . . . . . . . . . 11
            
          
   
      
                  |
72 | 47, 71 | sylan2 482 |
. . . . . . . . . 10
         
           
   
      
                  |
73 | 72 | anim2d 575 |
. . . . . . . . 9
         
               
                       
           |
74 | 73 | reximdva 2858 |
. . . . . . . 8
 
         
                 
          
               
           |
75 | 46, 74 | mpd 15 |
. . . . . . 7
 
      

     
                     |
76 | | rexex 2843 |
. . . . . . 7
  
                
                                |
77 | 75, 76 | syl 17 |
. . . . . 6
 
                   
          |
78 | 77 | ad2antrr 740 |
. . . . 5
                                           |
79 | | difss 3549 |
. . . . . . . . . . . . . 14
   
 
   |
80 | 79, 64 | sstri 3427 |
. . . . . . . . . . . . 13
   
  |
81 | | ovolcl 22509 |
. . . . . . . . . . . . 13
                  |
82 | 80, 81 | ax-mp 5 |
. . . . . . . . . . . 12
       
   |
83 | 59, 82 | jctil 546 |
. . . . . . . . . . 11
                
          |
84 | 83 | ad4antlr 747 |
. . . . . . . . . 10
    
     
                                        
          |
85 | | ovolss 22516 |
. . . . . . . . . . . . . . 15
             
       
 
          |
86 | 79, 64, 85 | mp2an 686 |
. . . . . . . . . . . . . 14
       
 
         |
87 | | xrletr 11478 |
. . . . . . . . . . . . . . . 16
           
       
                 
 
                                            |
88 | 82, 66, 87 | mp3an12 1380 |
. . . . . . . . . . . . . . 15
                                                   
 
          |
89 | 60, 88 | syl 17 |
. . . . . . . . . . . . . 14
                                                 
 
          |
90 | 86, 89 | mpani 690 |
. . . . . . . . . . . . 13
                     
                    |
91 | 90 | ad4antlr 747 |
. . . . . . . . . . . 12
    
     
         
                                       |
92 | 91 | impr 631 |
. . . . . . . . . . 11
    
     
                                                 |
93 | | ovolge0 22512 |
. . . . . . . . . . . 12
     
            |
94 | 80, 93 | ax-mp 5 |
. . . . . . . . . . 11
           |
95 | 92, 94 | jctil 546 |
. . . . . . . . . 10
    
     
                                      
 
                    |
96 | | xrrege0 11492 |
. . . . . . . . . 10
            
        
                                         |
97 | 84, 95, 96 | syl2anc 673 |
. . . . . . . . 9
    
     
                                          |
98 | | resubcl 9958 |
. . . . . . . . . . . . . 14
                 |
99 | 98 | adantrr 731 |
. . . . . . . . . . . . 13
                        |
100 | | posdif 10128 |
. . . . . . . . . . . . . . . 16
             
          |
101 | 100 | ancoms 460 |
. . . . . . . . . . . . . . 15
             
          |
102 | 101 | biimpd 212 |
. . . . . . . . . . . . . 14
                        |
103 | 102 | impr 631 |
. . . . . . . . . . . . 13
                        |
104 | 99, 103 | elrpd 11361 |
. . . . . . . . . . . 12
                        |
105 | 104 | rphalfcld 11376 |
. . . . . . . . . . 11
                          |
106 | 3, 105 | sylan 479 |
. . . . . . . . . 10
                              |
107 | 106 | adantr 472 |
. . . . . . . . 9
    
     
                                         |
108 | | eqid 2471 |
. . . . . . . . . . 11
   
     
   |
109 | 108 | ovolgelb 22511 |
. . . . . . . . . 10
                             
        
 
           
                        |
110 | 80, 109 | mp3an1 1377 |
. . . . . . . . 9
                        
        
 
           
                        |
111 | 97, 107, 110 | syl2anc 673 |
. . . . . . . 8
    
     
                              

                   
   
                        |
112 | | elmapi 7511 |
. . . . . . . . . . 11
         
     |
113 | | ssid 3437 |
. . . . . . . . . . . . . 14
       |
114 | 108 | ovollb 22510 |
. . . . . . . . . . . . . 14
           
                 
      |
115 | 113, 114 | mpan2 685 |
. . . . . . . . . . . . 13
               
     
   
  |
116 | 115 | adantl 473 |
. . . . . . . . . . . 12
     
     
                                                   
      |
117 | | eqid 2471 |
. . . . . . . . . . . . . . 15
    
  |
118 | 117, 108 | ovolsf 22503 |
. . . . . . . . . . . . . 14
           
           |
119 | | frn 5747 |
. . . . . . . . . . . . . . 15
   
        
   
 
     |
120 | 119, 55 | syl6ss 3430 |
. . . . . . . . . . . . . 14
   
        
   
 
  |
121 | | supxrcl 11625 |
. . . . . . . . . . . . . 14
    
       
      |
122 | 118, 120,
121 | 3syl 18 |
. . . . . . . . . . . . 13
                 
  |
123 | 99 | rehalfcld 10882 |
. . . . . . . . . . . . . . . . 17
                          |
124 | 3, 123 | sylan 479 |
. . . . . . . . . . . . . . . 16
                              |
125 | 124 | adantr 472 |
. . . . . . . . . . . . . . 15
    
     
                                         |
126 | 97, 125 | readdcld 9688 |
. . . . . . . . . . . . . 14
    
     
                                                     |
127 | 126 | rexrd 9708 |
. . . . . . . . . . . . 13
    
     
                                                     |
128 | | rncoss 5101 |
. . . . . . . . . . . . . . . . 17
   |
129 | 128 | unissi 4213 |
. . . . . . . . . . . . . . . 16
     |
130 | 129, 63 | sseqtr4i 3451 |
. . . . . . . . . . . . . . 15
    |
131 | | ovolcl 22509 |
. . . . . . . . . . . . . . 15
   
          |
132 | 130, 131 | ax-mp 5 |
. . . . . . . . . . . . . 14
         |
133 | | xrletr 11478 |
. . . . . . . . . . . . . 14
         
     
   
        
                            
             
                                                      |
134 | 132, 133 | mp3an1 1377 |
. . . . . . . . . . . . 13
       
                                             
     
            
                    
        
               |
135 | 122, 127,
134 | syl2anr 486 |
. . . . . . . . . . . 12
     
     
                                                     
             
                                                      |
136 | 116, 135 | mpand 689 |
. . . . . . . . . . 11
     
     
                                            
   
                            
        
               |
137 | 112, 136 | sylan2 482 |
. . . . . . . . . 10
     
     
                             
            
            
           
                
               |
138 | 137 | anim2d 575 |
. . . . . . . . 9
     
     
                             
                         
                                      
        
                |
139 | 138 | reximdva 2858 |
. . . . . . . 8
    
     
                                 
        
 
           
                      

                              
                |
140 | 111, 139 | mpd 15 |
. . . . . . 7
    
     
                              

                              
               |
141 | | rexex 2843 |
. . . . . . 7
  
         
 
         
        
                               
        
               |
142 | 140, 141 | syl 17 |
. . . . . 6
    
     
                                    
 
         
        
               |
143 | 59, 66 | jctil 546 |
. . . . . . . . . . . 12
              
          |
144 | 143 | ad3antlr 745 |
. . . . . . . . . . 11
                           
          |
145 | | ovolge0 22512 |
. . . . . . . . . . . . . 14
   
          |
146 | 64, 145 | ax-mp 5 |
. . . . . . . . . . . . 13
         |
147 | 146 | jctl 550 |
. . . . . . . . . . . 12
               
                           |
148 | 147 | adantl 473 |
. . . . . . . . . . 11
 
                   
                          |
149 | | xrrege0 11492 |
. . . . . . . . . . 11
          
                                            |
150 | 144, 148,
149 | syl2an 485 |
. . . . . . . . . 10
    
     
                                        |
151 | 150, 125 | resubcld 10068 |
. . . . . . . . 9
    
     
                                                   |
152 | 150, 107 | ltsubrpd 11393 |
. . . . . . . . 9
    
     
                                                           |
153 | | retop 21860 |
. . . . . . . . . . 11
     |
154 | | retopbas 21859 |
. . . . . . . . . . . . 13
 |
155 | | bastg 20058 |
. . . . . . . . . . . . 13

      |
156 | 154, 155 | ax-mp 5 |
. . . . . . . . . . . 12
     |
157 | 61, 156 | sstri 3427 |
. . . . . . . . . . 11
       |
158 | | uniopn 20004 |
. . . . . . . . . . 11
            
         |
159 | 153, 157,
158 | mp2an 686 |
. . . . . . . . . 10
        |
160 | | mblfinlem2 32042 |
. . . . . . . . . 10
                                                              
                                  |
161 | 159, 160 | mp3an1 1377 |
. . . . . . . . 9
                                                       
                                  |
162 | 151, 152,
161 | syl2anc 673 |
. . . . . . . 8
    
     
                              
                                        |
163 | 162 | adantr 472 |
. . . . . . 7
     
     
                                              
        
              
                                        |
164 | | indif2 3677 |
. . . . . . . . . . . . . . 15
               |
165 | 22 | cldss 20121 |
. . . . . . . . . . . . . . . . 17
      
 
  |
166 | | df-ss 3404 |
. . . . . . . . . . . . . . . . 17

    |
167 | 165, 166 | sylib 201 |
. . . . . . . . . . . . . . . 16
      
 
    |
168 | 167 | difeq1d 3539 |
. . . . . . . . . . . . . . 15
      
 
 
            |
169 | 164, 168 | syl5eq 2517 |
. . . . . . . . . . . . . 14
      
 
              |
170 | 128, 156 | sstri 3427 |
. . . . . . . . . . . . . . . . 17
       |
171 | | uniopn 20004 |
. . . . . . . . . . . . . . . . 17
            
         |
172 | 153, 170,
171 | mp2an 686 |
. . . . . . . . . . . . . . . 16
        |
173 | 22 | opncld 20125 |
. . . . . . . . . . . . . . . 16
                        
    |
174 | 153, 172,
173 | mp2an 686 |
. . . . . . . . . . . . . . 15
          
   |
175 | | incld 20135 |
. . . . . . . . . . . . . . 15
         
 
        
   
 
         
    |
176 | 174, 175 | mpan2 685 |
. . . . . . . . . . . . . 14
      
 
            
    |
177 | 169, 176 | eqeltrrd 2550 |
. . . . . . . . . . . . 13
      
 
          
    |
178 | | simpr 468 |
. . . . . . . . . . . . . . 15
             
     |
179 | | simpl 464 |
. . . . . . . . . . . . . . 15
             
   
 
    |
180 | 178, 179 | ssdif2d 3561 |
. . . . . . . . . . . . . 14
             
                 |
181 | | dfin4 3674 |
. . . . . . . . . . . . . . 15
   
            |
182 | | inss2 3644 |
. . . . . . . . . . . . . . 15
   
  |
183 | 181, 182 | eqsstr3i 3449 |
. . . . . . . . . . . . . 14
   
   
 
 |
184 | 180, 183 | syl6ss 3430 |
. . . . . . . . . . . . 13
             
       |
185 | | sseq1 3439 |
. . . . . . . . . . . . . . . 16
           
   |
186 | 185 | anbi1d 719 |
. . . . . . . . . . . . . . 15
           
         
 
                     |
187 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
         
           |
188 | 187 | eqcoms 2479 |
. . . . . . . . . . . . . . . 16
         
           |
189 | 188 | biantrud 515 |
. . . . . . . . . . . . . . 15
                     
             |
190 | 186, 189 | bitr4d 264 |
. . . . . . . . . . . . . 14
           
         
        |
191 | 190 | rspcev 3136 |
. . . . . . . . . . . . 13
                    
      
       
            |
192 | 177, 184,
191 | syl2an 485 |
. . . . . . . . . . . 12
         
     
       
      
       
            |
193 | 192 | an12s 818 |
. . . . . . . . . . 11
                
 
               
                |
194 | 193 | adantrrr 739 |
. . . . . . . . . 10
                
 
 
                             
                          |
195 | 194 | adantlr 729 |
. . . . . . . . 9
                  
        
                     
 
                             
                          |
196 | 195 | adantll 728 |
. . . . . . . 8
                                 
                                  
                                                     
      
       
            |
197 | | difss 3549 |
. . . . . . . . . . . 12
        |
198 | | ovolsscl 22517 |
. . . . . . . . . . . 12
   
    
          

        |
199 | 197, 198 | mp3an1 1377 |
. . . . . . . . . . 11
 
          

        |
200 | 199 | ad5antr 748 |
. . . . . . . . . 10
                                 
                                  
                                                     
              |
201 | | simp-6r 789 |
. . . . . . . . . 10
                                 
                                  
                                                     
       |
202 | | simpl 464 |
. . . . . . . . . . 11
       
  |
203 | 202 | ad4antlr 747 |
. . . . . . . . . 10
                                 
                                  
                                                     
  |
204 | | difdif2 3691 |
. . . . . . . . . . . 12
                 |
205 | 204 | fveq2i 5882 |
. . . . . . . . . . 11
                           |
206 | | difss 3549 |
. . . . . . . . . . . . . . 15
   |
207 | | inss1 3643 |
. . . . . . . . . . . . . . 15
      |
208 | 206, 207 | unssi 3600 |
. . . . . . . . . . . . . 14
          |
209 | | ovolsscl 22517 |
. . . . . . . . . . . . . 14
          
                      |
210 | 208, 209 | mp3an1 1377 |
. . . . . . . . . . . . 13
 
                      |
211 | 210 | ad5antr 748 |
. . . . . . . . . . . 12
                                 
                                  
                                                     
                |
212 | | ovolsscl 22517 |
. . . . . . . . . . . . . . 15
   
          
    |
213 | 206, 212 | mp3an1 1377 |
. . . . . . . . . . . . . 14
 
          
    |
214 | 213 | ad5antr 748 |
. . . . . . . . . . . . 13
                                 
                                  
                                                     
         |
215 | | ovolsscl 22517 |
. . . . . . . . . . . . . . 15
      
                  |
216 | 207, 215 | mp3an1 1377 |
. . . . . . . . . . . . . 14
 
          
       |
217 | 216 | ad5antr 748 |
. . . . . . . . . . . . 13
                                 
                                  
                                                     
            |
218 | 214, 217 | readdcld 9688 |
. . . . . . . . . . . 12
                                 
                                  
                                                     
                     |
219 | 3, 202, 98 | syl2an 485 |
. . . . . . . . . . . . 13
                            |
220 | 219 | ad3antrrr 744 |
. . . . . . . . . . . 12
                                 
                                  
                                                     
         |
221 | | ssdifss 3553 |
. . . . . . . . . . . . . . 15

    |
222 | 221 | adantr 472 |
. . . . . . . . . . . . . 14
 
       
  |
223 | | ssinss1 3651 |
. . . . . . . . . . . . . . 15

       |
224 | 223 | adantr 472 |
. . . . . . . . . . . . . 14
 
             |
225 | | ovolun 22530 |
. . . . . . . . . . . . . 14
         
        
           
                          
        |
226 | 222, 213,
224, 216, 225 | syl22anc 1293 |
. . . . . . . . . . . . 13
 
                         
               |
227 | 226 | ad5antr 748 |
. . . . . . . . . . . 12
                                 
                                  
                                                     
                          
        |
228 | 124 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
     
     
                                              
        
                         |
229 | 228 | adantr 472 |
. . . . . . . . . . . . . 14
                                 
                                  
                                                     
           |
230 | 150 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
                                 
                                  
                                                     
          |
231 | | simprl 772 |
. . . . . . . . . . . . . . . . 17
         
 
                            
    |
232 | 150 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
     
                                              
        
                        |
233 | | ovolsscl 22517 |
. . . . . . . . . . . . . . . . . 18
 
                      |
234 | 64, 233 | mp3an2 1378 |
. . . . . . . . . . . . . . . . 17
 
                   |
235 | 231, 232,
234 | syl2anr 486 |
. . . . . . . . . . . . . . . 16
                                 
                                  
                                             |