Theorem omecl

Description: The outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omecl.o	|- ( ph -> O e. OutMeas )
	omecl.x	|- X = U. dom O
	omecl.ss	|- ( ph -> A C_ X )
Assertion	omecl	|- ( ph -> ( O ` A ) e. ( 0 [,] +oo ) )

Proof

Step	Hyp	Ref	Expression
1		omecl.o	|- ( ph -> O e. OutMeas )
2		omecl.x	|- X = U. dom O
3		omecl.ss	|- ( ph -> A C_ X )
4	1 2	omef	|- ( ph -> O : ~P X --> ( 0 [,] +oo ) )
5	2	a1i	|- ( ph -> X = U. dom O )
6	1	dmexd	|- ( ph -> dom O e. _V )
7	6	uniexd	|- ( ph -> U. dom O e. _V )
8	5 7	eqeltrd	|- ( ph -> X e. _V )
9	8 3	ssexd	|- ( ph -> A e. _V )
10		elpwg	|- ( A e. _V -> ( A e. ~P X <-> A C_ X ) )
11	9 10	syl	|- ( ph -> ( A e. ~P X <-> A C_ X ) )
12	3 11	mpbird	|- ( ph -> A e. ~P X )
13	4 12	ffvelcdmd	|- ( ph -> ( O ` A ) e. ( 0 [,] +oo ) )