# 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 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge {A}\in 𝒫{S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{x}\right)\right)\to {M}\left(\bigcup {A}\right)=\underset{{x}\in {A}}{{\sum }^{*}}{M}\left({x}\right)$

### Proof

Step Hyp Ref Expression
1 simp2 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge {A}\in 𝒫{S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{x}\right)\right)\to {A}\in 𝒫{S}$
2 measbase ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
3 ismeas ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left({M}\in \mathrm{measures}\left({S}\right)↔\left({M}:{S}⟶\left[0,\mathrm{+\infty }\right]\wedge {M}\left(\varnothing \right)=0\wedge \forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left(\left({y}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {y}}{Disj}{x}\right)\to {M}\left(\bigcup {y}\right)=\underset{{x}\in {y}}{{\sum }^{*}}{M}\left({x}\right)\right)\right)\right)$
4 2 3 syl ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \left({M}\in \mathrm{measures}\left({S}\right)↔\left({M}:{S}⟶\left[0,\mathrm{+\infty }\right]\wedge {M}\left(\varnothing \right)=0\wedge \forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left(\left({y}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {y}}{Disj}{x}\right)\to {M}\left(\bigcup {y}\right)=\underset{{x}\in {y}}{{\sum }^{*}}{M}\left({x}\right)\right)\right)\right)$
5 4 ibi ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \left({M}:{S}⟶\left[0,\mathrm{+\infty }\right]\wedge {M}\left(\varnothing \right)=0\wedge \forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left(\left({y}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {y}}{Disj}{x}\right)\to {M}\left(\bigcup {y}\right)=\underset{{x}\in {y}}{{\sum }^{*}}{M}\left({x}\right)\right)\right)$
6 5 simp3d ${⊢}{M}\in \mathrm{measures}\left({S}\right)\to \forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left(\left({y}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {y}}{Disj}{x}\right)\to {M}\left(\bigcup {y}\right)=\underset{{x}\in {y}}{{\sum }^{*}}{M}\left({x}\right)\right)$
7 6 3ad2ant1 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge {A}\in 𝒫{S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{x}\right)\right)\to \forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left(\left({y}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {y}}{Disj}{x}\right)\to {M}\left(\bigcup {y}\right)=\underset{{x}\in {y}}{{\sum }^{*}}{M}\left({x}\right)\right)$
8 simp3 ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge {A}\in 𝒫{S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{x}\right)\right)\to \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{x}\right)$
9 breq1 ${⊢}{y}={A}\to \left({y}\preccurlyeq \mathrm{\omega }↔{A}\preccurlyeq \mathrm{\omega }\right)$
10 disjeq1 ${⊢}{y}={A}\to \left(\underset{{x}\in {y}}{Disj}{x}↔\underset{{x}\in {A}}{Disj}{x}\right)$
11 9 10 anbi12d ${⊢}{y}={A}\to \left(\left({y}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {y}}{Disj}{x}\right)↔\left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{x}\right)\right)$
12 unieq ${⊢}{y}={A}\to \bigcup {y}=\bigcup {A}$
13 12 fveq2d ${⊢}{y}={A}\to {M}\left(\bigcup {y}\right)={M}\left(\bigcup {A}\right)$
14 esumeq1 ${⊢}{y}={A}\to \underset{{x}\in {y}}{{\sum }^{*}}{M}\left({x}\right)=\underset{{x}\in {A}}{{\sum }^{*}}{M}\left({x}\right)$
15 13 14 eqeq12d ${⊢}{y}={A}\to \left({M}\left(\bigcup {y}\right)=\underset{{x}\in {y}}{{\sum }^{*}}{M}\left({x}\right)↔{M}\left(\bigcup {A}\right)=\underset{{x}\in {A}}{{\sum }^{*}}{M}\left({x}\right)\right)$
16 11 15 imbi12d ${⊢}{y}={A}\to \left(\left(\left({y}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {y}}{Disj}{x}\right)\to {M}\left(\bigcup {y}\right)=\underset{{x}\in {y}}{{\sum }^{*}}{M}\left({x}\right)\right)↔\left(\left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{x}\right)\to {M}\left(\bigcup {A}\right)=\underset{{x}\in {A}}{{\sum }^{*}}{M}\left({x}\right)\right)\right)$
17 16 rspcv ${⊢}{A}\in 𝒫{S}\to \left(\forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left(\left({y}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {y}}{Disj}{x}\right)\to {M}\left(\bigcup {y}\right)=\underset{{x}\in {y}}{{\sum }^{*}}{M}\left({x}\right)\right)\to \left(\left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{x}\right)\to {M}\left(\bigcup {A}\right)=\underset{{x}\in {A}}{{\sum }^{*}}{M}\left({x}\right)\right)\right)$
18 1 7 8 17 syl3c ${⊢}\left({M}\in \mathrm{measures}\left({S}\right)\wedge {A}\in 𝒫{S}\wedge \left({A}\preccurlyeq \mathrm{\omega }\wedge \underset{{x}\in {A}}{Disj}{x}\right)\right)\to {M}\left(\bigcup {A}\right)=\underset{{x}\in {A}}{{\sum }^{*}}{M}\left({x}\right)$