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 [,] +∞ )