Step | Hyp | Ref
| Expression |
1 | | 1re 9668 |
. . . . . . 7
 |
2 | 1 | rexri 9719 |
. . . . . 6
 |
3 | | 0le1 10165 |
. . . . . 6
 |
4 | | pnfge 11461 |
. . . . . . 7

  |
5 | 2, 4 | ax-mp 5 |
. . . . . 6
 |
6 | | 0xr 9713 |
. . . . . . 7
 |
7 | | pnfxr 11441 |
. . . . . . 7
 |
8 | | elicc1 11709 |
. . . . . . 7
      

    |
9 | 6, 7, 8 | mp2an 683 |
. . . . . 6
   

   |
10 | 2, 3, 5, 9 | mpbir3an 1196 |
. . . . 5
    |
11 | | 0e0iccpnf 11772 |
. . . . 5
    |
12 | 10, 11 | keepel 3960 |
. . . 4
         |
13 | 12 | rgenw 2761 |
. . 3
           |
14 | | df-dde 29105 |
. . . 4
δ          |
15 | 14 | fmpt 6066 |
. . 3
 
        
δ         |
16 | 13, 15 | mpbi 213 |
. 2
δ        |
17 | | 0ss 3775 |
. . 3
 |
18 | | noel 3747 |
. . 3
 |
19 | | ddeval0 29107 |
. . 3
 
 δ    |
20 | 17, 18, 19 | mp2an 683 |
. 2
δ   |
21 | | rabxm 3767 |
. . . . . . . . 9
       |
22 | | esumeq1 28904 |
. . . . . . . . 9
      
Σ*  δ  Σ*        δ    |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
Σ*  δ  Σ*        δ   |
24 | | nfv 1772 |
. . . . . . . . 9
    |
25 | | nfcv 2603 |
. . . . . . . . 9
     |
26 | | nfcv 2603 |
. . . . . . . . 9
     |
27 | | rabexg 4567 |
. . . . . . . . 9
       |
28 | | rabexg 4567 |
. . . . . . . . 9
       |
29 | | rabnc 3768 |
. . . . . . . . . 10
       |
30 | 29 | a1i 11 |
. . . . . . . . 9
           |
31 | | elrabi 3205 |
. . . . . . . . . . . 12
     |
32 | 31 | adantl 472 |
. . . . . . . . . . 11
      
  |
33 | | simpl 463 |
. . . . . . . . . . 11
      
    |
34 | | elelpwi 3974 |
. . . . . . . . . . 11
 
  
   |
35 | 32, 33, 34 | syl2anc 671 |
. . . . . . . . . 10
      
   |
36 | 16 | ffvelrni 6044 |
. . . . . . . . . 10
  δ       |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
      
δ       |
38 | | elrabi 3205 |
. . . . . . . . . . . 12
     |
39 | 38 | adantl 472 |
. . . . . . . . . . 11
         |
40 | | simpl 463 |
. . . . . . . . . . 11
           |
41 | 39, 40, 34 | syl2anc 671 |
. . . . . . . . . 10
          |
42 | 41, 36 | syl 17 |
. . . . . . . . 9
       δ       |
43 | 24, 25, 26, 27, 28, 30, 37, 42 | esumsplit 28923 |
. . . . . . . 8
   Σ*        δ  Σ*   δ    Σ*   δ     |
44 | 23, 43 | syl5eq 2508 |
. . . . . . 7
   Σ*  δ  Σ*   δ    Σ*   δ     |
45 | 44 | adantr 471 |
. . . . . 6
    Disj

Σ*  δ  Σ*   δ    Σ*   δ     |
46 | | esumeq1 28904 |
. . . . . . . . . . . 12
     Σ*   δ  Σ*   δ    |
47 | 46 | adantl 472 |
. . . . . . . . . . 11
       Disj


      
Σ*   δ  Σ*
  δ    |
48 | | simp-4l 781 |
. . . . . . . . . . . 12
       Disj


      
    |
49 | | vex 3060 |
. . . . . . . . . . . . . 14
 |
50 | 49 | rabsnel 28187 |
. . . . . . . . . . . . 13
       |
51 | 50 | adantl 472 |
. . . . . . . . . . . 12
       Disj


      
  |
52 | | eleq2 2529 |
. . . . . . . . . . . . . 14
 
   |
53 | 49, 52 | rabsnt 4062 |
. . . . . . . . . . . . 13
       |
54 | 53 | adantl 472 |
. . . . . . . . . . . 12
       Disj


      
  |
55 | | elelpwi 3974 |
. . . . . . . . . . . . . . . 16
 
  
   |
56 | 55 | ancoms 459 |
. . . . . . . . . . . . . . 15
    
   |
57 | 56 | adantrr 728 |
. . . . . . . . . . . . . 14
          |
58 | | simpr 467 |
. . . . . . . . . . . . . . . 16
      |
59 | 58 | fveq2d 5892 |
. . . . . . . . . . . . . . 15
    δ  δ    |
60 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
    |
61 | 16 | ffvelrni 6044 |
. . . . . . . . . . . . . . 15
  δ       |
62 | 59, 60, 61 | esumsn 28935 |
. . . . . . . . . . . . . 14
  Σ*   δ  δ    |
63 | 57, 62 | syl 17 |
. . . . . . . . . . . . 13
       Σ*   δ  δ    |
64 | 57 | elpwid 3973 |
. . . . . . . . . . . . . 14
      
  |
65 | | simprr 771 |
. . . . . . . . . . . . . 14
         |
66 | | ddeval1 29106 |
. . . . . . . . . . . . . 14
 
 δ    |
67 | 64, 65, 66 | syl2anc 671 |
. . . . . . . . . . . . 13
       δ    |
68 | 63, 67 | eqtrd 2496 |
. . . . . . . . . . . 12
       Σ*   δ    |
69 | 48, 51, 54, 68 | syl12anc 1274 |
. . . . . . . . . . 11
       Disj


      
Σ*   δ    |
70 | 47, 69 | eqtrd 2496 |
. . . . . . . . . 10
       Disj


      
Σ*   δ    |
71 | | df-disj 4388 |
. . . . . . . . . . . . . . 15
Disj
  
  |
72 | | c0ex 9663 |
. . . . . . . . . . . . . . . 16
 |
73 | | eleq1 2528 |
. . . . . . . . . . . . . . . . 17
 
   |
74 | 73 | rmobidv 2992 |
. . . . . . . . . . . . . . . 16
  

   |
75 | 72, 74 | spcv 3152 |
. . . . . . . . . . . . . . 15
   
   |
76 | 71, 75 | sylbi 200 |
. . . . . . . . . . . . . 14
Disj
   |
77 | | rmo5 3023 |
. . . . . . . . . . . . . . . 16
 
 
    |
78 | 77 | biimpi 199 |
. . . . . . . . . . . . . . 15
   

   |
79 | 78 | imp 435 |
. . . . . . . . . . . . . 14
     
  |
80 | 76, 79 | sylan 478 |
. . . . . . . . . . . . 13
 Disj
     |
81 | | reusn 4058 |
. . . . . . . . . . . . 13
 
        |
82 | 80, 81 | sylib 201 |
. . . . . . . . . . . 12
 Disj
          |
83 | | eleq2 2529 |
. . . . . . . . . . . . . . . . 17
 
   |
84 | 83 | cbvrabv 3056 |
. . . . . . . . . . . . . . . 16
     |
85 | 84 | eqeq1i 2467 |
. . . . . . . . . . . . . . 15
           |
86 | 50 | ancri 559 |
. . . . . . . . . . . . . . 15
             |
87 | 85, 86 | sylbir 218 |
. . . . . . . . . . . . . 14
             |
88 | 87 | eximi 1718 |
. . . . . . . . . . . . 13
                 |
89 | | df-rex 2755 |
. . . . . . . . . . . . 13
                |
90 | 88, 89 | sylibr 217 |
. . . . . . . . . . . 12
       

     |
91 | 82, 90 | syl 17 |
. . . . . . . . . . 11
 Disj
         |
92 | 91 | adantll 725 |
. . . . . . . . . 10
    
Disj  
 

     |
93 | 70, 92 | r19.29a 2944 |
. . . . . . . . 9
    
Disj  

Σ*   δ    |
94 | | elpwi 3972 |
. . . . . . . . . . . 12
  
   |
95 | | sspwuni 4381 |
. . . . . . . . . . . 12
 
   |
96 | 94, 95 | sylib 201 |
. . . . . . . . . . 11
      |
97 | | eluni2 4216 |
. . . . . . . . . . . 12
 

  |
98 | 97 | biimpri 211 |
. . . . . . . . . . 11
     |
99 | | ddeval1 29106 |
. . . . . . . . . . 11
    
δ     |
100 | 96, 98, 99 | syl2an 484 |
. . . . . . . . . 10
     
δ     |
101 | 100 | adantlr 726 |
. . . . . . . . 9
    
Disj  
 δ     |
102 | 93, 101 | eqtr4d 2499 |
. . . . . . . 8
    
Disj  

Σ*   δ  δ     |
103 | | nfre1 2860 |
. . . . . . . . . . . . 13
    |
104 | 103 | nfn 1994 |
. . . . . . . . . . . 12
   |
105 | 83 | elrab 3208 |
. . . . . . . . . . . . . . . 16
  

   |
106 | 105 | exbii 1729 |
. . . . . . . . . . . . . . 15
          |
107 | | neq0 3754 |
. . . . . . . . . . . . . . 15
  
     |
108 | | df-rex 2755 |
. . . . . . . . . . . . . . 15
 
  
   |
109 | 106, 107,
108 | 3bitr4i 285 |
. . . . . . . . . . . . . 14
  

  |
110 | 109 | biimpi 199 |
. . . . . . . . . . . . 13
   
  |
111 | 110 | con1i 134 |
. . . . . . . . . . . 12
      |
112 | 104, 111 | esumeq1d 28905 |
. . . . . . . . . . 11
  Σ*   δ 
Σ*  δ    |
113 | | esumnul 28918 |
. . . . . . . . . . 11
Σ*  δ   |
114 | 112, 113 | syl6eq 2512 |
. . . . . . . . . 10
  Σ*   δ    |
115 | 114 | adantl 472 |
. . . . . . . . 9
    
Disj    Σ*   δ    |
116 | 97 | biimpi 199 |
. . . . . . . . . . . 12
  
  |
117 | 116 | con3i 142 |
. . . . . . . . . . 11
 
   |
118 | | ddeval0 29107 |
. . . . . . . . . . 11
     δ     |
119 | 96, 117, 118 | syl2an 484 |
. . . . . . . . . 10
    
 δ     |
120 | 119 | adantlr 726 |
. . . . . . . . 9
    
Disj    δ     |
121 | 115, 120 | eqtr4d 2499 |
. . . . . . . 8
    
Disj    Σ*   δ  δ     |
122 | 102, 121 | pm2.61dan 805 |
. . . . . . 7
    Disj

Σ*   δ  δ     |
123 | 41 | elpwid 3973 |
. . . . . . . . . . 11
         |
124 | 83 | notbid 300 |
. . . . . . . . . . . . . 14
 
   |
125 | 124 | elrab 3208 |
. . . . . . . . . . . . 13
  

   |
126 | 125 | simprbi 470 |
. . . . . . . . . . . 12
  
  |
127 | 126 | adantl 472 |
. . . . . . . . . . 11
      
  |
128 | | ddeval0 29107 |
. . . . . . . . . . 11
 
 δ    |
129 | 123, 127,
128 | syl2anc 671 |
. . . . . . . . . 10
       δ    |
130 | 129 | esumeq2dv 28908 |
. . . . . . . . 9
   Σ*   δ 
Σ*      |
131 | | vex 3060 |
. . . . . . . . . . 11
 |
132 | 131 | rabex 4568 |
. . . . . . . . . 10

  |
133 | 26 | esum0 28919 |
. . . . . . . . . 10
   Σ*      |
134 | 132, 133 | ax-mp 5 |
. . . . . . . . 9
Σ*     |
135 | 130, 134 | syl6eq 2512 |
. . . . . . . 8
   Σ*   δ    |
136 | 135 | adantr 471 |
. . . . . . 7
    Disj

Σ*   δ    |
137 | 122, 136 | oveq12d 6333 |
. . . . . 6
    Disj
 Σ*   δ    Σ*   δ    δ         |
138 | 131 | uniex 6614 |
. . . . . . . . . 10
  |
139 | 138 | elpw 3969 |
. . . . . . . . 9
 
 
  |
140 | 139 | biimpri 211 |
. . . . . . . 8
      |
141 | | iccssxr 11746 |
. . . . . . . . 9
    |
142 | 16 | ffvelrni 6044 |
. . . . . . . . 9
 
 δ        |
143 | 141, 142 | sseldi 3442 |
. . . . . . . 8
 
 δ     |
144 | | xaddid1 11561 |
. . . . . . . 8
 δ    δ       δ     |
145 | 96, 140, 143, 144 | 4syl 19 |
. . . . . . 7
    δ       δ     |
146 | 145 | adantr 471 |
. . . . . 6
    Disj
  δ       δ     |
147 | 45, 137, 146 | 3eqtrrd 2501 |
. . . . 5
    Disj
 δ   Σ*  δ    |
148 | 147 | adantrl 727 |
. . . 4
     Disj   δ   Σ*  δ    |
149 | 148 | ex 440 |
. . 3
     Disj 
δ   Σ*  δ     |
150 | 149 | rgen 2759 |
. 2
     Disj  δ   Σ*  δ    |
151 | | reex 9656 |
. . . 4
 |
152 | | pwsiga 29001 |
. . . 4
  sigAlgebra    |
153 | 151, 152 | ax-mp 5 |
. . 3
 sigAlgebra   |
154 | | elrnsiga 28997 |
. . 3
  sigAlgebra    sigAlgebra |
155 | | ismeas 29070 |
. . 3
   sigAlgebra δ measures   δ       δ      
Disj  δ   Σ*  δ       |
156 | 153, 154,
155 | mp2b 10 |
. 2
δ measures   δ       δ      
Disj  δ   Σ*  δ      |
157 | 16, 20, 150, 156 | mpbir3an 1196 |
1
δ measures    |