# 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 \left(\mathrm{dom}vol{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)\to {F}:ℝ⟶ℝ$

### Proof

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