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 ∈ 𝒫 x O ⁡ y ≤ O ⁡ x ∧ ∀ x ∈ 𝒫 dom ⁡ O x ≼ ω → O ⁡ ⋃ x ≤ sum^ ⁡ O ↾ x
2 1 ibi ⊢ 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 2 simplld ⊢ O ∈ OutMeas → O : dom ⁡ O ⟶ 0 +∞ ∧ dom ⁡ O = 𝒫 ⋃ dom ⁡ O ∧ O ⁡ ∅ = 0
4 3 simplrd ⊢ O ∈ OutMeas → dom ⁡ O = 𝒫 ⋃ dom ⁡ O