Theorem omexrcl

Description: The outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		omexrcl.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		omexrcl.x	$$⊢X=\bigcup \mathrm{dom}O$$
3		omexrcl.a	$$⊢\phi \to A\subseteq X$$
4		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
5	1 2 3	omecl	$$⊢\phi \to O\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$
6	4 5	sselid	$$⊢\phi \to O\left(A\right)\in {ℝ}^{*}$$