Step | Hyp | Ref
| Expression |
1 | | omssubadd.b |
. . . . . 6
   |
2 | | nnenom 12231 |
. . . . . . 7
 |
3 | 2 | ensymi 7637 |
. . . . . 6
 |
4 | | domentr 7646 |
. . . . . 6
 

  |
5 | 1, 3, 4 | sylancl 675 |
. . . . 5
   |
6 | | brdomi 7598 |
. . . . 5

       |
7 | 5, 6 | syl 17 |
. . . 4
        |
8 | 7 | adantr 472 |
. . 3
 
Σ*              |
9 | | simplll 776 |
. . . . . . . . . 10
    Σ*            
  |
10 | | ctex 7602 |
. . . . . . . . . . 11

  |
11 | 1, 10 | syl 17 |
. . . . . . . . . 10
   |
12 | 9, 11 | syl 17 |
. . . . . . . . 9
    Σ*            
  |
13 | | nfv 1769 |
. . . . . . . . . . . . 13
   |
14 | | nfcv 2612 |
. . . . . . . . . . . . . . 15
   |
15 | 14 | nfesum1 28935 |
. . . . . . . . . . . . . 14
 Σ*       |
16 | | nfcv 2612 |
. . . . . . . . . . . . . 14
   |
17 | 15, 16 | nfel 2624 |
. . . . . . . . . . . . 13
 Σ*       |
18 | 13, 17 | nfan 2031 |
. . . . . . . . . . . 12
  
Σ*        |
19 | | nfv 1769 |
. . . . . . . . . . . 12
      |
20 | 18, 19 | nfan 2031 |
. . . . . . . . . . 11
    Σ*             |
21 | | nfv 1769 |
. . . . . . . . . . 11
  |
22 | 20, 21 | nfan 2031 |
. . . . . . . . . 10
     Σ*              |
23 | 9 | adantr 472 |
. . . . . . . . . . . . . 14
     Σ*                |
24 | | simpr 468 |
. . . . . . . . . . . . . 14
     Σ*                |
25 | 11 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
Σ*         |
26 | | oms.o |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
27 | | oms.r |
. . . . . . . . . . . . . . . . . . . . . . . 24
          |
28 | | omsf 29193 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          toOMeas             |
29 | | oms.m |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
toOMeas   |
30 | 29 | feq1i 5730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          toOMeas             |
31 | 28, 30 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     |
32 | 26, 27, 31 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . 23
            |
33 | 32 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
 
            |
34 | | omssubadd.a |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    |
35 | | fdm 5745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          |
36 | 27, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
37 | 36 | unieqd 4200 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
38 | 37 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
39 | 34, 38 | sseqtr4d 3455 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
  |
40 | | uniexg 6607 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    |
41 | 26, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    |
42 | 41 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
    |
43 | | ssexg 4542 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     |
44 | 34, 42, 43 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
45 | | elpwg 3950 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 
    |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 
 
    |
47 | 39, 46 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     |
48 | 33, 47 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . 21
 
          |
49 | 48 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . 20
  
Σ*       
         |
50 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . 20
 
Σ*       Σ*        |
51 | 18, 25, 49, 50 | esumcvgre 28986 |
. . . . . . . . . . . . . . . . . . 19
  
Σ*       
      |
52 | 51 | adantlr 729 |
. . . . . . . . . . . . . . . . . 18
    Σ*                   |
53 | 52 | adantlr 729 |
. . . . . . . . . . . . . . . . 17
     Σ*                    |
54 | | rpssre 11335 |
. . . . . . . . . . . . . . . . . . 19
 |
55 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . 20
          
  |
56 | | 2rp 11330 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
58 | | df-f1 5594 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
         |
59 | 58 | simplbi 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
60 | 59 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
           |
61 | 60 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
62 | 61 | nnzd 11062 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
63 | 57, 62 | rpexpcld 12477 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
64 | 63 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . 20
          
          |
65 | 55, 64 | rpdivcld 11381 |
. . . . . . . . . . . . . . . . . . 19
          
            |
66 | 54, 65 | sseldi 3416 |
. . . . . . . . . . . . . . . . . 18
          
            |
67 | 66 | adantl3r 764 |
. . . . . . . . . . . . . . . . 17
     Σ*                          |
68 | | rexadd 11548 |
. . . . . . . . . . . . . . . . 17
                                                      |
69 | 53, 67, 68 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
     Σ*                                                   |
70 | 9, 48 | sylan 479 |
. . . . . . . . . . . . . . . . 17
     Σ*                       |
71 | | dfrp2 28427 |
. . . . . . . . . . . . . . . . . . . 20
    |
72 | | ioossicc 11745 |
. . . . . . . . . . . . . . . . . . . 20
       |
73 | 71, 72 | eqsstri 3448 |
. . . . . . . . . . . . . . . . . . 19
 
  |
74 | 73, 65 | sseldi 3416 |
. . . . . . . . . . . . . . . . . 18
          
               |
75 | 74 | adantl3r 764 |
. . . . . . . . . . . . . . . . 17
     Σ*                             |
76 | 70, 75 | xrge0addcld 28419 |
. . . . . . . . . . . . . . . 16
     Σ*                                      |
77 | 69, 76 | eqeltrrd 2550 |
. . . . . . . . . . . . . . 15
     Σ*                                   |
78 | 54, 55 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . 19
          
  |
79 | 78 | adantl3r 764 |
. . . . . . . . . . . . . . . . . 18
     Σ*                |
80 | 54, 63 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . 20
                   |
81 | 80 | adantlr 729 |
. . . . . . . . . . . . . . . . . . 19
          
          |
82 | 81 | adantl3r 764 |
. . . . . . . . . . . . . . . . . 18
     Σ*                        |
83 | | simplr 770 |
. . . . . . . . . . . . . . . . . . 19
     Σ*                |
84 | 83 | rpgt0d 11367 |
. . . . . . . . . . . . . . . . . 18
     Σ*                |
85 | | 2re 10701 |
. . . . . . . . . . . . . . . . . . . 20
 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
     Σ*                |
87 | 62 | adantllr 733 |
. . . . . . . . . . . . . . . . . . . 20
    Σ*                   |
88 | 87 | adantlr 729 |
. . . . . . . . . . . . . . . . . . 19
     Σ*                    |
89 | | 2pos 10723 |
. . . . . . . . . . . . . . . . . . . 20
 |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
     Σ*                |
91 | | expgt0 12343 |
. . . . . . . . . . . . . . . . . . 19
      
          |
92 | 86, 88, 90, 91 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
     Σ*                        |
93 | 79, 82, 84, 92 | divgt0d 10564 |
. . . . . . . . . . . . . . . . 17
     Σ*                          |
94 | 67, 53 | ltaddposd 10218 |
. . . . . . . . . . . . . . . . 17
     Σ*              
         
                       |
95 | 93, 94 | mpbid 215 |
. . . . . . . . . . . . . . . 16
     Σ*                                    |
96 | 29 | fveq1i 5880 |
. . . . . . . . . . . . . . . . . . . 20
     toOMeas      |
97 | 26 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
98 | 27 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
 
          |
99 | | omsfval 29191 |
. . . . . . . . . . . . . . . . . . . . 21
            toOMeas     inf   
 
  Σ*              |
100 | 97, 98, 34, 99 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . 20
 
  toOMeas     inf       
Σ*
             |
101 | 96, 100 | syl5eq 2517 |
. . . . . . . . . . . . . . . . . . 19
 
     inf   
 
  Σ*              |
102 | 9, 101 | sylan 479 |
. . . . . . . . . . . . . . . . . 18
     Σ*                  inf   
 
  Σ*              |
103 | 102 | eqcomd 2477 |
. . . . . . . . . . . . . . . . 17
     Σ*              inf       
Σ*
                 |
104 | 103 | breq1d 4405 |
. . . . . . . . . . . . . . . 16
     Σ*              inf       
Σ*
                              
                   |
105 | 95, 104 | mpbird 240 |
. . . . . . . . . . . . . . 15
     Σ*              inf       
Σ*
                             |
106 | 77, 105 | jca 541 |
. . . . . . . . . . . . . 14
     Σ*                                  inf       
Σ*
                              |
107 | | iccssxr 11742 |
. . . . . . . . . . . . . . . . . . 19
    |
108 | | xrltso 11463 |
. . . . . . . . . . . . . . . . . . 19
 |
109 | | soss 4778 |
. . . . . . . . . . . . . . . . . . 19
          |
110 | 107, 108,
109 | mp2 9 |
. . . . . . . . . . . . . . . . . 18
    |
111 | | biid 244 |
. . . . . . . . . . . . . . . . . 18
  
     |
112 | 110, 111 | mpbi 213 |
. . . . . . . . . . . . . . . . 17
    |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
      |
114 | | omscl 29192 |
. . . . . . . . . . . . . . . . . 18
        
  
  
 
  Σ*      
     |
115 | 97, 98, 47, 114 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
 
 
     
Σ*
       
   |
116 | | xrge0infss 28415 |
. . . . . . . . . . . . . . . . 17
       
Σ*
       
              
Σ*
           
       
Σ*
           |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . 16
 
              
Σ*
           
       
Σ*
           |
118 | 113, 117 | infglb 8024 |
. . . . . . . . . . . . . . 15
 
                      inf   
 
  Σ*                            
       
Σ*
                          |
119 | 118 | imp 436 |
. . . . . . . . . . . . . 14
                        inf       
Σ*
                                    
Σ*
                         |
120 | 23, 24, 106, 119 | syl21anc 1291 |
. . . . . . . . . . . . 13
     Σ*                     
Σ*
                         |
121 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . 19
  
 
  Σ*         
 
  Σ*        |
122 | | esumex 28924 |
. . . . . . . . . . . . . . . . . . 19
Σ*
      |
123 | 121, 122 | elrnmpti 5091 |
. . . . . . . . . . . . . . . . . 18
   
 
  Σ*               Σ*        |
124 | 123 | anbi1i 709 |
. . . . . . . . . . . . . . . . 17
        
Σ*
                      
 
   
  
Σ*
    
                   |
125 | | r19.41v 2928 |
. . . . . . . . . . . . . . . . 17
         Σ*                                Σ*                         |
126 | 124, 125 | bitr4i 260 |
. . . . . . . . . . . . . . . 16
        
Σ*
                      
        Σ*                         |
127 | 126 | exbii 1726 |
. . . . . . . . . . . . . . 15
          
Σ*
                      
  
       Σ*                         |
128 | | df-rex 2762 |
. . . . . . . . . . . . . . 15
        
Σ*
                            
 
  Σ*                          |
129 | | rexcom4 3053 |
. . . . . . . . . . . . . . 15
            Σ*                      
  
       Σ*                         |
130 | 127, 128,
129 | 3bitr4i 285 |
. . . . . . . . . . . . . 14
        
Σ*
                                  Σ*                         |
131 | | breq1 4398 |
. . . . . . . . . . . . . . . . . 18
 Σ*                       Σ*
                        |
132 | | idd 24 |
. . . . . . . . . . . . . . . . . 18
 Σ*      Σ*                     
Σ*
    
                   |
133 | 131, 132 | sylbid 223 |
. . . . . . . . . . . . . . . . 17
 Σ*                      
Σ*
    
                   |
134 | 133 | imp 436 |
. . . . . . . . . . . . . . . 16
 
Σ*
    
                
Σ*
    
                  |
135 | 134 | exlimiv 1784 |
. . . . . . . . . . . . . . 15
    Σ*                       Σ*                        |
136 | 135 | reximi 2852 |
. . . . . . . . . . . . . 14
            Σ*                              Σ*                        |
137 | 130, 136 | sylbi 200 |
. . . . . . . . . . . . 13
        
Σ*
                      
       Σ*                        |
138 | 120, 137 | syl 17 |
. . . . . . . . . . . 12
     Σ*                     Σ*                        |
139 | | simpr 468 |
. . . . . . . . . . . . . . . 16
 

   |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . 15
     
   |
141 | 140 | ss2rabi 3497 |
. . . . . . . . . . . . . 14
       
  |
142 | | rexss 3482 |
. . . . . . . . . . . . . 14
        
         Σ*                     
          
Σ*
    
                    |
143 | 141, 142 | ax-mp 5 |
. . . . . . . . . . . . 13
        Σ*                     
          
Σ*
    
                   |
144 | | unieq 4198 |
. . . . . . . . . . . . . . . . . . . . 21
     |
145 | 144 | sseq2d 3446 |
. . . . . . . . . . . . . . . . . . . 20
  
    |
146 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
147 | 145, 146 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . 19
   
 

    |
148 | 147 | elrab 3184 |
. . . . . . . . . . . . . . . . . 18
  
 
          |
149 | 148 | simprbi 471 |
. . . . . . . . . . . . . . . . 17
  
 
       |
150 | 149 | simpld 466 |
. . . . . . . . . . . . . . . 16
  
 
     |
151 | 150 | a1i 11 |
. . . . . . . . . . . . . . 15
     Σ*                         |
152 | 151 | anim1d 574 |
. . . . . . . . . . . . . 14
     Σ*                     
Σ*
    
                  
Σ*
    
                    |
153 | 152 | reximdv 2857 |
. . . . . . . . . . . . 13
     Σ*               
 
       
Σ*
    
                       Σ*
                         |
154 | 143, 153 | syl5bi 225 |
. . . . . . . . . . . 12
     Σ*               
      Σ*                           
Σ*
    
                    |
155 | 138, 154 | mpd 15 |
. . . . . . . . . . 11
     Σ*                   
Σ*
    
                   |
156 | 155 | ex 441 |
. . . . . . . . . 10
    Σ*            
      
Σ*
    
                    |
157 | 22, 156 | ralrimi 2800 |
. . . . . . . . 9
    Σ*            

     
Σ*
    
                   |
158 | | unieq 4198 |
. . . . . . . . . . . . 13
             |
159 | 158 | sseq2d 3446 |
. . . . . . . . . . . 12
      
        |
160 | | esumeq1 28929 |
. . . . . . . . . . . . 13
    
Σ*
    
Σ*
           |
161 | 160 | breq1d 4405 |
. . . . . . . . . . . 12
     Σ*                      Σ*                             |
162 | 159, 161 | anbi12d 725 |
. . . . . . . . . . 11
        Σ*
                     
     
Σ*
        
                    |
163 | 162 | ac6sg 8936 |
. . . . . . . . . 10
  

 
   Σ*                      
          
     
Σ*
        
                     |
164 | 163 | imp 436 |
. . . . . . . . 9
   
    
Σ*
    
                 
          
     
Σ*
        
                    |
165 | 12, 157, 164 | syl2anc 673 |
. . . . . . . 8
    Σ*            
          
     
Σ*
        
                    |
166 | 9 | ad2antrr 740 |
. . . . . . . . . . . . . 14
     
Σ*            
     
   
     Σ*
                             |
167 | 39 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . . 18
     |
168 | | iunss 4310 |
. . . . . . . . . . . . . . . . . 18
 


   |
169 | 167, 168 | sylibr 217 |
. . . . . . . . . . . . . . . . 17
     |
170 | 44 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . . . 19
 
  |
171 | | iunexg 6788 |
. . . . . . . . . . . . . . . . . . 19
    
  |
172 | 11, 170, 171 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
 
  |
173 | | elpwg 3950 |
. . . . . . . . . . . . . . . . . 18
 
 
   
   |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . . . . 17
    
     |
175 | 169, 174 | mpbird 240 |
. . . . . . . . . . . . . . . 16
 
    |
176 | 32, 175 | ffvelrnd 6038 |
. . . . . . . . . . . . . . 15
    
      |
177 | 107, 176 | sseldi 3416 |
. . . . . . . . . . . . . 14
    
   |
178 | 166, 177 | syl 17 |
. . . . . . . . . . . . 13
     
Σ*            
     
   
     Σ*
                              
   |
179 | | simplr 770 |
. . . . . . . . . . . . . . . . 17
     
Σ*            
     
   
     Σ*
                                
   |
180 | 25 | ad4antr 746 |
. . . . . . . . . . . . . . . . 17
     
Σ*            
     
   
     Σ*
                          
  |
181 | | fex 6155 |
. . . . . . . . . . . . . . . . 17
       

   |
182 | 179, 180,
181 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
     
Σ*            
     
   
     Σ*
                             |
183 | | rnexg 6744 |
. . . . . . . . . . . . . . . 16

  |
184 | | uniexg 6607 |
. . . . . . . . . . . . . . . 16
    |
185 | 182, 183,
184 | 3syl 18 |
. . . . . . . . . . . . . . 15
     
Σ*            
     
   
     Σ*
                              |
186 | | simp-5l 786 |
. . . . . . . . . . . . . . . 16
     
Σ*            
     
   
     Σ*
                             |
187 | 27 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
        
 
 
         |
188 | | frn 5747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      

     |
189 | | ssrab2 3500 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
190 | 188, 189 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . . . . 23
      

   |
191 | 190 | unissd 4214 |
. . . . . . . . . . . . . . . . . . . . . 22
      
      |
192 | | unipw 4650 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
193 | 191, 192 | syl6sseq 3464 |
. . . . . . . . . . . . . . . . . . . . 21
      
    |
194 | 193 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
 
           |
195 | 36 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
          |
196 | 194, 195 | sseqtrd 3454 |
. . . . . . . . . . . . . . . . . . 19
 
           |
197 | 196 | sselda 3418 |
. . . . . . . . . . . . . . . . . 18
        
 
 
  |
198 | 187, 197 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . 17
        
 
 
         |
199 | 198 | ralrimiva 2809 |
. . . . . . . . . . . . . . . 16
 
                    |
200 | 186, 179,
199 | syl2anc 673 |
. . . . . . . . . . . . . . 15
     
Σ*            
     
   
     Σ*
                           
           |
201 | | nfcv 2612 |
. . . . . . . . . . . . . . . 16
    |
202 | 201 | esumcl 28925 |
. . . . . . . . . . . . . . 15
  
          
Σ*            |
203 | 185, 200,
202 | syl2anc 673 |
. . . . . . . . . . . . . 14
     
Σ*            
     
   
     Σ*
                           Σ*            |
204 | 107, 203 | sseldi 3416 |
. . . . . . . . . . . . 13
     
Σ*            
     
   
     Σ*
                           Σ*         |
205 | | simp-5r 787 |
. . . . . . . . . . . . . . 15
     
Σ*            
     
   
     Σ*
                           Σ*        |
206 | 205 | rexrd 9708 |
. . . . . . . . . . . . . 14
     
Σ*            
     
   
     Σ*
                           Σ*        |
207 | | simpllr 777 |
. . . . . . . . . . . . . . 15
     
Σ*            
     
   
     Σ*
                             |
208 | 207 | rpxrd 11365 |
. . . . . . . . . . . . . 14
     
Σ*            
     
   
     Σ*
                             |
209 | 206, 208 | xaddcld 11612 |
. . . . . . . . . . . . 13
     
Σ*            
     
   
     Σ*
                           Σ*            |
210 | 188 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . 22
     
Σ*            
     
   
     Σ*
                          
 
   |
211 | | sstr 3426 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
    
    |
212 | 189, 211 | mpan2 685 |
. . . . . . . . . . . . . . . . . . . . . . 23

      |
213 | | sspwuni 4360 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
214 | 212, 213 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . 22

      |
215 | 210, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
     
Σ*            
     
   
     Σ*
                              |
216 | | ffn 5739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
   |
217 | 216 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
Σ*            
     
   
     Σ*
                             |
218 | 166, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
Σ*            
     
   
     Σ*
                             |
219 | | fnct 28372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
220 | | rnct 28375 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
221 | 219, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
222 | | dfss3 3408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  
      |
223 | 222 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

         |
224 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
225 | 224 | elrab 3184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  

     |
226 | 225 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
   |
227 | 226 | ralimi 2796 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
 
    |
228 | 223, 227 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24

      |
229 | | unictb 9018 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
230 | 221, 228,
229 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
  
     |
231 | 217, 218,
210, 230 | syl21anc 1291 |
. . . . . . . . . . . . . . . . . . . . . 22
     
Σ*            
     
   
     Σ*
                              |
232 | | ctex 7602 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
233 | | elpwg 3950 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
    |
234 | 231, 232,
233 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
     
Σ*            
     
   
     Σ*
                             
    |
235 | 215, 234 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . 20
     
Σ*            
     
   
     Σ*
                               |
236 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     Σ*
                                 |
237 | 236 | ralimi 2796 |
. . . . . . . . . . . . . . . . . . . . . 22
 
      Σ*                          

       |
238 | | fvssunirn 5902 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      |
239 | 238 | unissi 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        |
240 | | sstr 3426 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                 |
241 | 239, 240 | mpan2 685 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          |
242 | 241 | ralimi 2796 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     
    |
243 | | iunss 4310 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 

    |
244 | 242, 243 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     
    |
245 | 237, 244 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
      Σ*                          
     |
246 | 245 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
     
Σ*            
     
   
     Σ*
                           
    |
247 | 235, 246,
231 | jca32 544 |
. . . . . . . . . . . . . . . . . . 19
     
Σ*            
     
   
     Σ*
                                       |
248 | | unieq 4198 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
249 | 248 | sseq2d 3446 |
. . . . . . . . . . . . . . . . . . . . 21
           |
250 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
251 | 249, 250 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . . 20
    

          |
252 | 251 | elrab 3184 |
. . . . . . . . . . . . . . . . . . 19
 
   

              |
253 | 247, 252 | sylibr 217 |
. . . . . . . . . . . . . . . . . 18
     
Σ*            
     
   
     Σ*
                               

    |
254 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
255 | 254 | cbvesumv 28938 |
. . . . . . . . . . . . . . . . . 18
Σ*       Σ* 
      |
256 | | esumeq1 28929 |
. . . . . . . . . . . . . . . . . . . 20
  Σ*      Σ*         |
257 | 256 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . 19
  Σ*       Σ*     
Σ*       Σ* 
        |
258 | 257 | rspcev 3136 |
. . . . . . . . . . . . . . . . . 18
      
  
Σ*       Σ* 
     
    
   Σ*       Σ*        |
259 | 253, 255,
258 | sylancl 675 |
. . . . . . . . . . . . . . . . 17
     
Σ*            
     
   
     Σ*
                           
   

  Σ*       Σ*        |
260 | | esumex 28924 |
. . . . . . . . . . . . . . . . . 18
Σ*        |
261 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . 19
  
     Σ*           

  Σ*        |
262 | 261 | elrnmpt 5087 |
. . . . . . . . . . . . . . . . . 18
Σ* 
    
Σ* 
         
  
Σ*
     
    
   Σ*       Σ*         |
263 | 260, 262 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
Σ* 
         
  
Σ*
     
    
   Σ*       Σ*        |
264 | 259, 263 | sylibr 217 |
. . . . . . . . . . . . . . . 16
     
Σ*            
     
   
     Σ*
                           Σ*         
     Σ*         |
265 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
      |
266 | | omscl 29192 |
. . . . . . . . . . . . . . . . . . . 20
            
  
     Σ*            |
267 | 26, 27, 175, 266 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . 19
     
  
Σ*
       
   |
268 | | xrge0infss 28415 |
. . . . . . . . . . . . . . . . . . 19
     

  Σ*      
   
 
        
  
Σ*
           
     
  
Σ*
           |
269 | 267, 268 | syl 17 |
. . . . . . . . . . . . . . . . . 18
            
  
Σ*
           
     
  
Σ*
           |
270 | 265, 269 | inflb 8023 |
. . . . . . . . . . . . . . . . 17
 Σ*       
   

  Σ*      
Σ*       inf     

  Σ*               |
271 | 29 | fveq1i 5880 |
. . . . . . . . . . . . . . . . . . . 20
      toOMeas       |
272 | 169, 37 | sseqtrd 3454 |
. . . . . . . . . . . . . . . . . . . . 21
     |
273 | | omsfval 29191 |
. . . . . . . . . . . . . . . . . . . . 21
             toOMeas      inf   
     Σ*           
  |
274 | 26, 27, 272, 273 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . 20
  toOMeas      inf   
     Σ*           
  |
275 | 271, 274 | syl5eq 2517 |
. . . . . . . . . . . . . . . . . . 19
    
 inf   
     Σ*           
  |
276 | 275 | breq2d 4407 |
. . . . . . . . . . . . . . . . . 18
 Σ*           
Σ*       inf     

  Σ*               |
277 | 276 | notbid 301 |
. . . . . . . . . . . . . . . . 17
 
Σ*           
Σ*       inf     

  Σ*               |
278 | 270, 277 | sylibrd 242 |
. . . . . . . . . . . . . . . 16
 Σ*       
   

  Σ*      
Σ*               |
279 | 166, 264,
278 | sylc 61 |
. . . . . . . . . . . . . . 15
     
Σ*            
     
   
     Σ*
                           Σ*
     
       |
280 | | biid 244 |
. . . . . . . . . . . . . . 15
 Σ*      
    
Σ*              |
281 | 279, 280 | sylib 201 |
. . . . . . . . . . . . . 14
     
Σ*            
     
   
     Σ*
                           Σ*
     
       |
282 | | xrlenlt 9717 |
. . . . . . . . . . . . . . 15
     

Σ*             
Σ*      
Σ*               |
283 | 178, 204,
282 | syl2anc 673 |
. . . . . . . . . . . . . 14
     
Σ*            
     
   
     Σ*
                                
Σ*      
Σ*               |
284 | 281, 283 | mpbird 240 |
. . . . . . . . . . . . 13
     
Σ*            
     
   
     Σ*
                              
 Σ*         |
285 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . 19
      
  |
286 | 22, 285 | nfan 2031 |
. . . . . . . . . . . . . . . . . 18
     
Σ*            
     
   |
287 | | nfra1 2785 |
. . . . . . . . . . . . . . . . . 18
   
     Σ*
                           |
288 | 286, 287 | nfan 2031 |
. . . . . . . . . . . . . . . . 17
      
Σ*            
     
   
     Σ*
                            |
289 | | simp-6l 788 |
. . . . . . . . . . . . . . . . . . 19
      
Σ*            
     
   
     Σ*
                          
   |
290 | | simpllr 777 |
. . . . . . . . . . . . . . . . . . 19
      
Σ*            
     
   
     Σ*
                          
      
   |
291 | | simpr 468 |
. . . . . . . . . . . . . . . . . . 19
      
Σ*            
     
   
     Σ*
                          
   |
292 | 27 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . . . . 22
         
  
              |
293 | | simpllr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
  
          
   |
294 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
  
       |
295 | 293, 294 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
  
              |
296 | 189, 295 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
  
            |
297 | 296 | elpwid 3952 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
  
           |
298 | 292, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
  
       |
299 | 297, 298 | sseqtrd 3454 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
  
           |
300 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
  
           |
301 | 299, 300 | sseldd 3419 |
. . . . . . . . . . . . . . . . . . . . . 22
         
  
       |
302 | 292, 301 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . . . 21
         
  
              |
303 | 302 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . . . . 20
        
 
                |
304 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . 21
     |
305 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
306 | 305 | esumcl 28925 |
. . . . . . . . . . . . . . . . . . . . 21
       |