# Metamath Proof Explorer

## Theorem volf

Description: The domain and range of the Lebesgue measure function. (Contributed by Mario Carneiro, 19-Mar-2014)

Ref Expression
Assertion volf ${⊢}vol:\mathrm{dom}vol⟶\left[0,\mathrm{+\infty }\right]$

### Proof

Step Hyp Ref Expression
1 ovolf ${⊢}{vol}^{*}:𝒫ℝ⟶\left[0,\mathrm{+\infty }\right]$
2 ffun ${⊢}{vol}^{*}:𝒫ℝ⟶\left[0,\mathrm{+\infty }\right]\to \mathrm{Fun}{vol}^{*}$
3 funres ${⊢}\mathrm{Fun}{vol}^{*}\to \mathrm{Fun}\left({{vol}^{*}↾}_{\mathrm{dom}vol}\right)$
4 1 2 3 mp2b ${⊢}\mathrm{Fun}\left({{vol}^{*}↾}_{\mathrm{dom}vol}\right)$
5 volres ${⊢}vol={{vol}^{*}↾}_{\mathrm{dom}vol}$
6 5 funeqi ${⊢}\mathrm{Fun}vol↔\mathrm{Fun}\left({{vol}^{*}↾}_{\mathrm{dom}vol}\right)$
7 4 6 mpbir ${⊢}\mathrm{Fun}vol$
8 resss ${⊢}{{vol}^{*}↾}_{\mathrm{dom}vol}\subseteq {vol}^{*}$
9 5 8 eqsstri ${⊢}vol\subseteq {vol}^{*}$
10 fssxp ${⊢}{vol}^{*}:𝒫ℝ⟶\left[0,\mathrm{+\infty }\right]\to {vol}^{*}\subseteq 𝒫ℝ×\left[0,\mathrm{+\infty }\right]$
11 1 10 ax-mp ${⊢}{vol}^{*}\subseteq 𝒫ℝ×\left[0,\mathrm{+\infty }\right]$
12 9 11 sstri ${⊢}vol\subseteq 𝒫ℝ×\left[0,\mathrm{+\infty }\right]$
13 7 12 pm3.2i ${⊢}\left(\mathrm{Fun}vol\wedge vol\subseteq 𝒫ℝ×\left[0,\mathrm{+\infty }\right]\right)$
14 funssxp ${⊢}\left(\mathrm{Fun}vol\wedge vol\subseteq 𝒫ℝ×\left[0,\mathrm{+\infty }\right]\right)↔\left(vol:\mathrm{dom}vol⟶\left[0,\mathrm{+\infty }\right]\wedge \mathrm{dom}vol\subseteq 𝒫ℝ\right)$
15 13 14 mpbi ${⊢}\left(vol:\mathrm{dom}vol⟶\left[0,\mathrm{+\infty }\right]\wedge \mathrm{dom}vol\subseteq 𝒫ℝ\right)$
16 15 simpli ${⊢}vol:\mathrm{dom}vol⟶\left[0,\mathrm{+\infty }\right]$