Metamath Proof Explorer

Theorem ome0

Description: The outer measure of the empty set is 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis ome0.1 
|- ( ph -> O e. OutMeas )
Assertion ome0 
|- ( ph -> ( O ` (/) ) = 0 )

Proof

Step Hyp Ref Expression
1 ome0.1 
 |-  ( ph -> O e. OutMeas )
2 isome 
 |-  ( O e. OutMeas -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. x e. ~P U. dom O A. y e. ~P x ( O ` y ) <_ ( O ` x ) ) /\ A. x e. ~P dom O ( x ~<_ _om -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) ) ) )
3 1 2 syl 
 |-  ( ph -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. x e. ~P U. dom O A. y e. ~P x ( O ` y ) <_ ( O ` x ) ) /\ A. x e. ~P dom O ( x ~<_ _om -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) ) ) )
4 1 3 mpbid 
 |-  ( ph -> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. x e. ~P U. dom O A. y e. ~P x ( O ` y ) <_ ( O ` x ) ) /\ A. x e. ~P dom O ( x ~<_ _om -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) ) )
5 4 simplld 
 |-  ( ph -> ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) )
6 5 simprd 
 |-  ( ph -> ( O ` (/) ) = 0 )