Theorem ovncl

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

	Ref	Expression
Hypotheses	ovncl.1	$$⊢\phi \to X\in \mathrm{Fin}$$
	ovncl.2	$$⊢\phi \to A\subseteq {ℝ}^X$$
Assertion	ovncl	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$

Proof

Step	Hyp	Ref	Expression
1		ovncl.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ovncl.2	$$⊢\phi \to A\subseteq {ℝ}^X$$
3	1	ovnf	$$⊢\phi \to \mathrm{voln*}\left(X\right):𝒫\left({ℝ}^X\right)⟶\left[0,\mathrm{+\infty }\right]$$
4		ovexd	$$⊢\phi \to {ℝ}^X\in \mathrm{V}$$
5	4 2	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
6		elpwg	$$⊢A\in \mathrm{V}\to \left(A\in 𝒫\left({ℝ}^X\right)\leftrightarrow A\subseteq {ℝ}^X\right)$$
7	5 6	syl	$$⊢\phi \to \left(A\in 𝒫\left({ℝ}^X\right)\leftrightarrow A\subseteq {ℝ}^X\right)$$
8	2 7	mpbird	$$⊢\phi \to A\in 𝒫\left({ℝ}^X\right)$$
9	3 8	ffvelrnd	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$