# 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 e. ( dom vol MblFnM BrSiga ) -> F : RR --> RR )`

### Proof

Step Hyp Ref Expression
1 dmvlsiga
` |-  dom vol e. ( sigAlgebra ` RR )`
2 issgon
` |-  ( dom vol e. ( sigAlgebra ` RR ) <-> ( dom vol e. U. ran sigAlgebra /\ RR = U. dom vol ) )`
3 1 2 mpbi
` |-  ( dom vol e. U. ran sigAlgebra /\ RR = U. dom vol )`
4 3 simpli
` |-  dom vol e. U. ran sigAlgebra`
5 4 a1i
` |-  ( F e. ( dom vol MblFnM BrSiga ) -> dom vol e. U. ran sigAlgebra )`
6 brsigarn
` |-  BrSiga e. ( sigAlgebra ` RR )`
7 issgon
` |-  ( BrSiga e. ( sigAlgebra ` RR ) <-> ( BrSiga e. U. ran sigAlgebra /\ RR = U. BrSiga ) )`
8 6 7 mpbi
` |-  ( BrSiga e. U. ran sigAlgebra /\ RR = U. BrSiga )`
9 8 simpli
` |-  BrSiga e. U. ran sigAlgebra`
10 9 a1i
` |-  ( F e. ( dom vol MblFnM BrSiga ) -> BrSiga e. U. ran sigAlgebra )`
11 id
` |-  ( F e. ( dom vol MblFnM BrSiga ) -> F e. ( dom vol MblFnM BrSiga ) )`
12 5 10 11 mbfmf
` |-  ( F e. ( dom vol MblFnM BrSiga ) -> F : U. dom vol --> U. BrSiga )`
13 3 simpri
` |-  RR = U. dom vol`
14 8 simpri
` |-  RR = U. BrSiga`
15 13 14 feq23i
` |-  ( F : RR --> RR <-> F : U. dom vol --> U. BrSiga )`
16 12 15 sylibr
` |-  ( F e. ( dom vol MblFnM BrSiga ) -> F : RR --> RR )`