Metamath Proof Explorer

Theorem omef

Description: An outer measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses omef.o 
|- ( ph -> O e. OutMeas )
omef.x 
|- X = U. dom O
Assertion omef 
|- ( ph -> O : ~P X --> ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 omef.o 
 |-  ( ph -> O e. OutMeas )
2 omef.x 
 |-  X = U. dom O
3 isome 
 |-  ( O e. OutMeas -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. y e. ~P U. dom O A. z e. ~P y ( O ` z ) <_ ( O ` y ) ) /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) ) )
4 1 3 syl 
 |-  ( ph -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. y e. ~P U. dom O A. z e. ~P y ( O ` z ) <_ ( O ` y ) ) /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) ) )
5 1 4 mpbid 
 |-  ( ph -> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. y e. ~P U. dom O A. z e. ~P y ( O ` z ) <_ ( O ` y ) ) /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) )
6 5 simplld 
 |-  ( ph -> ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) )
7 6 simplld 
 |-  ( ph -> O : dom O --> ( 0 [,] +oo ) )
8 2 pweqi 
 |-  ~P X = ~P U. dom O
9 simp-4r 
 |-  ( ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. y e. ~P U. dom O A. z e. ~P y ( O ` z ) <_ ( O ` y ) ) /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) -> dom O = ~P U. dom O )
10 5 9 syl 
 |-  ( ph -> dom O = ~P U. dom O )
11 8 10 eqtr4id 
 |-  ( ph -> ~P X = dom O )
12 11 feq2d 
 |-  ( ph -> ( O : ~P X --> ( 0 [,] +oo ) <-> O : dom O --> ( 0 [,] +oo ) ) )
13 7 12 mpbird 
 |-  ( ph -> O : ~P X --> ( 0 [,] +oo ) )