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 ⊢ φ → O ∈ OutMeas
Assertion ome0 ⊢ φ → O ⁡ ∅ = 0

Proof

Step Hyp Ref Expression
1 ome0.1 ⊢ φ → O ∈ OutMeas
2 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
3 1 2 syl ⊢ φ → 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
4 1 3 mpbid ⊢ φ → 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
5 4 simplld ⊢ φ → O : dom ⁡ O ⟶ 0 +∞ ∧ dom ⁡ O = 𝒫 ⋃ dom ⁡ O ∧ O ⁡ ∅ = 0
6 5 simprd ⊢ φ → O ⁡ ∅ = 0