Metamath Proof Explorer

Theorem ovn02

Description: For the zero-dimensional space, voln* assigns zero to every subset. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion ovn02 ⊢ voln* ⁡ ∅ = x ∈ 𝒫 ∅ ⟼ 0

Proof

Step Hyp Ref Expression
1 tru ⊢ ⊤
2 0fi ⊢ ∅ ∈ Fin
3 2 a1i ⊢ ⊤ → ∅ ∈ Fin
4 3 ovnf ⊢ ⊤ → voln* ⁡ ∅ : 𝒫 ℝ ∅ ⟶ 0 +∞
5 4 feqmptd ⊢ ⊤ → voln* ⁡ ∅ = x ∈ 𝒫 ℝ ∅ ⟼ voln* ⁡ ∅ ⁡ x
6 1 5 ax-mp ⊢ voln* ⁡ ∅ = x ∈ 𝒫 ℝ ∅ ⟼ voln* ⁡ ∅ ⁡ x
7 reex ⊢ ℝ ∈ V
8 mapdm0 ⊢ ℝ ∈ V → ℝ ∅ = ∅
9 7 8 ax-mp ⊢ ℝ ∅ = ∅
10 9 pweqi ⊢ 𝒫 ℝ ∅ = 𝒫 ∅
11 mpteq1 ⊢ 𝒫 ℝ ∅ = 𝒫 ∅ → x ∈ 𝒫 ℝ ∅ ⟼ voln* ⁡ ∅ ⁡ x = x ∈ 𝒫 ∅ ⟼ voln* ⁡ ∅ ⁡ x
12 10 11 ax-mp ⊢ x ∈ 𝒫 ℝ ∅ ⟼ voln* ⁡ ∅ ⁡ x = x ∈ 𝒫 ∅ ⟼ voln* ⁡ ∅ ⁡ x
13 elpwi ⊢ x ∈ 𝒫 ∅ → x ⊆ ∅
14 9 eqcomi ⊢ ∅ = ℝ ∅
15 14 a1i ⊢ x ∈ 𝒫 ∅ → ∅ = ℝ ∅
16 13 15 sseqtrd ⊢ x ∈ 𝒫 ∅ → x ⊆ ℝ ∅
17 16 ovn0val ⊢ x ∈ 𝒫 ∅ → voln* ⁡ ∅ ⁡ x = 0
18 17 mpteq2ia ⊢ x ∈ 𝒫 ∅ ⟼ voln* ⁡ ∅ ⁡ x = x ∈ 𝒫 ∅ ⟼ 0
19 6 12 18 3eqtri ⊢ voln* ⁡ ∅ = x ∈ 𝒫 ∅ ⟼ 0