Description: The measure of a countable disjoint union is the sum of the measures. (Contributed by Thierry Arnoux, 26-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | measvun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 | |
|
2 | measbase | |
|
3 | ismeas | |
|
4 | 2 3 | syl | |
5 | 4 | ibi | |
6 | 5 | simp3d | |
7 | 6 | 3ad2ant1 | |
8 | simp3 | |
|
9 | breq1 | |
|
10 | disjeq1 | |
|
11 | 9 10 | anbi12d | |
12 | unieq | |
|
13 | 12 | fveq2d | |
14 | esumeq1 | |
|
15 | 13 14 | eqeq12d | |
16 | 11 15 | imbi12d | |
17 | 16 | rspcv | |
18 | 1 7 8 17 | syl3c | |