Theorem meaiunle

Description: The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of Fremlin1 p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	meaiunle.nph	$$⊢Ⅎn\phi$$
	meaiunle.m	$$⊢\phi \to M\in \mathrm{Meas}$$
	meaiunle.s	$$⊢S=\mathrm{dom}M$$
	meaiunle.z	$$⊢Z={\mathbb{Z}}_{\ge N}$$
	meaiunle.e	$$⊢\phi \to E:Z⟶S$$
Assertion	meaiunle	$$⊢\phi \to M\left(\bigcup _{n\in Z}E\left(n\right)\right)\le \mathrm{sum^}\left(\left(n\in Z⟼M\left(E\left(n\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		meaiunle.nph	$$⊢Ⅎn\phi$$
2		meaiunle.m	$$⊢\phi \to M\in \mathrm{Meas}$$
3		meaiunle.s	$$⊢S=\mathrm{dom}M$$
4		meaiunle.z	$$⊢Z={\mathbb{Z}}_{\ge N}$$
5		meaiunle.e	$$⊢\phi \to E:Z⟶S$$
6		eqid	$$⊢\left(n\in Z⟼E\left(n\right)\setminus \bigcup _{x\in \left(N..^n\right)}E\left(x\right)\right)=\left(n\in Z⟼E\left(n\right)\setminus \bigcup _{x\in \left(N..^n\right)}E\left(x\right)\right)$$
7	1 2 3 4 5 6	meaiunlelem	$$⊢\phi \to M\left(\bigcup _{n\in Z}E\left(n\right)\right)\le \mathrm{sum^}\left(\left(n\in Z⟼M\left(E\left(n\right)\right)\right)\right)$$