Metamath Proof Explorer

Theorem ovn0val

Description: The Lebesgue outer measure (for the zero dimensional space of reals) of every subset is zero. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis ovn0val.1 ⊢ φ → A ⊆ ℝ ∅
Assertion ovn0val ⊢ φ → voln* ⁡ ∅ ⁡ A = 0

Proof

Step Hyp Ref Expression
1 ovn0val.1 ⊢ φ → A ⊆ ℝ ∅
2 0fi ⊢ ∅ ∈ Fin
3 2 a1i ⊢ φ → ∅ ∈ Fin
4 eqid ⊢ z ∈ ℝ * | ∃ i ∈ ℝ 2 ∅ ℕ A ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ ∅ vol ⁡ . ∘ i ⁡ j ⁡ k = z ∈ ℝ * | ∃ i ∈ ℝ 2 ∅ ℕ A ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ ∅ vol ⁡ . ∘ i ⁡ j ⁡ k
5 3 1 4 ovnval2 ⊢ φ → voln* ⁡ ∅ ⁡ A = if ∅ = ∅ 0 inf z ∈ ℝ * | ∃ i ∈ ℝ 2 ∅ ℕ A ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ ∅ vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * <
6 eqid ⊢ ∅ = ∅
7 iftrue ⊢ ∅ = ∅ → if ∅ = ∅ 0 inf z ∈ ℝ * | ∃ i ∈ ℝ 2 ∅ ℕ A ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ ∅ vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * < = 0
8 6 7 ax-mp ⊢ if ∅ = ∅ 0 inf z ∈ ℝ * | ∃ i ∈ ℝ 2 ∅ ℕ A ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ ∅ vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * < = 0
9 8 a1i ⊢ φ → if ∅ = ∅ 0 inf z ∈ ℝ * | ∃ i ∈ ℝ 2 ∅ ℕ A ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ ∅ vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * < = 0
10 5 9 eqtrd ⊢ φ → voln* ⁡ ∅ ⁡ A = 0