Metamath Proof Explorer

Theorem ovol0

Description: The empty set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014)

Ref Expression
Assertion ovol0 
|- ( vol* ` (/) ) = 0

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ RR
2 nnex 
 |-  NN e. _V
3 2 0dom 
 |-  (/) ~<_ NN
4 ovolctb2 
 |-  ( ( (/) C_ RR /\ (/) ~<_ NN ) -> ( vol* ` (/) ) = 0 )
5 1 3 4 mp2an 
 |-  ( vol* ` (/) ) = 0