This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovolval

Description: The value of the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 17-Sep-2020)

Ref Expression
Hypothesis ovolval.1 ⊢ M = y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
Assertion ovolval ⊢ A ⊆ ℝ → vol * ⁡ A = inf M ℝ * <

Proof

Step Hyp Ref Expression
1 ovolval.1 ⊢ M = y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
2 reex ⊢ ℝ ∈ V
3 2 elpw2 ⊢ A ∈ 𝒫 ℝ ↔ A ⊆ ℝ
4 cleq1lem ⊢ x = A → x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ↔ A ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
5 4 rexbidv ⊢ x = A → ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ↔ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
6 5 rabbidv ⊢ x = A → y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < = y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <
7 6 1 eqtr4di ⊢ x = A → y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < = M
8 7 infeq1d ⊢ x = A → inf y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ℝ * < = inf M ℝ * <
9 df-ovol ⊢ vol * = x ∈ 𝒫 ℝ ⟼ inf y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ℝ * <
10 xrltso ⊢ < Or ℝ *
11 10 infex ⊢ inf M ℝ * < ∈ V
12 8 9 11 fvmpt ⊢ A ∈ 𝒫 ℝ → vol * ⁡ A = inf M ℝ * <
13 3 12 sylbir ⊢ A ⊆ ℝ → vol * ⁡ A = inf M ℝ * <