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

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 ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) ∈ V
3 df-ovol ⊢ vol* = ( 𝑥 ∈ 𝒫 ℝ ↦ inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) )
4 2 3 fnmpti ⊢ vol* Fn 𝒫 ℝ
5 elpwi ⊢ ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ )
6 ovolcl ⊢ ( 𝑥 ⊆ ℝ → ( vol* ‘ 𝑥 ) ∈ ℝ* )
7 ovolge0 ⊢ ( 𝑥 ⊆ ℝ → 0 ≤ ( vol* ‘ 𝑥 ) )
8 pnfge ⊢ ( ( vol* ‘ 𝑥 ) ∈ ℝ* → ( vol* ‘ 𝑥 ) ≤ +∞ )
9 6 8 syl ⊢ ( 𝑥 ⊆ ℝ → ( vol* ‘ 𝑥 ) ≤ +∞ )
10 0xr ⊢ 0 ∈ ℝ*
11 pnfxr ⊢ +∞ ∈ ℝ*
12 elicc1 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( vol* ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( vol* ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( vol* ‘ 𝑥 ) ∧ ( vol* ‘ 𝑥 ) ≤ +∞ ) ) )
13 10 11 12 mp2an ⊢ ( ( vol* ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( vol* ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( vol* ‘ 𝑥 ) ∧ ( vol* ‘ 𝑥 ) ≤ +∞ ) )
14 6 7 9 13 syl3anbrc ⊢ ( 𝑥 ⊆ ℝ → ( vol* ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
15 5 14 syl ⊢ ( 𝑥 ∈ 𝒫 ℝ → ( vol* ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
16 15 rgen ⊢ ∀ 𝑥 ∈ 𝒫 ℝ ( vol* ‘ 𝑥 ) ∈ ( 0 [,] +∞ )
17 ffnfv ⊢ ( vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ ) ↔ ( vol* Fn 𝒫 ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( vol* ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) )
18 4 16 17 mpbir2an ⊢ vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ )