# 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 ${⊢}{\phi }\to {O}\in \mathrm{OutMeas}$
Assertion ome0 ${⊢}{\phi }\to {O}\left(\varnothing \right)=0$

### Proof

Step Hyp Ref Expression
1 ome0.1 ${⊢}{\phi }\to {O}\in \mathrm{OutMeas}$
2 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)$
3 1 2 syl ${⊢}{\phi }\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)$
4 1 3 mpbid ${⊢}{\phi }\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)$
5 4 simplld ${⊢}{\phi }\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)$
6 5 simprd ${⊢}{\phi }\to {O}\left(\varnothing \right)=0$