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	|- ( ph -> X e. Fin )
	ovncl.2	|- ( ph -> A C_ ( RR ^m X ) )
Assertion	ovncl	|- ( ph -> ( ( voln* ` X ) ` A ) e. ( 0 [,] +oo ) )

Proof

Step	Hyp	Ref	Expression
1		ovncl.1	|- ( ph -> X e. Fin )
2		ovncl.2	|- ( ph -> A C_ ( RR ^m X ) )
3	1	ovnf	|- ( ph -> ( voln* ` X ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) )
4		ovexd	|- ( ph -> ( RR ^m X ) e. _V )
5	4 2	ssexd	|- ( ph -> A e. _V )
6		elpwg	|- ( A e. _V -> ( A e. ~P ( RR ^m X ) <-> A C_ ( RR ^m X ) ) )
7	5 6	syl	|- ( ph -> ( A e. ~P ( RR ^m X ) <-> A C_ ( RR ^m X ) ) )
8	2 7	mpbird	|- ( ph -> A e. ~P ( RR ^m X ) )
9	3 8	ffvelrnd	|- ( ph -> ( ( voln* ` X ) ` A ) e. ( 0 [,] +oo ) )