Step | Hyp | Ref
| Expression |
1 | | voliunlem.3 |
. . . . 5
       |
2 | | frn 5747 |
. . . . 5
       |
3 | 1, 2 | syl 17 |
. . . 4
   |
4 | | mblss 22563 |
. . . . . 6
   |
5 | | selpw 3949 |
. . . . . 6
 
  |
6 | 4, 5 | sylibr 217 |
. . . . 5
    |
7 | 6 | ssriv 3422 |
. . . 4
  |
8 | 3, 7 | syl6ss 3430 |
. . 3
    |
9 | | sspwuni 4360 |
. . 3

 
  |
10 | 8, 9 | sylib 201 |
. 2
    |
11 | | elpwi 3951 |
. . . 4
    |
12 | | inundif 3836 |
. . . . . . . 8
         |
13 | 12 | fveq2i 5882 |
. . . . . . 7
     
             |
14 | | inss1 3643 |
. . . . . . . . 9
  
 |
15 | | simp2 1031 |
. . . . . . . . 9
 
        |
16 | 14, 15 | syl5ss 3429 |
. . . . . . . 8
 
           |
17 | | ovolsscl 22517 |
. . . . . . . . . 10
    
                |
18 | 14, 17 | mp3an1 1377 |
. . . . . . . . 9
 
          
     |
19 | 18 | 3adant1 1048 |
. . . . . . . 8
 
                |
20 | | difss 3549 |
. . . . . . . . 9
    |
21 | 20, 15 | syl5ss 3429 |
. . . . . . . 8
 
           |
22 | | ovolsscl 22517 |
. . . . . . . . . 10
    
                |
23 | 20, 22 | mp3an1 1377 |
. . . . . . . . 9
 
          
     |
24 | 23 | 3adant1 1048 |
. . . . . . . 8
 
                |
25 | | ovolun 22530 |
. . . . . . . 8
                       
                       
       
      |
26 | 16, 19, 21, 24, 25 | syl22anc 1293 |
. . . . . . 7
 
                                 
     |
27 | 13, 26 | syl5eqbrr 4430 |
. . . . . 6
 
                
       
      |
28 | 19 | rexrd 9708 |
. . . . . . . 8
 
                |
29 | | nnuz 11218 |
. . . . . . . . . . . 12
     |
30 | | 1zzd 10992 |
. . . . . . . . . . . 12
 
        |
31 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
           |
32 | 31 | ineq2d 3625 |
. . . . . . . . . . . . . . . 16
 
             |
33 | 32 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
                         |
34 | | voliunlem.6 |
. . . . . . . . . . . . . . 15
     
        |
35 | | fvex 5889 |
. . . . . . . . . . . . . . 15
            |
36 | 33, 34, 35 | fvmpt 5963 |
. . . . . . . . . . . . . 14
                  |
37 | 36 | adantl 473 |
. . . . . . . . . . . . 13
                           |
38 | | inss1 3643 |
. . . . . . . . . . . . . . . 16
       |
39 | | ovolsscl 22517 |
. . . . . . . . . . . . . . . 16
       
          
        |
40 | 38, 39 | mp3an1 1377 |
. . . . . . . . . . . . . . 15
 
          
        |
41 | 40 | 3adant1 1048 |
. . . . . . . . . . . . . 14
 
                   |
42 | 41 | adantr 472 |
. . . . . . . . . . . . 13
                       |
43 | 37, 42 | eqeltrd 2549 |
. . . . . . . . . . . 12
                |
44 | 29, 30, 43 | serfre 12280 |
. . . . . . . . . . 11
 
               |
45 | | frn 5747 |
. . . . . . . . . . 11
      
  
  |
46 | 44, 45 | syl 17 |
. . . . . . . . . 10
 
     
  
  |
47 | | ressxr 9702 |
. . . . . . . . . 10
 |
48 | 46, 47 | syl6ss 3430 |
. . . . . . . . 9
 
     
  
  |
49 | | supxrcl 11625 |
. . . . . . . . 9
             |
50 | 48, 49 | syl 17 |
. . . . . . . 8
 
               |
51 | | simp3 1032 |
. . . . . . . . . 10
 
             |
52 | 51, 24 | resubcld 10068 |
. . . . . . . . 9
 
                       |
53 | 52 | rexrd 9708 |
. . . . . . . 8
 
                       |
54 | | iunin2 4333 |
. . . . . . . . . . 11
               |
55 | | ffn 5739 |
. . . . . . . . . . . . . 14
       |
56 | | fniunfv 6170 |
. . . . . . . . . . . . . 14
         |
57 | 1, 55, 56 | 3syl 18 |
. . . . . . . . . . . . 13
         |
58 | 57 | 3ad2ant1 1051 |
. . . . . . . . . . . 12
 
              |
59 | 58 | ineq2d 3625 |
. . . . . . . . . . 11
 
       
          |
60 | 54, 59 | syl5eq 2517 |
. . . . . . . . . 10
 
       
          |
61 | 60 | fveq2d 5883 |
. . . . . . . . 9
 
           
          
     |
62 | | eqid 2471 |
. . . . . . . . . 10
       |
63 | | inss1 3643 |
. . . . . . . . . . . 12
       |
64 | 63, 15 | syl5ss 3429 |
. . . . . . . . . . 11
 
              |
65 | 64 | adantr 472 |
. . . . . . . . . 10
          
       |
66 | | ovolsscl 22517 |
. . . . . . . . . . . . 13
       
          
        |
67 | 63, 66 | mp3an1 1377 |
. . . . . . . . . . . 12
 
          
        |
68 | 67 | 3adant1 1048 |
. . . . . . . . . . 11
 
                   |
69 | 68 | adantr 472 |
. . . . . . . . . 10
                       |
70 | 62, 34, 65, 69 | ovoliun 22536 |
. . . . . . . . 9
 
           
               |
71 | 61, 70 | eqbrtrrd 4418 |
. . . . . . . 8
 
                       |
72 | 1 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
 
            |
73 | | voliunlem.5 |
. . . . . . . . . . . . . 14
 Disj
      |
74 | 73 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
 
      Disj       |
75 | 72, 74, 34, 15, 51 | voliunlem1 22582 |
. . . . . . . . . . . 12
                     
           |
76 | 44 | ffvelrnda 6037 |
. . . . . . . . . . . . 13
                  |
77 | 24 | adantr 472 |
. . . . . . . . . . . . 13
                    |
78 | | simpl3 1035 |
. . . . . . . . . . . . 13
                 |
79 | | leaddsub 10111 |
. . . . . . . . . . . . 13
             
                    
        
     
                  |
80 | 76, 77, 78, 79 | syl3anc 1292 |
. . . . . . . . . . . 12
                               
     
                  |
81 | 75, 80 | mpbid 215 |
. . . . . . . . . . 11
               
                 |
82 | 81 | ralrimiva 2809 |
. . . . . . . . . 10
 
                              |
83 | | ffn 5739 |
. . . . . . . . . . 11
            |
84 | | breq1 4398 |
. . . . . . . . . . . 12
                      
     
                  |
85 | 84 | ralrn 6040 |
. . . . . . . . . . 11
                        
                        |
86 | 44, 83, 85 | 3syl 18 |
. . . . . . . . . 10
 
           
               
                        |
87 | 82, 86 | mpbird 240 |
. . . . . . . . 9
 
                            |
88 | | supxrleub 11637 |
. . . . . . . . . 10
                
           
              
    
                  |
89 | 48, 53, 88 | syl2anc 673 |
. . . . . . . . 9
 
             
              
    
                  |
90 | 87, 89 | mpbird 240 |
. . . . . . . 8
 
                              |
91 | 28, 50, 53, 71, 90 | xrletrd 11482 |
. . . . . . 7
 
                               |
92 | | leaddsub 10111 |
. . . . . . . 8
      
       
               
       
        
                          |
93 | 19, 24, 51, 92 | syl3anc 1292 |
. . . . . . 7
 
            
       
        
                          |
94 | 91, 93 | mpbird 240 |
. . . . . 6
 
                    
          |
95 | 19, 24 | readdcld 9688 |
. . . . . . 7
 
                    
     |
96 | 51, 95 | letri3d 9794 |
. . . . . 6
 
                          
  
                    
        
       
             |
97 | 27, 94, 96 | mpbir2and 936 |
. . . . 5
 
                
       
      |
98 | 97 | 3expia 1233 |
. . . 4
 
      
                  
       |
99 | 11, 98 | sylan2 482 |
. . 3
 
                  
       
       |
100 | 99 | ralrimiva 2809 |
. 2
                   
       
       |
101 | | ismbl 22558 |
. 2
                      
       
        |
102 | 10, 100, 101 | sylanbrc 677 |
1
    |