# Metamath Proof Explorer

## Theorem omedm

Description: The domain of an outer measure is a power set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion omedm ${⊢}{O}\in \mathrm{OutMeas}\to \mathrm{dom}{O}=𝒫\bigcup \mathrm{dom}{O}$

### Proof

Step Hyp Ref Expression
1 isome ${⊢}{O}\in \mathrm{OutMeas}\to \left({O}\in \mathrm{OutMeas}↔\left(\left(\left(\left({O}:\mathrm{dom}{O}⟶\left[0,\mathrm{+\infty }\right]\wedge \mathrm{dom}{O}=𝒫\bigcup \mathrm{dom}{O}\right)\wedge {O}\left(\varnothing \right)=0\right)\wedge \forall {x}\in 𝒫\bigcup \mathrm{dom}{O}\phantom{\rule{.4em}{0ex}}\forall {y}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}{O}\left({y}\right)\le {O}\left({x}\right)\right)\wedge \forall {x}\in 𝒫\mathrm{dom}{O}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to {O}\left(\bigcup {x}\right)\le \mathrm{sum^}\left({{O}↾}_{{x}}\right)\right)\right)\right)$
2 1 ibi ${⊢}{O}\in \mathrm{OutMeas}\to \left(\left(\left(\left({O}:\mathrm{dom}{O}⟶\left[0,\mathrm{+\infty }\right]\wedge \mathrm{dom}{O}=𝒫\bigcup \mathrm{dom}{O}\right)\wedge {O}\left(\varnothing \right)=0\right)\wedge \forall {x}\in 𝒫\bigcup \mathrm{dom}{O}\phantom{\rule{.4em}{0ex}}\forall {y}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}{O}\left({y}\right)\le {O}\left({x}\right)\right)\wedge \forall {x}\in 𝒫\mathrm{dom}{O}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to {O}\left(\bigcup {x}\right)\le \mathrm{sum^}\left({{O}↾}_{{x}}\right)\right)\right)$
3 2 simplld ${⊢}{O}\in \mathrm{OutMeas}\to \left(\left({O}:\mathrm{dom}{O}⟶\left[0,\mathrm{+\infty }\right]\wedge \mathrm{dom}{O}=𝒫\bigcup \mathrm{dom}{O}\right)\wedge {O}\left(\varnothing \right)=0\right)$
4 3 simplrd ${⊢}{O}\in \mathrm{OutMeas}\to \mathrm{dom}{O}=𝒫\bigcup \mathrm{dom}{O}$