Step | Hyp | Ref
| Expression |
1 | | ovncvrrp.x |
. . . 4
   |
2 | | ovncvrrp.n0 |
. . . 4
   |
3 | | ovncvrrp.a |
. . . 4

    |
4 | | ovncvrrp.e |
. . . 4
   |
5 | | eqid 2471 |
. . . 4


         
 
       
Σ^                     
          
 
       
Σ^                      |
6 | 1, 2, 3, 4, 5 | ovnlerp 38502 |
. . 3
   
         
 
       
Σ^                     
  voln*           |
7 | | simp1 1030 |
. . . . . 6
 
 
         
 
       
Σ^                       voln*            |
8 | | simp3 1032 |
. . . . . 6
 
 
         
 
       
Σ^                       voln*            voln*           |
9 | | rabid 2953 |
. . . . . . . . . 10
 
          
 
       
Σ^                          
   
           
Σ^                       |
10 | 9 | biimpi 199 |
. . . . . . . . 9
 
          
 
       
Σ^                     
          
 
       
Σ^                       |
11 | 10 | simprd 470 |
. . . . . . . 8
 
          
 
       
Σ^                         
   
           
Σ^                      |
12 | 11 | adantr 472 |
. . . . . . 7
  

         
 
       
Σ^                       voln*                    
 
       
Σ^                      |
13 | 12 | 3adant1 1048 |
. . . . . 6
 
 
         
 
       
Σ^                       voln*                    
 
       
Σ^                      |
14 | | nfv 1769 |
. . . . . . . 8
     voln*           |
15 | | nfe1 1935 |
. . . . . . . 8
         Σ^              voln*           |
16 | | simp1l 1054 |
. . . . . . . . . . . 12
     voln*                  
 
       
Σ^                       |
17 | | simp2 1031 |
. . . . . . . . . . . 12
     voln*                  
 
       
Σ^                        
    |
18 | | simp3l 1058 |
. . . . . . . . . . . 12
     voln*                  
 
       
Σ^                                   |
19 | | id 22 |
. . . . . . . . . . . . . . 15
       
 
 
        
                      |
20 | | fveq1 5878 |
. . . . . . . . . . . . . . . . . . . . 21
           |
21 | 20 | coeq2d 5002 |
. . . . . . . . . . . . . . . . . . . 20
               |
22 | 21 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . 19
  
                    |
23 | 22 | ixpeq2dv 7556 |
. . . . . . . . . . . . . . . . . 18
 
          
 
          |
24 | 23 | iuneq2d 4296 |
. . . . . . . . . . . . . . . . 17
                           |
25 | 24 | sseq2d 3446 |
. . . . . . . . . . . . . . . 16
             
               |
26 | 25 | elrab 3184 |
. . . . . . . . . . . . . . 15
       
            
                      |
27 | 19, 26 | sylibr 217 |
. . . . . . . . . . . . . 14
       
 
 
        
      
               |
28 | 27 | 3adant1 1048 |
. . . . . . . . . . . . 13
 
                       
 
               |
29 | | ovncvrrp.c |
. . . . . . . . . . . . . . . . 17
  
     
 
               |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . 16
           
                |
31 | | sseq1 3439 |
. . . . . . . . . . . . . . . . . 18
 
           
               |
32 | 31 | rabbidv 3022 |
. . . . . . . . . . . . . . . . 17
       
            
      
               |
33 | 32 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
       
            
      
               |
34 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . 20
   |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
     |
36 | 35, 3 | ssexd 4543 |
. . . . . . . . . . . . . . . . . 18
   |
37 | | elpwg 3950 |
. . . . . . . . . . . . . . . . . 18
 
  
     |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
   

     |
39 | 3, 38 | mpbird 240 |
. . . . . . . . . . . . . . . 16
      |
40 | | ovex 6336 |
. . . . . . . . . . . . . . . . . 18
     
 |
41 | 40 | rabex 4550 |
. . . . . . . . . . . . . . . . 17
      
            
 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . 16
     
 
               |
43 | 30, 33, 39, 42 | fvmptd 5969 |
. . . . . . . . . . . . . . 15
           
               |
44 | 43 | eqcomd 2477 |
. . . . . . . . . . . . . 14
     
 
                   |
45 | 44 | 3ad2ant1 1051 |
. . . . . . . . . . . . 13
 
                         
            
      |
46 | 28, 45 | eleqtrd 2551 |
. . . . . . . . . . . 12
 
                         |
47 | 16, 17, 18, 46 | syl3anc 1292 |
. . . . . . . . . . 11
     voln*                  
 
       
Σ^                           |
48 | | ovncvrrp.l |
. . . . . . . . . . . . . . . . . . . . 21
                  |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
       
    
               |
50 | | coeq2 4998 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
51 | 50 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                |
52 | 51 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
           |
53 | 52 | prodeq2ad 37769 |
. . . . . . . . . . . . . . . . . . . . 21
                                 |
54 | 53 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
      
 

    
     
     
                |
55 | | elmapi 7511 |
. . . . . . . . . . . . . . . . . . . . . 22
      
          |
56 | 55 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
       
           |
57 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . 21
       
   |
58 | 56, 57 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . 20
       
       
   |
59 | | prodex 14038 |
. . . . . . . . . . . . . . . . . . . . 21

               |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
       
                  |
61 | 49, 54, 58, 60 | fvmptd 5969 |
. . . . . . . . . . . . . . . . . . 19
       
         
                |
62 | 61 | mpteq2dva 4482 |
. . . . . . . . . . . . . . . . . 18
      
                             |
63 | 62 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
      
Σ^            Σ^                     |
64 | 63 | adantr 472 |
. . . . . . . . . . . . . . . 16
       
Σ^                    Σ^            Σ^                     |
65 | | id 22 |
. . . . . . . . . . . . . . . . . 18
 Σ^                   Σ^                     |
66 | 65 | eqcomd 2477 |
. . . . . . . . . . . . . . . . 17
 Σ^                   Σ^                     |
67 | 66 | adantl 473 |
. . . . . . . . . . . . . . . 16
       
Σ^                    Σ^                     |
68 | 64, 67 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
       
Σ^                    Σ^              |
69 | 68 | 3adant1 1048 |
. . . . . . . . . . . . . 14
 
  voln*               Σ^                    Σ^              |
70 | | simp1 1030 |
. . . . . . . . . . . . . 14
 
  voln*               Σ^                   
  voln*           |
71 | 69, 70 | eqbrtrd 4416 |
. . . . . . . . . . . . 13
 
  voln*               Σ^                    Σ^              voln*           |
72 | 71 | 3adant1l 1284 |
. . . . . . . . . . . 12
     voln*                Σ^                    Σ^              voln*           |
73 | 72 | 3adant3l 1288 |
. . . . . . . . . . 11
     voln*                  
 
       
Σ^                     Σ^              voln*           |
74 | 47, 73 | jca 541 |
. . . . . . . . . 10
     voln*                  
 
       
Σ^                         
Σ^              voln*            |
75 | | 19.8a 1955 |
. . . . . . . . . 10
      Σ^              voln*                 Σ^              voln*            |
76 | 74, 75 | syl 17 |
. . . . . . . . 9
     voln*                  
 
       
Σ^                            Σ^              voln*            |
77 | 76 | 3exp 1230 |
. . . . . . . 8
 
  voln*                
 
           
Σ^                          
Σ^              voln*              |
78 | 14, 15, 77 | rexlimd 2866 |
. . . . . . 7
 
  voln*           
   
   
           
Σ^                          
Σ^              voln*             |
79 | 78 | imp 436 |
. . . . . 6
     voln*          
         
 
       
Σ^                            Σ^              voln*            |
80 | 7, 8, 13, 79 | syl21anc 1291 |
. . . . 5
 
 
         
 
       
Σ^                       voln*                 Σ^              voln*            |
81 | 80 | 3exp 1230 |
. . . 4
   
         
 
       
Σ^                        voln*        
       Σ^              voln*              |
82 | 81 | rexlimdv 2870 |
. . 3
        
   
           
Σ^                     
  voln*        
       Σ^              voln*             |
83 | 6, 82 | mpd 15 |
. 2
        Σ^              voln*            |
84 | | rabid 2953 |
. . . . . . . 8
      Σ^              voln*         
    
Σ^              voln*            |
85 | 84 | bicomi 207 |
. . . . . . 7
      Σ^              voln*         
     Σ^              voln*            |
86 | 85 | biimpi 199 |
. . . . . 6
      Σ^              voln*               Σ^              voln*            |
87 | 86 | adantl 473 |
. . . . 5
 
    
Σ^              voln*                Σ^              voln*            |
88 | | ovncvrrp.d |
. . . . . . . . . 10
  
       Σ^              voln*             |
89 | | nfcv 2612 |
. . . . . . . . . . 11
        Σ^              voln*            |
90 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
91 | | nfv 1769 |
. . . . . . . . . . . . 13
  Σ^              voln*          |
92 | | nfmpt1 4485 |
. . . . . . . . . . . . . . 15
    
     
 
               |
93 | 29, 92 | nfcxfr 2610 |
. . . . . . . . . . . . . 14
   |
94 | | nfcv 2612 |
. . . . . . . . . . . . . 14
   |
95 | 93, 94 | nffv 5886 |
. . . . . . . . . . . . 13
       |
96 | 91, 95 | nfrab 2958 |
. . . . . . . . . . . 12
       Σ^              voln*           |
97 | 90, 96 | nfmpt 4484 |
. . . . . . . . . . 11
        Σ^              voln*            |
98 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
99 | 98 | eleq2d 2534 |
. . . . . . . . . . . . . 14
     
       |
100 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
  voln*      voln*       |
101 | 100 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
   voln*           voln*           |
102 | 101 | breq2d 4407 |
. . . . . . . . . . . . . 14
  Σ^              voln*         Σ^              voln*            |
103 | 99, 102 | anbi12d 725 |
. . . . . . . . . . . . 13
       Σ^              voln*         
    
Σ^              voln*             |
104 | 103 | rabbidva2 3020 |
. . . . . . . . . . . 12
      Σ^              voln*               Σ^              voln*            |
105 | 104 | mpteq2dv 4483 |
. . . . . . . . . . 11
       Σ^              voln*                 Σ^              voln*             |
106 | 89, 97, 105 | cbvmpt 4487 |
. . . . . . . . . 10
          Σ^              voln*                
     Σ^              voln*             |
107 | 88, 106 | eqtri 2493 |
. . . . . . . . 9
  
       Σ^              voln*             |
108 | 107 | a1i 11 |
. . . . . . . 8
 
    
Σ^              voln*          
    
     Σ^              voln*              |
109 | | fveq2 5879 |
. . . . . . . . . . . . 13
           |
110 | 109 | eleq2d 2534 |
. . . . . . . . . . . 12
     
       |
111 | | fveq2 5879 |
. . . . . . . . . . . . . 14
  voln*      voln*       |
112 | 111 | oveq1d 6323 |
. . . . . . . . . . . . 13
   voln*           voln*           |
113 | 112 | breq2d 4407 |
. . . . . . . . . . . 12
  Σ^              voln*         Σ^              voln*            |
114 | 110, 113 | anbi12d 725 |
. . . . . . . . . . 11
       Σ^              voln*         
    
Σ^              voln*             |
115 | 114 | rabbidva2 3020 |
. . . . . . . . . 10
      Σ^              voln*               Σ^              voln*            |
116 | 115 | mpteq2dv 4483 |
. . . . . . . . 9
       Σ^              voln*                 Σ^              voln*             |
117 | 116 | adantl 473 |
. . . . . . . 8
        Σ^              voln*          
       Σ^              voln*                 Σ^              voln*             |
118 | 39 | adantr 472 |
. . . . . . . 8
 
    
Σ^              voln*          
     |
119 | | rpex 37656 |
. . . . . . . . . 10
 |
120 | 119 | mptex 6152 |
. . . . . . . . 9

     Σ^              voln*            |
121 | 120 | a1i 11 |
. . . . . . . 8
 
    
Σ^              voln*                 Σ^              voln*             |
122 | 108, 117,
118, 121 | fvmptd 5969 |
. . . . . . 7
 
    
Σ^              voln*               
     Σ^              voln*             |
123 | | oveq2 6316 |
. . . . . . . . . 10
   voln*           voln*           |
124 | 123 | breq2d 4407 |
. . . . . . . . 9
  Σ^              voln*         Σ^              voln*            |
125 | 124 | rabbidv 3022 |
. . . . . . . 8
      Σ^              voln*               Σ^              voln*            |
126 | 125 | adantl 473 |
. . . . . . 7
        Σ^              voln*          
      Σ^              voln*               Σ^              voln*            |
127 | 4 | adantr 472 |
. . . . . . 7
 
    
Σ^              voln*          
  |
128 | | fvex 5889 |
. . . . . . . . 9
     |
129 | 128 | rabex 4550 |
. . . . . . . 8
     Σ^              voln*           |
130 | 129 | a1i 11 |
. . . . . . 7
 
    
Σ^              voln*                Σ^              voln*            |
131 | 122, 126,
127, 130 | fvmptd 5969 |
. . . . . 6
 
    
Σ^              voln*                        Σ^              voln*            |
132 | 131 | eqcomd 2477 |
. . . . 5
 
    
Σ^              voln*                Σ^              voln*                    |
133 | 87, 132 | eleqtrd 2551 |
. . . 4
 
    
Σ^              voln*                     |
134 | 133 | ex 441 |
. . 3
      
Σ^              voln*                     |
135 | 134 | eximdv 1772 |
. 2
         Σ^              voln*                      |
136 | 83, 135 | mpd 15 |
1
            |