Step | Hyp | Ref
| Expression |
1 | | nnuz 11218 |
. . 3
     |
2 | | eqid 2471 |
. . 3
   
             |
3 | | 1zzd 10992 |
. . 3
 

  |
4 | | eqidd 2472 |
. . 3
       

                |
5 | | uniioombl.1 |
. . . . . . . . . . 11
          |
6 | | uniioombl.2 |
. . . . . . . . . . 11
 Disj
          |
7 | | uniioombl.3 |
. . . . . . . . . . 11
   
   |
8 | | uniioombl.a |
. . . . . . . . . . 11

   |
9 | | uniioombl.e |
. . . . . . . . . . 11
        |
10 | | uniioombl.c |
. . . . . . . . . . 11
   |
11 | | uniioombl.g |
. . . . . . . . . . 11
          |
12 | | uniioombl.s |
. . . . . . . . . . 11

     |
13 | | uniioombl.t |
. . . . . . . . . . 11
   
   |
14 | | uniioombl.v |
. . . . . . . . . . 11
              |
15 | 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | uniioombllem2a 22618 |
. . . . . . . . . 10
             
           |
16 | | inss2 3644 |
. . . . . . . . . . . . 13
                           |
17 | 16 | a1i 11 |
. . . . . . . . . . . 12
 

                            |
18 | | inss2 3644 |
. . . . . . . . . . . . . . . . 17
      |
19 | 11 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . 17
 

   
     |
20 | 18, 19 | sseldi 3416 |
. . . . . . . . . . . . . . . 16
 

        |
21 | | 1st2nd2 6849 |
. . . . . . . . . . . . . . . 16
      
                         |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . 15
 

                         |
23 | 22 | fveq2d 5883 |
. . . . . . . . . . . . . 14
 

                                 |
24 | | df-ov 6311 |
. . . . . . . . . . . . . 14
                                            |
25 | 23, 24 | syl6eqr 2523 |
. . . . . . . . . . . . 13
 

                              |
26 | | ioossre 11721 |
. . . . . . . . . . . . 13
                     |
27 | 25, 26 | syl6eqss 3468 |
. . . . . . . . . . . 12
 

          |
28 | 25 | fveq2d 5883 |
. . . . . . . . . . . . . 14
 

                                        |
29 | | ovolfcl 22497 |
. . . . . . . . . . . . . . . 16
                                              |
30 | 11, 29 | sylan 479 |
. . . . . . . . . . . . . . 15
 

                                    |
31 | | ovolioo 22600 |
. . . . . . . . . . . . . . 15
                                                                                |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . 14
 

                                             |
33 | 28, 32 | eqtrd 2505 |
. . . . . . . . . . . . 13
 

                                 |
34 | 30 | simp2d 1043 |
. . . . . . . . . . . . . 14
 

          |
35 | 30 | simp1d 1042 |
. . . . . . . . . . . . . 14
 

          |
36 | 34, 35 | resubcld 10068 |
. . . . . . . . . . . . 13
 

                    |
37 | 33, 36 | eqeltrd 2549 |
. . . . . . . . . . . 12
 

               |
38 | | ovolsscl 22517 |
. . . . . . . . . . . 12
          
                        
                                       |
39 | 17, 27, 37, 38 | syl3anc 1292 |
. . . . . . . . . . 11
 

                         |
40 | 39 | adantr 472 |
. . . . . . . . . 10
                              |
41 | | uniioombllem2.k |
. . . . . . . . . . 11
       
inf       
    |
42 | 41 | ioorcl 22608 |
. . . . . . . . . 10
          
                                                      
     |
43 | 15, 40, 42 | syl2anc 673 |
. . . . . . . . 9
                          
     |
44 | | eqid 2471 |
. . . . . . . . 9
                                                 |
45 | 43, 44 | fmptd 6061 |
. . . . . . . 8
 

                           
     |
46 | | uniioombllem2.h |
. . . . . . . . . . 11
         
           |
47 | 46 | a1i 11 |
. . . . . . . . . 10
 

         
            |
48 | 41 | ioorf 22604 |
. . . . . . . . . . . 12
        |
49 | 48 | a1i 11 |
. . . . . . . . . . 11
 

         |
50 | 49 | feqmptd 5932 |
. . . . . . . . . 10
 

        |
51 | | fveq2 5879 |
. . . . . . . . . 10
                                               |
52 | 15, 47, 50, 51 | fmptco 6072 |
. . . . . . . . 9
 

                            |
53 | 52 | feq1d 5724 |
. . . . . . . 8
 

         
            
                     |
54 | 45, 53 | mpbird 240 |
. . . . . . 7
 

      
    |
55 | | eqid 2471 |
. . . . . . . 8
      
    |
56 | 55 | ovolfsf 22502 |
. . . . . . 7
           
            |
57 | 54, 56 | syl 17 |
. . . . . 6
 

              |
58 | 57 | ffvelrnda 6037 |
. . . . 5
       

          |
59 | | elrege0 11764 |
. . . . 5
   

                              |
60 | 58, 59 | sylib 201 |
. . . 4
        

                 |
61 | 60 | simpld 466 |
. . 3
       

       |
62 | 60 | simprd 470 |
. . 3
       

       |
63 | 52 | fveq1d 5881 |
. . . . . . . . . . . . . . 15
 

                   
                |
64 | | fvex 5889 |
. . . . . . . . . . . . . . . 16
                       |
65 | 44 | fvmpt2 5972 |
. . . . . . . . . . . . . . . 16
                                                                
            |
66 | 64, 65 | mpan2 685 |
. . . . . . . . . . . . . . 15
                                        
            |
67 | 63, 66 | sylan9eq 2525 |
. . . . . . . . . . . . . 14
                      
            |
68 | 67 | fveq2d 5883 |
. . . . . . . . . . . . 13
                                           |
69 | 41 | ioorinv 22607 |
. . . . . . . . . . . . . 14
         
        
              
                               |
70 | 15, 69 | syl 17 |
. . . . . . . . . . . . 13
                   
                               |
71 | 68, 70 | eqtrd 2505 |
. . . . . . . . . . . 12
                       
           |
72 | 71 | ralrimiva 2809 |
. . . . . . . . . . 11
 

                               |
73 | | fveq2 5879 |
. . . . . . . . . . . . . 14
               |
74 | 73 | fveq2d 5883 |
. . . . . . . . . . . . 13
                       |
75 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
76 | 75 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                   |
77 | 76 | ineq1d 3624 |
. . . . . . . . . . . . 13
         
                 
           |
78 | 74, 77 | eqeq12d 2486 |
. . . . . . . . . . . 12
                             
                  
            |
79 | 78 | rspccva 3135 |
. . . . . . . . . . 11
                                                              |
80 | 72, 79 | sylan 479 |
. . . . . . . . . 10
                       
           |
81 | | inss1 3643 |
. . . . . . . . . 10
                           |
82 | 80, 81 | syl6eqss 3468 |
. . . . . . . . 9
                         |
83 | 82 | ralrimiva 2809 |
. . . . . . . 8
 

          
          |
84 | 6 | adantr 472 |
. . . . . . . 8
 

Disj
          |
85 | | disjss2 4369 |
. . . . . . . 8
 
                  Disj
        Disj              |
86 | 83, 84, 85 | sylc 61 |
. . . . . . 7
 

Disj
            |
87 | 54, 86, 2 | uniioovol 22615 |
. . . . . 6
 

               

    
  |
88 | 70 | mpteq2dva 4482 |
. . . . . . . . . . 11
 

               
                     
            |
89 | | rexpssxrxp 9703 |
. . . . . . . . . . . . . 14
     |
90 | 18, 89 | sstri 3427 |
. . . . . . . . . . . . 13
      |
91 | 90, 43 | sseldi 3416 |
. . . . . . . . . . . 12
                           
   |
92 | | ioof 11757 |
. . . . . . . . . . . . . 14
  
     |
93 | 92 | a1i 11 |
. . . . . . . . . . . . 13
 

  
      |
94 | 93 | feqmptd 5932 |
. . . . . . . . . . . 12
 

 
        |
95 | | fveq2 5879 |
. . . . . . . . . . . 12
            
                            
             |
96 | 91, 52, 94, 95 | fmptco 6072 |
. . . . . . . . . . 11
 

                                  |
97 | 88, 96, 47 | 3eqtr4d 2515 |
. . . . . . . . . 10
 

      |
98 | 97 | rneqd 5068 |
. . . . . . . . 9
 

      |
99 | 98 | unieqd 4200 |
. . . . . . . 8
 

        |
100 | | fvex 5889 |
. . . . . . . . . . . . . 14
         |
101 | 100 | inex1 4537 |
. . . . . . . . . . . . 13
                   |
102 | 46 | fvmpt2 5972 |
. . . . . . . . . . . . 13
          
                                  |
103 | 101, 102 | mpan2 685 |
. . . . . . . . . . . 12
                         |
104 | | incom 3616 |
. . . . . . . . . . . 12
                          
          |
105 | 103, 104 | syl6eq 2521 |
. . . . . . . . . . 11
                         |
106 | 105 | iuneq2i 4288 |
. . . . . . . . . 10
     
        
          |
107 | | iunin2 4333 |
. . . . . . . . . 10
                            
          |
108 | 106, 107 | eqtri 2493 |
. . . . . . . . 9
             
           |
109 | 15, 46 | fmptd 6061 |
. . . . . . . . . . 11
 

      |
110 | | ffn 5739 |
. . . . . . . . . . 11
       |
111 | 109, 110 | syl 17 |
. . . . . . . . . 10
 

  |
112 | | fniunfv 6170 |
. . . . . . . . . 10
         |
113 | 111, 112 | syl 17 |
. . . . . . . . 9
 

        |
114 | 108, 113 | syl5eqr 2519 |
. . . . . . . 8
 

                      |
115 | 5 | adantr 472 |
. . . . . . . . . . . 12
 

   
     |
116 | | fvco3 5957 |
. . . . . . . . . . . 12
           
              |
117 | 115, 116 | sylan 479 |
. . . . . . . . . . 11
      
              |
118 | 117 | iuneq2dv 4291 |
. . . . . . . . . 10
 

       
          |
119 | | ffn 5739 |
. . . . . . . . . . . . . 14
        
   |
120 | 92, 119 | ax-mp 5 |
. . . . . . . . . . . . 13
   |
121 | | fss 5749 |
. . . . . . . . . . . . . 14
                       |
122 | 115, 90, 121 | sylancl 675 |
. . . . . . . . . . . . 13
 

    
   |
123 | | fnfco 5760 |
. . . . . . . . . . . . 13
               |
124 | 120, 122,
123 | sylancr 676 |
. . . . . . . . . . . 12
 

    |
125 | | fniunfv 6170 |
. . . . . . . . . . . 12
               |
126 | 124, 125 | syl 17 |
. . . . . . . . . . 11
 

            |
127 | 126, 8 | syl6eqr 2523 |
. . . . . . . . . 10
 

         |
128 | 118, 127 | eqtr3d 2507 |
. . . . . . . . 9
 

           |
129 | 128 | ineq2d 3625 |
. . . . . . . 8
 

                               |
130 | 99, 114, 129 | 3eqtr2d 2511 |
. . . . . . 7
 

                 |
131 | 130 | fveq2d 5883 |
. . . . . 6
 

                      
    |
132 | 87, 131 | eqtr3d 2507 |
. . . . 5
 

     

    
            
    |
133 | | inss1 3643 |
. . . . . . 7
                   |
134 | 133 | a1i 11 |
. . . . . 6
 

                    |
135 | | ovolsscl 22517 |
. . . . . 6
          
        
                                  
    |
136 | 134, 27, 37, 135 | syl3anc 1292 |
. . . . 5
 

                 |
137 | 132, 136 | eqeltrd 2549 |
. . . 4
 

     

    
  |
138 | 55, 2 | ovolsf 22503 |
. . . . . . . . 9
             

            |
139 | 54, 138 | syl 17 |
. . . . . . . 8
 

   
             |
140 | | ffn 5739 |
. . . . . . . 8
   

             

     |
141 | 139, 140 | syl 17 |
. . . . . . 7
 

   
      |
142 | | fnfvelrn 6034 |
. . . . . . 7
    

       

         

     |
143 | 141, 142 | sylan 479 |
. . . . . 6
        

         

     |
144 | | frn 5747 |
. . . . . . . . 9
   

         
   
         |
145 | 139, 144 | syl 17 |
. . . . . . . 8
 

   

    
   |
146 | | icossxr 11744 |
. . . . . . . 8
    |
147 | 145, 146 | syl6ss 3430 |
. . . . . . 7
 

   

     |
148 | | supxrub 11635 |
. . . . . . 7
             
          

       
            
        |
149 | 147, 148 | sylan 479 |
. . . . . 6
       

         

       

                 
  |
150 | 143, 149 | syldan 478 |
. . . . 5
        

     
     

    
  |
151 | 150 | ralrimiva 2809 |
. . . 4
 

    
            
        |
152 | | breq2 4399 |
. . . . . 6
      

    
    
                             
   |
153 | 152 | ralbidv 2829 |
. . . . 5
      

    
     
           

                 
   |
154 | 153 | rspcev 3136 |
. . . 4
       

         

                 
      

     
  |
155 | 137, 151,
154 | syl2anc 673 |
. . 3
 

     
         |
156 | 1, 2, 3, 4, 61, 62, 155 | isumsup2 13981 |
. 2
 

   
         

       |
157 | 55 | ovolfs2 22602 |
. . . . 5
           
      

    |
158 | 54, 157 | syl 17 |
. . . 4
 

        

    |
159 | | coass 5361 |
. . . . 5
   
           |
160 | 97 | coeq2d 5002 |
. . . . 5
 

 
          |
161 | 159, 160 | syl5eq 2517 |
. . . 4
 

   
        |
162 | 158, 161 | eqtrd 2505 |
. . 3
 

          |
163 | 162 | seqeq3d 12259 |
. 2
 

   
       
    |
164 | | rge0ssre 11766 |
. . . . 5
    |
165 | 145, 164 | syl6ss 3430 |
. . . 4
 

   

     |
166 | | 1nn 10642 |
. . . . . . 7
 |
167 | | fdm 5745 |
. . . . . . . 8
   

         
   
      |
168 | 139, 167 | syl 17 |
. . . . . . 7
 

   

     |
169 | 166, 168 | syl5eleqr 2556 |
. . . . . 6
 

   

     |
170 | | ne0i 3728 |
. . . . . 6
    
   
   
      |
171 | 169, 170 | syl 17 |
. . . . 5
 

   

     |
172 | | dm0rn0 5057 |
. . . . . 6
    

             |
173 | 172 | necon3bii 2695 |
. . . . 5
    

             |
174 | 171, 173 | sylib 201 |
. . . 4
 

   

     |
175 | | breq1 4398 |
. . . . . . . 8
    
           

         |
176 | 175 | ralrn 6040 |
. . . . . . 7
   

        

   
    
          |
177 | 141, 176 | syl 17 |
. . . . . 6
 

 
   
    
    
          |
178 | 177 | rexbidv 2892 |
. . . . 5
 

  
   
    
     
          |
179 | 155, 178 | mpbird 240 |
. . . 4
 

     

      |
180 | | supxrre 11638 |
. . . 4
             
         

          
           

       |
181 | 165, 174,
179, 180 | syl3anc 1292 |
. . 3
 

     

    
     

       |
182 | 181, 132 | eqtr3d 2507 |
. 2
 

     

                 
    |
183 | 156, 163,
182 | 3brtr3d 4425 |
1
 

                       |