Metamath Proof Explorer

Theorem ovolf

Description: The domain and codomain of the outer volume function. (Contributed by Mario Carneiro, 16-Mar-2014) (Proof shortened by AV, 17-Sep-2020)

Ref Expression
Assertion ovolf ⊢ vol * : 𝒫 ℝ ⟶ 0 +∞

Proof

Step Hyp Ref Expression
1 xrltso ⊢ < Or ℝ *
2 1 infex ⊢ inf y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ℝ * < ∈ V
3 df-ovol ⊢ vol * = x ∈ 𝒫 ℝ ⟼ inf y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ℝ * <
4 2 3 fnmpti ⊢ vol * Fn 𝒫 ℝ
5 elpwi ⊢ x ∈ 𝒫 ℝ → x ⊆ ℝ
6 ovolcl ⊢ x ⊆ ℝ → vol * ⁡ x ∈ ℝ *
7 ovolge0 ⊢ x ⊆ ℝ → 0 ≤ vol * ⁡ x
8 pnfge ⊢ vol * ⁡ x ∈ ℝ * → vol * ⁡ x ≤ +∞
9 6 8 syl ⊢ x ⊆ ℝ → vol * ⁡ x ≤ +∞
10 0xr ⊢ 0 ∈ ℝ *
11 pnfxr ⊢ +∞ ∈ ℝ *
12 elicc1 ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * → vol * ⁡ x ∈ 0 +∞ ↔ vol * ⁡ x ∈ ℝ * ∧ 0 ≤ vol * ⁡ x ∧ vol * ⁡ x ≤ +∞
13 10 11 12 mp2an ⊢ vol * ⁡ x ∈ 0 +∞ ↔ vol * ⁡ x ∈ ℝ * ∧ 0 ≤ vol * ⁡ x ∧ vol * ⁡ x ≤ +∞
14 6 7 9 13 syl3anbrc ⊢ x ⊆ ℝ → vol * ⁡ x ∈ 0 +∞
15 5 14 syl ⊢ x ∈ 𝒫 ℝ → vol * ⁡ x ∈ 0 +∞
16 15 rgen ⊢ ∀ x ∈ 𝒫 ℝ vol * ⁡ x ∈ 0 +∞
17 ffnfv ⊢ vol * : 𝒫 ℝ ⟶ 0 +∞ ↔ vol * Fn 𝒫 ℝ ∧ ∀ x ∈ 𝒫 ℝ vol * ⁡ x ∈ 0 +∞
18 4 16 17 mpbir2an ⊢ vol * : 𝒫 ℝ ⟶ 0 +∞