Step | Hyp | Ref
| Expression |
1 | | uniioombl.1 |
. . 3
          |
2 | | ssid 3462 |
. . 3
       |
3 | | uniioombl.3 |
. . . 4
   
   |
4 | 3 | ovollb 22480 |
. . 3
           
                  |
5 | 1, 2, 4 | sylancl 673 |
. 2
               |
6 | 1 | adantr 471 |
. . . . . . . . . . 11
 

   
     |
7 | | elfznn 11856 |
. . . . . . . . . . 11
       |
8 | | eqid 2461 |
. . . . . . . . . . . 12
    
  |
9 | 8 | ovolfsval 22471 |
. . . . . . . . . . 11
            
                        |
10 | 6, 7, 9 | syl2an 484 |
. . . . . . . . . 10
           
                        |
11 | | fvco3 5964 |
. . . . . . . . . . . . . . 15
           
              |
12 | 6, 7, 11 | syl2an 484 |
. . . . . . . . . . . . . 14
          
              |
13 | | inss2 3664 |
. . . . . . . . . . . . . . . . . 18
      |
14 | | ffvelrn 6042 |
. . . . . . . . . . . . . . . . . . 19
             
     |
15 | 6, 7, 14 | syl2an 484 |
. . . . . . . . . . . . . . . . . 18
            
     |
16 | 13, 15 | sseldi 3441 |
. . . . . . . . . . . . . . . . 17
                 |
17 | | 1st2nd2 6856 |
. . . . . . . . . . . . . . . . 17
      
                         |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
                                  |
19 | 18 | fveq2d 5891 |
. . . . . . . . . . . . . . 15
                                          |
20 | | df-ov 6317 |
. . . . . . . . . . . . . . 15
                                            |
21 | 19, 20 | syl6eqr 2513 |
. . . . . . . . . . . . . 14
                                       |
22 | 12, 21 | eqtrd 2495 |
. . . . . . . . . . . . 13
          
                          |
23 | | ioombl 22566 |
. . . . . . . . . . . . 13
                     |
24 | 22, 23 | syl6eqel 2547 |
. . . . . . . . . . . 12
          
      |
25 | | mblvol 22532 |
. . . . . . . . . . . 12
      
               
       |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
                                |
27 | 22 | fveq2d 5891 |
. . . . . . . . . . 11
                                               |
28 | | ovolfcl 22467 |
. . . . . . . . . . . . 13
                                              |
29 | 6, 7, 28 | syl2an 484 |
. . . . . . . . . . . 12
                                             |
30 | | ovolioo 22569 |
. . . . . . . . . . . 12
                                                                                |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
                                                      |
32 | 26, 27, 31 | 3eqtrd 2499 |
. . . . . . . . . 10
                                       |
33 | 10, 32 | eqtr4d 2498 |
. . . . . . . . 9
           
        
       |
34 | | simpr 467 |
. . . . . . . . . 10
 

  |
35 | | nnuz 11222 |
. . . . . . . . . 10
     |
36 | 34, 35 | syl6eleq 2549 |
. . . . . . . . 9
 

      |
37 | 29 | simp2d 1027 |
. . . . . . . . . . . 12
                   |
38 | 29 | simp1d 1026 |
. . . . . . . . . . . 12
                   |
39 | 37, 38 | resubcld 10074 |
. . . . . . . . . . 11
                             |
40 | 32, 39 | eqeltrd 2539 |
. . . . . . . . . 10
                     |
41 | 40 | recnd 9694 |
. . . . . . . . 9
                     |
42 | 33, 36, 41 | fsumser 13844 |
. . . . . . . 8
 

          
        
       |
43 | 3 | fveq1i 5888 |
. . . . . . . 8
              |
44 | 42, 43 | syl6reqr 2514 |
. . . . . . 7
 

    
                 |
45 | | fzfid 12217 |
. . . . . . . 8
 

      |
46 | 24, 40 | jca 539 |
. . . . . . . . 9
                    
        |
47 | 46 | ralrimiva 2813 |
. . . . . . . 8
 

                          |
48 | 7 | ssriv 3447 |
. . . . . . . . 9
     |
49 | | uniioombl.2 |
. . . . . . . . . . 11
 Disj
          |
50 | 1, 11 | sylan 478 |
. . . . . . . . . . . 12
 

                |
51 | 50 | disjeq2dv 4391 |
. . . . . . . . . . 11
 Disj
      Disj            |
52 | 49, 51 | mpbird 240 |
. . . . . . . . . 10
 Disj
 
      |
53 | 52 | adantr 471 |
. . . . . . . . 9
 

Disj
        |
54 | | disjss1 4392 |
. . . . . . . . 9
    
Disj       Disj               |
55 | 48, 53, 54 | mpsyl 65 |
. . . . . . . 8
 

Disj
             |
56 | | volfiniun 22548 |
. . . . . . . 8
                       
      Disj            
                                  |
57 | 45, 47, 55, 56 | syl3anc 1276 |
. . . . . . 7
 

                                  |
58 | 24 | ralrimiva 2813 |
. . . . . . . . 9
 

              |
59 | | finiunmbl 22545 |
. . . . . . . . 9
                   
             |
60 | 45, 58, 59 | syl2anc 671 |
. . . . . . . 8
 

              |
61 | | mblvol 22532 |
. . . . . . . 8
 
          
                                   |
62 | 60, 61 | syl 17 |
. . . . . . 7
 

                                   |
63 | 44, 57, 62 | 3eqtr2d 2501 |
. . . . . 6
 

                       |
64 | | iunss1 4303 |
. . . . . . . . 9
    
                     |
65 | 48, 64 | mp1i 13 |
. . . . . . . 8
 

                     |
66 | | ioof 11760 |
. . . . . . . . . . 11
  
     |
67 | | rexpssxrxp 9710 |
. . . . . . . . . . . . 13
     |
68 | 13, 67 | sstri 3452 |
. . . . . . . . . . . 12
      |
69 | | fss 5759 |
. . . . . . . . . . . 12
                       |
70 | 1, 68, 69 | sylancl 673 |
. . . . . . . . . . 11
         |
71 | | fco 5761 |
. . . . . . . . . . 11
                
        |
72 | 66, 70, 71 | sylancr 674 |
. . . . . . . . . 10
          |
73 | 72 | adantr 471 |
. . . . . . . . 9
 

         |
74 | | ffn 5750 |
. . . . . . . . 9
            |
75 | | fniunfv 6176 |
. . . . . . . . 9
               |
76 | 73, 74, 75 | 3syl 18 |
. . . . . . . 8
 

            |
77 | 65, 76 | sseqtrd 3479 |
. . . . . . 7
 

                 |
78 | | frn 5757 |
. . . . . . . . . 10
             |
79 | 72, 78 | syl 17 |
. . . . . . . . 9
      |
80 | | sspwuni 4380 |
. . . . . . . . 9
  
      |
81 | 79, 80 | sylib 201 |
. . . . . . . 8
      |
82 | 81 | adantr 471 |
. . . . . . 7
 

     |
83 | | ovolss 22486 |
. . . . . . 7
             
                                  |
84 | 77, 82, 83 | syl2anc 671 |
. . . . . 6
 

                           |
85 | 63, 84 | eqbrtrd 4436 |
. . . . 5
 

              |
86 | 85 | ralrimiva 2813 |
. . . 4
                |
87 | 8, 3 | ovolsf 22473 |
. . . . . 6
                 |
88 | 1, 87 | syl 17 |
. . . . 5
          |
89 | | ffn 5750 |
. . . . 5
       
  |
90 | | breq1 4418 |
. . . . . 6
     
           
           |
91 | 90 | ralrn 6047 |
. . . . 5
  
        
               |
92 | 88, 89, 91 | 3syl 18 |
. . . 4
  
       
                |
93 | 86, 92 | mpbird 240 |
. . 3
 
          |
94 | | frn 5757 |
. . . . . 6
       
     |
95 | 1, 87, 94 | 3syl 18 |
. . . . 5
  
   |
96 | | icossxr 11747 |
. . . . 5
    |
97 | 95, 96 | syl6ss 3455 |
. . . 4
   |
98 | | ovolcl 22479 |
. . . . 5
   
          |
99 | 81, 98 | syl 17 |
. . . 4
           |
100 | | supxrleub 11640 |
. . . 4
                        
           |
101 | 97, 99, 100 | syl2anc 671 |
. . 3
              
           |
102 | 93, 101 | mpbird 240 |
. 2
               |
103 | | supxrcl 11628 |
. . . 4

      |
104 | 97, 103 | syl 17 |
. . 3
       |
105 | | xrletri3 11479 |
. . 3
         
                                               |
106 | 99, 104, 105 | syl2anc 671 |
. 2
                                           |
107 | 5, 102, 106 | mpbir2and 938 |
1
               |