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 ( 𝐹 ∈ ( dom vol MblFnM 𝔅 ) → 𝐹 : ℝ ⟶ ℝ )

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 ( 𝐹 ∈ ( dom vol MblFnM 𝔅 ) → 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 ( 𝐹 ∈ ( dom vol MblFnM 𝔅 ) → 𝔅 ran sigAlgebra )
11 id ( 𝐹 ∈ ( dom vol MblFnM 𝔅 ) → 𝐹 ∈ ( dom vol MblFnM 𝔅 ) )
12 5 10 11 mbfmf ( 𝐹 ∈ ( dom vol MblFnM 𝔅 ) → 𝐹 : dom vol ⟶ 𝔅 )
13 3 simpri ℝ = dom vol
14 8 simpri ℝ = 𝔅
15 13 14 feq23i ( 𝐹 : ℝ ⟶ ℝ ↔ 𝐹 : dom vol ⟶ 𝔅 )
16 12 15 sylibr ( 𝐹 ∈ ( dom vol MblFnM 𝔅 ) → 𝐹 : ℝ ⟶ ℝ )