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 \in (dom vol {MblFn}_{μ} 𝔅_{ℝ}) \to F : ℝ ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		dmvlsiga	$⊢ dom vol \in sigAlgebra (ℝ)$
2		issgon	$⊢ dom vol \in sigAlgebra (ℝ) \leftrightarrow (dom vol \in ⋃ ran sigAlgebra \land ℝ = ⋃ dom vol)$
3	1 2	mpbi	$⊢ (dom vol \in ⋃ ran sigAlgebra \land ℝ = ⋃ dom vol)$
4	3	simpli	$⊢ dom vol \in ⋃ ran sigAlgebra$
5	4	a1i	$⊢ F \in (dom vol {MblFn}_{μ} 𝔅_{ℝ}) \to dom vol \in ⋃ ran sigAlgebra$
6		brsigarn	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ)$
7		issgon	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ) \leftrightarrow (𝔅_{ℝ} \in ⋃ ran sigAlgebra \land ℝ = ⋃ 𝔅_{ℝ})$
8	6 7	mpbi	$⊢ (𝔅_{ℝ} \in ⋃ ran sigAlgebra \land ℝ = ⋃ 𝔅_{ℝ})$
9	8	simpli	$⊢ 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
10	9	a1i	$⊢ F \in (dom vol {MblFn}_{μ} 𝔅_{ℝ}) \to 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
11		id	$⊢ F \in (dom vol {MblFn}_{μ} 𝔅_{ℝ}) \to F \in (dom vol {MblFn}_{μ} 𝔅_{ℝ})$
12	5 10 11	mbfmf	$⊢ F \in (dom vol {MblFn}_{μ} 𝔅_{ℝ}) \to F : ⋃ dom vol ⟶ ⋃ 𝔅_{ℝ}$
13	3	simpri	$⊢ ℝ = ⋃ dom vol$
14	8	simpri	$⊢ ℝ = ⋃ 𝔅_{ℝ}$
15	13 14	feq23i	$⊢ F : ℝ ⟶ ℝ \leftrightarrow F : ⋃ dom vol ⟶ ⋃ 𝔅_{ℝ}$
16	12 15	sylibr	$⊢ F \in (dom vol {MblFn}_{μ} 𝔅_{ℝ}) \to F : ℝ ⟶ ℝ$