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 0fin ⊢∅∈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∅=∅0supz∈ℝ*|∃i∈ℝ2∅ℕA⊆⋃j∈ℕ⨉k∈∅.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈∅vol⁡.∘i⁡j⁡kℝ*<
6 eqid ⊢∅=∅
7 iftrue ⊢∅=∅→if∅=∅0supz∈ℝ*|∃i∈ℝ2∅ℕA⊆⋃j∈ℕ⨉k∈∅.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈∅vol⁡.∘i⁡j⁡kℝ*<=0
8 6 7 ax-mp ⊢if∅=∅0supz∈ℝ*|∃i∈ℝ2∅ℕA⊆⋃j∈ℕ⨉k∈∅.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈∅vol⁡.∘i⁡j⁡kℝ*<=0
9 8 a1i ⊢φ→if∅=∅0supz∈ℝ*|∃i∈ℝ2∅ℕA⊆⋃j∈ℕ⨉k∈∅.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈∅vol⁡.∘i⁡j⁡kℝ*<=0
10 5 9 eqtrd ⊢φ→voln*⁡∅⁡A=0