# Metamath Proof Explorer

## Theorem ovolf

Description: The domain and range 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 $⊢ sup y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ x ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ℝ * < ∈ V$
3 df-ovol $⊢ vol * = x ∈ 𝒫 ℝ ⟼ sup 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 +∞$