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	|- ( ph -> X e. Fin )
	ovnxrcl.2	|- ( ph -> A C_ ( RR ^m X ) )
Assertion	ovnxrcl	|- ( ph -> ( ( voln* ` X ) ` A ) e. RR* )

Proof

Step	Hyp	Ref	Expression
1		ovnxrcl.1	|- ( ph -> X e. Fin )
2		ovnxrcl.2	|- ( ph -> A C_ ( RR ^m X ) )
3		iccssxr	|- ( 0 [,] +oo ) C_ RR*
4	1 2	ovncl	|- ( ph -> ( ( voln* ` X ) ` A ) e. ( 0 [,] +oo ) )
5	3 4	sselid	|- ( ph -> ( ( voln* ` X ) ` A ) e. RR* )