Metamath Proof Explorer


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 ffvelrnd
 |-  ( ph -> ( O ` A ) e. ( 0 [,] +oo ) )