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 )