# Metamath Proof Explorer

## Theorem ovnval

Description: Value of the Lebesgue outer measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis ovnval.1 $⊢ φ → X ∈ Fin$
Assertion ovnval $⊢ φ → voln* ⁡ X = y ∈ 𝒫 ℝ X ⟼ if X = ∅ 0 sup z ∈ ℝ * | ∃ i ∈ ℝ 2 X ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * <$

### Proof

Step Hyp Ref Expression
1 ovnval.1 $⊢ φ → X ∈ Fin$
2 df-ovoln $⊢ voln* = x ∈ Fin ⟼ y ∈ 𝒫 ℝ x ⟼ if x = ∅ 0 sup z ∈ ℝ * | ∃ i ∈ ℝ 2 x ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * <$
3 oveq2 $⊢ x = X → ℝ x = ℝ X$
4 3 pweqd $⊢ x = X → 𝒫 ℝ x = 𝒫 ℝ X$
5 eqeq1 $⊢ x = X → x = ∅ ↔ X = ∅$
6 oveq2 $⊢ x = X → ℝ 2 x = ℝ 2 X$
7 6 oveq1d $⊢ x = X → ℝ 2 x ℕ = ℝ 2 X ℕ$
8 ixpeq1 $⊢ x = X → ⨉ k ∈ x . ∘ i ⁡ j ⁡ k = ⨉ k ∈ X . ∘ i ⁡ j ⁡ k$
9 8 iuneq2d $⊢ x = X → ⋃ j ∈ ℕ ⨉ k ∈ x . ∘ i ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k$
10 9 sseq2d $⊢ x = X → y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x . ∘ i ⁡ j ⁡ k ↔ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k$
11 simpl $⊢ x = X ∧ j ∈ ℕ → x = X$
12 11 prodeq1d $⊢ x = X ∧ j ∈ ℕ → ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k = ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k$
13 12 mpteq2dva $⊢ x = X → j ∈ ℕ ⟼ ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k = j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k$
14 13 fveq2d $⊢ x = X → sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k$
15 14 eqeq2d $⊢ x = X → z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k ↔ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k$
16 10 15 anbi12d $⊢ x = X → y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k ↔ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k$
17 7 16 rexeqbidv $⊢ x = X → ∃ i ∈ ℝ 2 x ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k ↔ ∃ i ∈ ℝ 2 X ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k$
18 17 rabbidv $⊢ x = X → z ∈ ℝ * | ∃ i ∈ ℝ 2 x ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k = z ∈ ℝ * | ∃ i ∈ ℝ 2 X ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k$
19 18 infeq1d $⊢ x = X → sup z ∈ ℝ * | ∃ i ∈ ℝ 2 x ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * < = sup z ∈ ℝ * | ∃ i ∈ ℝ 2 X ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * <$
20 5 19 ifbieq2d $⊢ x = X → if x = ∅ 0 sup z ∈ ℝ * | ∃ i ∈ ℝ 2 x ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * < = if X = ∅ 0 sup z ∈ ℝ * | ∃ i ∈ ℝ 2 X ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * <$
21 4 20 mpteq12dv $⊢ x = X → y ∈ 𝒫 ℝ x ⟼ if x = ∅ 0 sup z ∈ ℝ * | ∃ i ∈ ℝ 2 x ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ x vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * < = y ∈ 𝒫 ℝ X ⟼ if X = ∅ 0 sup z ∈ ℝ * | ∃ i ∈ ℝ 2 X ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * <$
22 ovex $⊢ ℝ X ∈ V$
23 22 pwex $⊢ 𝒫 ℝ X ∈ V$
24 23 mptex $⊢ y ∈ 𝒫 ℝ X ⟼ if X = ∅ 0 sup z ∈ ℝ * | ∃ i ∈ ℝ 2 X ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * < ∈ V$
25 24 a1i $⊢ φ → y ∈ 𝒫 ℝ X ⟼ if X = ∅ 0 sup z ∈ ℝ * | ∃ i ∈ ℝ 2 X ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * < ∈ V$
26 2 21 1 25 fvmptd3 $⊢ φ → voln* ⁡ X = y ∈ 𝒫 ℝ X ⟼ if X = ∅ 0 sup z ∈ ℝ * | ∃ i ∈ ℝ 2 X ℕ y ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X . ∘ i ⁡ j ⁡ k ∧ z = sum^ ⁡ j ∈ ℕ ⟼ ∏ k ∈ X vol ⁡ . ∘ i ⁡ j ⁡ k ℝ * <$