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 )