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 +∞