Theorem ovnxrcl

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

	Ref	Expression
Hypotheses	ovnxrcl.1	$$⊢\phi \to X\in \mathrm{Fin}$$
	ovnxrcl.2	$$⊢\phi \to A\subseteq {ℝ}^X$$
Assertion	ovnxrcl	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		ovnxrcl.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ovnxrcl.2	$$⊢\phi \to A\subseteq {ℝ}^X$$
3		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
4	1 2	ovncl	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$
5	3 4	sseldi	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)\in {ℝ}^{*}$$