Theorem meage0

Description: If the measure of a measurable set is greater than or equal to 0 . (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	meage0.m	$$⊢\phi \to M\in \mathrm{Meas}$$
	meage0.a	$$⊢\phi \to A\in \mathrm{dom}M$$
Assertion	meage0	$$⊢\phi \to 0\le M\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		meage0.m	$$⊢\phi \to M\in \mathrm{Meas}$$
2		meage0.a	$$⊢\phi \to A\in \mathrm{dom}M$$
3		0xr	$$⊢0\in {ℝ}^{*}$$
4	3	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
5		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
6	5	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
7		eqid	$$⊢\mathrm{dom}M=\mathrm{dom}M$$
8	1 7 2	meacl	$$⊢\phi \to M\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$
9		iccgelb	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge M\left(A\right)\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le M\left(A\right)$$
10	4 6 8 9	syl3anc	$$⊢\phi \to 0\le M\left(A\right)$$