Step | Hyp | Ref
| Expression |
1 | | unieq 4198 |
. . . . . . . . 9

    |
2 | | uni0 4217 |
. . . . . . . . 9
  |
3 | 1, 2 | syl6eq 2521 |
. . . . . . . 8

   |
4 | 3 | fveq2d 5883 |
. . . . . . 7

           |
5 | | 0mbl 22571 |
. . . . . . . . 9
 |
6 | | mblvol 22562 |
. . . . . . . . 9

           |
7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
          |
8 | | ovol0 22524 |
. . . . . . . 8
      |
9 | 7, 8 | eqtri 2493 |
. . . . . . 7
     |
10 | 4, 9 | syl6req 2522 |
. . . . . 6

       |
11 | 10 | a1d 25 |
. . . . 5

 
 
           |
12 | | reldom 7593 |
. . . . . . . . . . 11
 |
13 | 12 | brrelexi 4880 |
. . . . . . . . . 10

  |
14 | | 0sdomg 7719 |
. . . . . . . . . 10
 
   |
15 | 13, 14 | syl 17 |
. . . . . . . . 9


   |
16 | 15 | biimparc 495 |
. . . . . . . 8
  
  |
17 | | fodomr 7741 |
. . . . . . . 8
  
       |
18 | 16, 17 | sylancom 680 |
. . . . . . 7
  
       |
19 | | unissb 4221 |
. . . . . . . . . . . . 13
 

  |
20 | 19 | anbi1i 709 |
. . . . . . . . . . . 12
    
 

   |
21 | | r19.26 2904 |
. . . . . . . . . . . 12
 


 
    |
22 | 20, 21 | bitr4i 260 |
. . . . . . . . . . 11
    

    |
23 | | ovolctb2 22523 |
. . . . . . . . . . . . . 14
 

       |
24 | 23 | ex 441 |
. . . . . . . . . . . . 13


        |
25 | 24 | imdistani 704 |
. . . . . . . . . . . 12
 


        |
26 | 25 | ralimi 2796 |
. . . . . . . . . . 11
 



         |
27 | 22, 26 | sylbi 200 |
. . . . . . . . . 10
     

        |
28 | 27 | ancoms 460 |
. . . . . . . . 9
  
  
         |
29 | | foima 5811 |
. . . . . . . . . . . 12
        
  |
30 | 29 | raleqdv 2979 |
. . . . . . . . . . 11
                    
         |
31 | | fofn 5808 |
. . . . . . . . . . . 12
       |
32 | | ssid 3437 |
. . . . . . . . . . . 12
 |
33 | | sseq1 3439 |
. . . . . . . . . . . . . 14
     
       |
34 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
                     |
35 | 34 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
                       |
36 | 33, 35 | anbi12d 725 |
. . . . . . . . . . . . 13
                               |
37 | 36 | ralima 6163 |
. . . . . . . . . . . 12
                                    |
38 | 31, 32, 37 | sylancl 675 |
. . . . . . . . . . 11
                                      |
39 | 30, 38 | bitr3d 263 |
. . . . . . . . . 10
                                 |
40 | | difss 3549 |
. . . . . . . . . . . . . . . . . 18
       ..^      
     |
41 | | ovolssnul 22518 |
. . . . . . . . . . . . . . . . . 18
       
 ..^                                    ..^          |
42 | 40, 41 | mp3an1 1377 |
. . . . . . . . . . . . . . . . 17
     
                   
 ..^          |
43 | | ssdifss 3553 |
. . . . . . . . . . . . . . . . . 18
    
       ..^      
  |
44 | | nulmbl 22567 |
. . . . . . . . . . . . . . . . . . 19
       
 ..^      
           ..^        
       ..^         |
45 | | mblvol 22562 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
  ..^              
  ..^                 
 ..^          |
46 | 45 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
  ..^               
  ..^                 
 ..^           |
47 | 46 | biimpar 493 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
 ..^               
  ..^                 
 ..^          |
48 | | 0re 9661 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
49 | 47, 48 | syl6eqel 2557 |
. . . . . . . . . . . . . . . . . . . . . 22
       
 ..^               
  ..^                 
 ..^          |
50 | 49 | expcom 442 |
. . . . . . . . . . . . . . . . . . . . 21
         
  ..^       
     
  ..^              
  ..^           |
51 | 50 | ancld 562 |
. . . . . . . . . . . . . . . . . . . 20
         
  ..^       
     
  ..^             
 ..^              
  ..^            |
52 | 51 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
       
 ..^      
           ..^        
     
  ..^             
 ..^              
  ..^            |
53 | 44, 52 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
       
 ..^      
           ..^        
     
  ..^              
  ..^           |
54 | 43, 53 | sylan 479 |
. . . . . . . . . . . . . . . . 17
     
           ..^        
     
  ..^              
  ..^           |
55 | 42, 54 | syldan 478 |
. . . . . . . . . . . . . . . 16
     
                
 ..^              
  ..^           |
56 | 55 | ralimi 2796 |
. . . . . . . . . . . . . . 15
 
    
          
      
 ..^              
  ..^           |
57 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
           |
58 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . . 22
  ..^  ..^   |
59 | 58 | iuneq1d 4294 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^        ..^        |
60 | 57, 59 | difeq12d 3541 |
. . . . . . . . . . . . . . . . . . . 20
     
  ..^           
  ..^         |
61 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . 20
        ..^             
  ..^         |
62 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . 21
     |
63 | | difexg 4545 |
. . . . . . . . . . . . . . . . . . . . 21
         
  ..^         |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
       ..^        |
65 | 60, 61, 64 | fvmpt 5963 |
. . . . . . . . . . . . . . . . . . 19
        
 ..^                
 ..^         |
66 | 65 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . 18
         
 ..^               
  ..^          |
67 | 65 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
             ..^                      ..^          |
68 | 67 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . 18
            
 ..^           
        
 ..^           |
69 | 66, 68 | anbi12d 725 |
. . . . . . . . . . . . . . . . 17
            ..^                     
 ..^                   
 ..^              
  ..^            |
70 | 69 | ralbiia 2822 |
. . . . . . . . . . . . . . . 16
 
        
 ..^                     
 ..^             
      
 ..^              
  ..^           |
71 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
           |
72 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^  ..^   |
73 | 72 | iuneq1d 4294 |
. . . . . . . . . . . . . . . . . . . 20
   ..^        ..^        |
74 | 71, 73 | difeq12d 3541 |
. . . . . . . . . . . . . . . . . . 19
     
  ..^           
  ..^         |
75 | 74 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . 18
       
 ..^      
       ..^          |
76 | 74 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
         
 ..^                  ..^          |
77 | 76 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . 18
         
  ..^               
  ..^           |
78 | 75, 77 | anbi12d 725 |
. . . . . . . . . . . . . . . . 17
        
 ..^              
  ..^        
     
  ..^              
  ..^            |
79 | 78 | cbvralv 3005 |
. . . . . . . . . . . . . . . 16
 
      
 ..^                 ..^                
 ..^              
  ..^           |
80 | 70, 79 | bitri 257 |
. . . . . . . . . . . . . . 15
 
        
 ..^                     
 ..^             
      
 ..^              
  ..^           |
81 | 56, 80 | sylibr 217 |
. . . . . . . . . . . . . 14
 
    
          
          ..^                     
 ..^               |
82 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
           |
83 | 82 | iundisj2 22581 |
. . . . . . . . . . . . . . 15
Disj      
 ..^        |
84 | | disjeq2 4370 |
. . . . . . . . . . . . . . . 16
 
       
 ..^                
 ..^      
Disj          ..^           Disj     
  ..^          |
85 | 84, 65 | mprg 2770 |
. . . . . . . . . . . . . . 15
Disj          ..^           Disj     
  ..^         |
86 | 83, 85 | mpbir 214 |
. . . . . . . . . . . . . 14
Disj          ..^            |
87 | | nnex 10637 |
. . . . . . . . . . . . . . . . 17
 |
88 | 87 | mptex 6152 |
. . . . . . . . . . . . . . . 16
        ..^         |
89 | | fveq1 5878 |
. . . . . . . . . . . . . . . . . . . . 21
       
 ..^                     ..^             |
90 | 89 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . 20
       
 ..^                    
 ..^              |
91 | 89 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
       
 ..^                          
 ..^              |
92 | 91 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . 20
       
 ..^                
          
 ..^               |
93 | 90, 92 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . 19
       
 ..^                                 ..^                     
 ..^                |
94 | 93 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . 18
       
 ..^         
              
          ..^                     
 ..^                |
95 | 89 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
          ..^                      ..^             |
96 | 95 | disjeq2dv 4371 |
. . . . . . . . . . . . . . . . . 18
       
 ..^        Disj    
Disj        
 ..^              |
97 | 94, 96 | anbi12d 725 |
. . . . . . . . . . . . . . . . 17
       
 ..^                         Disj               
  ..^                     
 ..^             Disj        
 ..^               |
98 | 89 | iuneq2d 4296 |
. . . . . . . . . . . . . . . . . . 19
       
 ..^             
       
 ..^             |
99 | 98 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
       
 ..^                              ..^              |
100 | | voliunnfl.1 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
101 | | voliunnfl.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
102 | | seqeq3 12256 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             |
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
104 | 100, 103 | eqtri 2493 |
. . . . . . . . . . . . . . . . . . . . 21
              |
105 | 104 | rneqi 5067 |
. . . . . . . . . . . . . . . . . . . 20
              |
106 | 105 | supeq1i 7979 |
. . . . . . . . . . . . . . . . . . 19
                    
 |
107 | 91 | mpteq2dv 4483 |
. . . . . . . . . . . . . . . . . . . . . 22
       
 ..^                             
 ..^               |
108 | 107 | seqeq3d 12259 |
. . . . . . . . . . . . . . . . . . . . 21
       
 ..^                                 
  ..^                |
109 | 108 | rneqd 5068 |
. . . . . . . . . . . . . . . . . . . 20
       
 ..^                                 
  ..^                |
110 | 109 | supeq1d 7978 |
. . . . . . . . . . . . . . . . . . 19
       
 ..^                                       
  ..^                  |
111 | 106, 110 | syl5eq 2517 |
. . . . . . . . . . . . . . . . . 18
       
 ..^                           
 ..^                  |
112 | 99, 111 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . 17
       
 ..^                                   ..^                           
 ..^                   |
113 | 97, 112 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
       
 ..^                          Disj     
             
  
          ..^                     
 ..^             Disj        
 ..^           
           
 ..^                           
 ..^                    |
114 | | voliunnfl.3 |
. . . . . . . . . . . . . . . 16
                 Disj     
               |
115 | 88, 113, 114 | vtocl 3086 |
. . . . . . . . . . . . . . 15
             ..^                     
 ..^             Disj        
 ..^           
           
 ..^                           
 ..^                  |
116 | 65 | iuneq2i 4288 |
. . . . . . . . . . . . . . . 16
          ..^                 
 ..^        |
117 | 116 | fveq2i 5882 |
. . . . . . . . . . . . . . 15
           
 ..^                     
 ..^         |
118 | 67 | mpteq2ia 4478 |
. . . . . . . . . . . . . . . . . 18
           
 ..^                        ..^          |
119 | | seqeq3 12256 |
. . . . . . . . . . . . . . . . . 18
           
  ..^                     
  ..^                      
 ..^                        
  ..^            |
120 | 118, 119 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
            
  ..^                           ..^           |
121 | 120 | rneqi 5067 |
. . . . . . . . . . . . . . . 16
            
  ..^                           ..^           |
122 | 121 | supeq1i 7979 |
. . . . . . . . . . . . . . 15
               
 ..^               
               ..^             |
123 | 115, 117,
122 | 3eqtr3g 2528 |
. . . . . . . . . . . . . 14
             ..^                     
 ..^             Disj        
 ..^           
         
 ..^                    
  ..^              |
124 | 81, 86, 123 | sylancl 675 |
. . . . . . . . . . . . 13
 
    
                   
 ..^                     
 ..^           
  |
125 | 124 | adantl 473 |
. . . . . . . . . . . 12
                                
 ..^                     
 ..^           
  |
126 | 82 | iundisj 22580 |
. . . . . . . . . . . . . . . 16
     
    
  ..^        |
127 | | fofun 5807 |
. . . . . . . . . . . . . . . . 17
       |
128 | | funiunfv 6171 |
. . . . . . . . . . . . . . . . 17

            |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . 16
     
           |
130 | 126, 129 | syl5eqr 2519 |
. . . . . . . . . . . . . . 15
     
     
 ..^              |
131 | 29 | unieqd 4200 |
. . . . . . . . . . . . . . 15
         
   |
132 | 130, 131 | eqtrd 2505 |
. . . . . . . . . . . . . 14
     
     
 ..^          |
133 | 132 | fveq2d 5883 |
. . . . . . . . . . . . 13
              
 ..^               |
134 | 133 | adantr 472 |
. . . . . . . . . . . 12
                                
 ..^               |
135 | 57 | sseq1d 3445 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
136 | 57 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . 22
                     |
137 | 136 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
138 | 135, 137 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
139 | 138 | rspccva 3135 |
. . . . . . . . . . . . . . . . . . 19
                       
            |
140 | | ssdifss 3553 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
       ..^      
  |
141 | 140 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
     
               
 ..^         |
142 | | difss 3549 |
. . . . . . . . . . . . . . . . . . . . . . 23
       ..^      
     |
143 | | ovolssnul 22518 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
 ..^                                    ..^          |
144 | 142, 143 | mp3an1 1377 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                   
 ..^          |
145 | 141, 144 | jca 541 |
. . . . . . . . . . . . . . . . . . . . 21
     
                
 ..^      
           ..^           |
146 | | nulmbl 22567 |
. . . . . . . . . . . . . . . . . . . . 21
       
 ..^      
           ..^        
       ..^         |
147 | | mblvol 22562 |
. . . . . . . . . . . . . . . . . . . . 21
     
  ..^              
  ..^                 
 ..^          |
148 | 145, 146,
147 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
     
                 
  ..^                 
 ..^          |
149 | 148, 144 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . 19
     
                 
  ..^          |
150 | 139, 149 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                           
 ..^          |
151 | 150 | mpteq2dva 4482 |
. . . . . . . . . . . . . . . . 17
 
    
                     ..^             |
152 | 151 | seqeq3d 12259 |
. . . . . . . . . . . . . . . 16
 
    
                       ..^                 |
153 | 152 | rneqd 5068 |
. . . . . . . . . . . . . . 15
 
    
                    
  ..^                 |
154 | 153 | supeq1d 7978 |
. . . . . . . . . . . . . 14
 
    
                         ..^                    
  |
155 | | 0cn 9653 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
156 | | ser1const 12307 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
157 | 155, 156 | mpan 684 |
. . . . . . . . . . . . . . . . . . . . 21
               |
158 | | nncn 10639 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
159 | 158 | mul01d 9850 |
. . . . . . . . . . . . . . . . . . . . 21
     |
160 | 157, 159 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . 20
             |
161 | 160 | mpteq2ia 4478 |
. . . . . . . . . . . . . . . . . . 19
               |
162 | | fconstmpt 4883 |
. . . . . . . . . . . . . . . . . . . . 21
       |
163 | | seqeq3 12256 |
. . . . . . . . . . . . . . . . . . . . 21
      
              |
164 | 162, 163 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
             |
165 | | 1z 10991 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
166 | | seqfn 12263 |
. . . . . . . . . . . . . . . . . . . . . 22
              |
167 | 165, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
            |
168 | | nnuz 11218 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
169 | 168 | fneq2i 5681 |
. . . . . . . . . . . . . . . . . . . . . 22
      
             |
170 | | dffn5 5924 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                     |
171 | 169, 170 | bitr3i 259 |
. . . . . . . . . . . . . . . . . . . . 21
                                |
172 | 167, 171 | mpbi 213 |
. . . . . . . . . . . . . . . . . . . 20
                    |
173 | 164, 172 | eqtr3i 2495 |
. . . . . . . . . . . . . . . . . . 19
                  |
174 | | fconstmpt 4883 |
. . . . . . . . . . . . . . . . . . 19
       |
175 | 161, 173,
174 | 3eqtr4i 2503 |
. . . . . . . . . . . . . . . . . 18
          |
176 | 175 | rneqi 5067 |
. . . . . . . . . . . . . . . . 17
          |
177 | | 1nn 10642 |
. . . . . . . . . . . . . . . . . 18
 |
178 | | ne0i 3728 |
. . . . . . . . . . . . . . . . . 18
   |
179 | | rnxp 5273 |
. . . . . . . . . . . . . . . . . 18

        |
180 | 177, 178,
179 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
       |
181 | 176, 180 | eqtri 2493 |
. . . . . . . . . . . . . . . 16
        |
182 | 181 | supeq1i 7979 |
. . . . . . . . . . . . . . 15
                |
183 | | xrltso 11463 |
. . . . . . . . . . . . . . . 16
 |
184 | | 0xr 9705 |
. . . . . . . . . . . . . . . 16
 |
185 | | supsn 8006 |
. . . . . . . . . . . . . . . 16
          |
186 | 183, 184,
185 | mp2an 686 |
. . . . . . . . . . . . . . 15
       |
187 | 182, 186 | eqtri 2493 |
. . . . . . . . . . . . . 14
          |
188 | 154, 187 | syl6eq 2521 |
. . . . . . . . . . . . 13
 
    
                         ..^              |
189 | 188 | adantl 473 |
. . . . . . . . . . . 12
                                    
 ..^           
  |
190 | 125, 134,
189 | 3eqtr3rd 2514 |
. . . . . . . . . . 11
                              |
191 | 190 | ex 441 |
. . . . . . . . . 10
                     
        |
192 | 39, 191 | sylbid 223 |
. . . . . . . . 9
             
        |
193 | 28, 192 | syl5 32 |
. . . . . . . 8
       

         |
194 | 193 | exlimiv 1784 |
. . . . . . 7
        
 
        |
195 | 18, 194 | syl 17 |
. . . . . 6
  
  
          |
196 | 195 | expimpd 614 |
. . . . 5

 
 
           |
197 | 11, 196 | pm2.61ine 2726 |
. . . 4
 
 
          |
198 | | renepnf 9706 |
. . . . . . 7
   |
199 | 48, 198 | mp1i 13 |
. . . . . 6
 
  |
200 | | fveq2 5879 |
. . . . . . 7
 
           |
201 | | rembl 22572 |
. . . . . . . . 9
 |
202 | | mblvol 22562 |
. . . . . . . . 9
            |
203 | 201, 202 | ax-mp 5 |
. . . . . . . 8
          |
204 | | ovolre 22557 |
. . . . . . . 8
      |
205 | 203, 204 | eqtri 2493 |
. . . . . . 7
     |
206 | 200, 205 | syl6eq 2521 |
. . . . . 6
 
       |
207 | 199, 206 | neeqtrrd 2717 |
. . . . 5
 
       |
208 | 207 | necon2i 2677 |
. . . 4
         |
209 | 197, 208 | syl 17 |
. . 3
 
 
   
  |
210 | 209 | expr 626 |
. 2
 

  
    |
211 | | eqimss 3470 |
. . 3
 

  |
212 | 211 | necon3bi 2669 |
. 2
     |
213 | 210, 212 | pm2.61d1 164 |
1
 

    |