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∈OutMeas→dom⁡O=𝒫⋃dom⁡O

Proof

Step Hyp Ref Expression
1 isome ⊢O∈OutMeas→O∈OutMeas↔O:dom⁡O⟶0+∞∧dom⁡O=𝒫⋃dom⁡O∧O⁡∅=0∧∀x∈𝒫⋃dom⁡O∀y∈𝒫xO⁡y≤O⁡x∧∀x∈𝒫dom⁡Ox≼ω→O⁡⋃x≤sum^⁡O↾x
2 1 ibi ⊢O∈OutMeas→O:dom⁡O⟶0+∞∧dom⁡O=𝒫⋃dom⁡O∧O⁡∅=0∧∀x∈𝒫⋃dom⁡O∀y∈𝒫xO⁡y≤O⁡x∧∀x∈𝒫dom⁡Ox≼ω→O⁡⋃x≤sum^⁡O↾x
3 2 simplld ⊢O∈OutMeas→O:dom⁡O⟶0+∞∧dom⁡O=𝒫⋃dom⁡O∧O⁡∅=0
4 3 simplrd ⊢O∈OutMeas→dom⁡O=𝒫⋃dom⁡O