Metamath Proof Explorer


Theorem elmbfmvol2

Description: Measurable functions with respect to the Lebesgue measure. We only have the inclusion, since MblFn includes complex-valued functions. (Contributed by Thierry Arnoux, 26-Jan-2017)

Ref Expression
Assertion elmbfmvol2
|- ( F e. ( dom vol MblFnM BrSiga ) -> F e. MblFn )

Proof

Step Hyp Ref Expression
1 retopbas
 |-  ran (,) e. TopBases
2 bastg
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
3 1 2 ax-mp
 |-  ran (,) C_ ( topGen ` ran (,) )
4 retop
 |-  ( topGen ` ran (,) ) e. Top
5 sssigagen
 |-  ( ( topGen ` ran (,) ) e. Top -> ( topGen ` ran (,) ) C_ ( sigaGen ` ( topGen ` ran (,) ) ) )
6 4 5 ax-mp
 |-  ( topGen ` ran (,) ) C_ ( sigaGen ` ( topGen ` ran (,) ) )
7 3 6 sstri
 |-  ran (,) C_ ( sigaGen ` ( topGen ` ran (,) ) )
8 df-brsiga
 |-  BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
9 7 8 sseqtrri
 |-  ran (,) C_ BrSiga
10 eqid
 |-  vol = vol
11 dmvlsiga
 |-  dom vol e. ( sigAlgebra ` RR )
12 elrnsiga
 |-  ( dom vol e. ( sigAlgebra ` RR ) -> dom vol e. U. ran sigAlgebra )
13 11 12 mp1i
 |-  ( vol = vol -> dom vol e. U. ran sigAlgebra )
14 brsigarn
 |-  BrSiga e. ( sigAlgebra ` RR )
15 elrnsiga
 |-  ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra )
16 14 15 mp1i
 |-  ( vol = vol -> BrSiga e. U. ran sigAlgebra )
17 13 16 ismbfm
 |-  ( vol = vol -> ( F e. ( dom vol MblFnM BrSiga ) <-> ( F e. ( U. BrSiga ^m U. dom vol ) /\ A. x e. BrSiga ( `' F " x ) e. dom vol ) ) )
18 10 17 ax-mp
 |-  ( F e. ( dom vol MblFnM BrSiga ) <-> ( F e. ( U. BrSiga ^m U. dom vol ) /\ A. x e. BrSiga ( `' F " x ) e. dom vol ) )
19 18 simprbi
 |-  ( F e. ( dom vol MblFnM BrSiga ) -> A. x e. BrSiga ( `' F " x ) e. dom vol )
20 ssralv
 |-  ( ran (,) C_ BrSiga -> ( A. x e. BrSiga ( `' F " x ) e. dom vol -> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
21 9 19 20 mpsyl
 |-  ( F e. ( dom vol MblFnM BrSiga ) -> A. x e. ran (,) ( `' F " x ) e. dom vol )
22 18 simplbi
 |-  ( F e. ( dom vol MblFnM BrSiga ) -> F e. ( U. BrSiga ^m U. dom vol ) )
23 elmapi
 |-  ( F e. ( RR ^m RR ) -> F : RR --> RR )
24 unibrsiga
 |-  U. BrSiga = RR
25 unidmvol
 |-  U. dom vol = RR
26 24 25 oveq12i
 |-  ( U. BrSiga ^m U. dom vol ) = ( RR ^m RR )
27 23 26 eleq2s
 |-  ( F e. ( U. BrSiga ^m U. dom vol ) -> F : RR --> RR )
28 ismbf
 |-  ( F : RR --> RR -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
29 22 27 28 3syl
 |-  ( F e. ( dom vol MblFnM BrSiga ) -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
30 21 29 mpbird
 |-  ( F e. ( dom vol MblFnM BrSiga ) -> F e. MblFn )