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 φ O OutMeas
omef.x X = dom O
Assertion omef φ O : 𝒫 X 0 +∞

Proof

Step Hyp Ref Expression
1 omef.o φ O OutMeas
2 omef.x X = dom O
3 isome O OutMeas O OutMeas O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 y 𝒫 dom O z 𝒫 y O z O y y 𝒫 dom O y ω O y sum^ O y
4 1 3 syl φ O OutMeas O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 y 𝒫 dom O z 𝒫 y O z O y y 𝒫 dom O y ω O y sum^ O y
5 1 4 mpbid φ O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 y 𝒫 dom O z 𝒫 y O z O y y 𝒫 dom O y ω O y sum^ O y
6 5 simplld φ O : dom O 0 +∞ dom O = 𝒫 dom O O = 0
7 6 simplld φ O : dom O 0 +∞
8 2 pweqi 𝒫 X = 𝒫 dom O
9 simp-4r O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 y 𝒫 dom O z 𝒫 y O z O y y 𝒫 dom O y ω O y sum^ O y dom O = 𝒫 dom O
10 5 9 syl φ dom O = 𝒫 dom O
11 8 10 eqtr4id φ 𝒫 X = dom O
12 11 feq2d φ O : 𝒫 X 0 +∞ O : dom O 0 +∞
13 7 12 mpbird φ O : 𝒫 X 0 +∞