Metamath Proof Explorer


Theorem measvun

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 MmeasuresSA𝒫SAωDisjxAxMA=*xAMx

Proof

Step Hyp Ref Expression
1 simp2 MmeasuresSA𝒫SAωDisjxAxA𝒫S
2 measbase MmeasuresSSransigAlgebra
3 ismeas SransigAlgebraMmeasuresSM:S0+∞M=0y𝒫SyωDisjxyxMy=*xyMx
4 2 3 syl MmeasuresSMmeasuresSM:S0+∞M=0y𝒫SyωDisjxyxMy=*xyMx
5 4 ibi MmeasuresSM:S0+∞M=0y𝒫SyωDisjxyxMy=*xyMx
6 5 simp3d MmeasuresSy𝒫SyωDisjxyxMy=*xyMx
7 6 3ad2ant1 MmeasuresSA𝒫SAωDisjxAxy𝒫SyωDisjxyxMy=*xyMx
8 simp3 MmeasuresSA𝒫SAωDisjxAxAωDisjxAx
9 breq1 y=AyωAω
10 disjeq1 y=ADisjxyxDisjxAx
11 9 10 anbi12d y=AyωDisjxyxAωDisjxAx
12 unieq y=Ay=A
13 12 fveq2d y=AMy=MA
14 esumeq1 y=A*xyMx=*xAMx
15 13 14 eqeq12d y=AMy=*xyMxMA=*xAMx
16 11 15 imbi12d y=AyωDisjxyxMy=*xyMxAωDisjxAxMA=*xAMx
17 16 rspcv A𝒫Sy𝒫SyωDisjxyxMy=*xyMxAωDisjxAxMA=*xAMx
18 1 7 8 17 syl3c MmeasuresSA𝒫SAωDisjxAxMA=*xAMx