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