Theorem vonxrcl

Description: The Lebesgue measure of a set is an extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonxrcl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	vonxrcl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
	vonxrcl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
Assertion	vonxrcl	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		vonxrcl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		vonxrcl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
3		vonxrcl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
4		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
5	1 2 3	voncl	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
6	4 5	sseldi	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ* )