Theorem voliunsge0

Description: The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	voliunsge0.1	$$⊢\phi \to E:\mathbb{N}⟶\mathrm{dom}vol$$
	voliunsge0.2	$$⊢\phi \to \underset{n\in \mathbb{N}}{Disj}E\left(n\right)$$
Assertion	voliunsge0	$$⊢\phi \to vol\left(\bigcup _{n\in \mathbb{N}}E\left(n\right)\right)=\mathrm{sum^}\left(\left(n\in \mathbb{N}⟼vol\left(E\left(n\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		voliunsge0.1	$$⊢\phi \to E:\mathbb{N}⟶\mathrm{dom}vol$$
2		voliunsge0.2	$$⊢\phi \to \underset{n\in \mathbb{N}}{Disj}E\left(n\right)$$
3		eqid	$$⊢seq1\left(+,\left(n\in \mathbb{N}⟼vol\left(E\left(n\right)\right)\right)\right)=seq1\left(+,\left(n\in \mathbb{N}⟼vol\left(E\left(n\right)\right)\right)\right)$$
4		eqid	$$⊢\left(n\in \mathbb{N}⟼vol\left(E\left(n\right)\right)\right)=\left(n\in \mathbb{N}⟼vol\left(E\left(n\right)\right)\right)$$
5	3 4 1 2	voliunsge0lem	$$⊢\phi \to vol\left(\bigcup _{n\in \mathbb{N}}E\left(n\right)\right)=\mathrm{sum^}\left(\left(n\in \mathbb{N}⟼vol\left(E\left(n\right)\right)\right)\right)$$