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 𝔅ℝ ) → 𝐹 : ℝ ⟶ ℝ )