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