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	|- ( ph -> X e. Fin )
	vonxrcl.s	|- S = dom ( voln ` X )
	vonxrcl.a	|- ( ph -> A e. S )
Assertion	vonxrcl	|- ( ph -> ( ( voln ` X ) ` A ) e. RR* )

Proof

Step	Hyp	Ref	Expression
1		vonxrcl.x	|- ( ph -> X e. Fin )
2		vonxrcl.s	|- S = dom ( voln ` X )
3		vonxrcl.a	|- ( ph -> A e. S )
4		iccssxr	|- ( 0 [,] +oo ) C_ RR*
5	1 2 3	voncl	|- ( ph -> ( ( voln ` X ) ` A ) e. ( 0 [,] +oo ) )
6	4 5	sseldi	|- ( ph -> ( ( voln ` X ) ` A ) e. RR* )