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

Metamath Proof Explorer

Theorem volf

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

Ref Expression
Assertion volf vol : dom vol ⟶ ( 0 [,] +∞ )

Proof

Step Hyp Ref Expression
1 ovolf ⊢ vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ )
2 ffun ⊢ ( vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ ) → Fun vol* )
3 funres ⊢ ( Fun vol* → Fun ( vol* ↾ dom vol ) )
4 1 2 3 mp2b ⊢ Fun ( vol* ↾ dom vol )
5 volres ⊢ vol = ( vol* ↾ dom vol )
6 5 funeqi ⊢ ( Fun vol ↔ Fun ( vol* ↾ dom vol ) )
7 4 6 mpbir ⊢ Fun vol
8 resss ⊢ ( vol* ↾ dom vol ) ⊆ vol*
9 5 8 eqsstri ⊢ vol ⊆ vol*
10 fssxp ⊢ ( vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ ) → vol* ⊆ ( 𝒫 ℝ × ( 0 [,] +∞ ) ) )
11 1 10 ax-mp ⊢ vol* ⊆ ( 𝒫 ℝ × ( 0 [,] +∞ ) )
12 9 11 sstri ⊢ vol ⊆ ( 𝒫 ℝ × ( 0 [,] +∞ ) )
13 7 12 pm3.2i ⊢ ( Fun vol ∧ vol ⊆ ( 𝒫 ℝ × ( 0 [,] +∞ ) ) )
14 funssxp ⊢ ( ( Fun vol ∧ vol ⊆ ( 𝒫 ℝ × ( 0 [,] +∞ ) ) ) ↔ ( vol : dom vol ⟶ ( 0 [,] +∞ ) ∧ dom vol ⊆ 𝒫 ℝ ) )
15 13 14 mpbi ⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) ∧ dom vol ⊆ 𝒫 ℝ )
16 15 simpli ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )