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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovnxrcl.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
Assertion	ovnxrcl	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		ovnxrcl.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovnxrcl.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
3		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
4	1 2	ovncl	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
5	3 4	sselid	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ* )