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 φ O OutMeas
Assertion ome0 φ O = 0

Proof

Step Hyp Ref Expression
1 ome0.1 φ O OutMeas
2 isome O OutMeas O OutMeas O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 x 𝒫 dom O y 𝒫 x O y O x x 𝒫 dom O x ω O x sum^ O x
3 1 2 syl φ O OutMeas O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 x 𝒫 dom O y 𝒫 x O y O x x 𝒫 dom O x ω O x sum^ O x
4 1 3 mpbid φ O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 x 𝒫 dom O y 𝒫 x O y O x x 𝒫 dom O x ω O x sum^ O x
5 4 simplld φ O : dom O 0 +∞ dom O = 𝒫 dom O O = 0
6 5 simprd φ O = 0