Metamath Proof Explorer

Theorem mbfmvolf

Description: Measurable functions with respect to the Lebesgue measure are real-valued functions on the real numbers. (Contributed by Thierry Arnoux, 27-Mar-2017)

Ref Expression
Assertion mbfmvolf ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → F : ℝ ⟶ ℝ

Proof

Step Hyp Ref Expression
1 dmvlsiga ⊢ dom ⁡ vol ∈ sigAlgebra ⁡ ℝ
2 issgon ⊢ dom ⁡ vol ∈ sigAlgebra ⁡ ℝ ↔ dom ⁡ vol ∈ ⋃ ran ⁡ sigAlgebra ∧ ℝ = ⋃ dom ⁡ vol
3 1 2 mpbi ⊢ dom ⁡ vol ∈ ⋃ ran ⁡ sigAlgebra ∧ ℝ = ⋃ dom ⁡ vol
4 3 simpli ⊢ dom ⁡ vol ∈ ⋃ ran ⁡ sigAlgebra
5 4 a1i ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → dom ⁡ vol ∈ ⋃ ran ⁡ sigAlgebra
6 brsigarn ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ
7 issgon ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ ↔ 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra ∧ ℝ = ⋃ 𝔅 ℝ
8 6 7 mpbi ⊢ 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra ∧ ℝ = ⋃ 𝔅 ℝ
9 8 simpli ⊢ 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
10 9 a1i ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
11 id ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ
12 5 10 11 mbfmf ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → F : ⋃ dom ⁡ vol ⟶ ⋃ 𝔅 ℝ
13 3 simpri ⊢ ℝ = ⋃ dom ⁡ vol
14 8 simpri ⊢ ℝ = ⋃ 𝔅 ℝ
15 13 14 feq23i ⊢ F : ℝ ⟶ ℝ ↔ F : ⋃ dom ⁡ vol ⟶ ⋃ 𝔅 ℝ
16 12 15 sylibr ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → F : ℝ ⟶ ℝ