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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovncl.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
Assertion	ovncl	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		ovncl.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovncl.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
3	1	ovnf	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) : 𝒫 ( ℝ ↑m 𝑋 ) ⟶ ( 0 [,] +∞ ) )
4		ovexd	⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) ∈ V )
5	4 2	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
6		elpwg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↔ 𝐴 ⊆ ( ℝ ↑m 𝑋 ) ) )
7	5 6	syl	⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↔ 𝐴 ⊆ ( ℝ ↑m 𝑋 ) ) )
8	2 7	mpbird	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ( ℝ ↑m 𝑋 ) )
9	3 8	ffvelcdmd	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )