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