Theorem omege0

Description: If the outer measure of a set is greater than or equal to 0 . (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	omege0.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	omege0.x	$$⊢X=\bigcup \mathrm{dom}O$$
	omege0.a	$$⊢\phi \to A\subseteq X$$
Assertion	omege0	$$⊢\phi \to 0\le O\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		omege0.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		omege0.x	$$⊢X=\bigcup \mathrm{dom}O$$
3		omege0.a	$$⊢\phi \to A\subseteq X$$
4		0xr	$$⊢0\in {ℝ}^{*}$$
5	4	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
6		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
7	6	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
8	1 2 3	omecl	$$⊢\phi \to O\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$
9		iccgelb	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge O\left(A\right)\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le O\left(A\right)$$
10	5 7 8 9	syl3anc	$$⊢\phi \to 0\le O\left(A\right)$$