MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iblmbf Unicode version

Theorem iblmbf 19122
Description: An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.)
Assertion
Ref Expression
iblmbf  |-  ( F  e.  L ^1  ->  F  e. MblFn )

Proof of Theorem iblmbf
Dummy variables  f 
k  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ibl 18978 . . 3  |-  L ^1  =  { f  e. MblFn  |  A. k  e.  ( 0 ... 3 ) ( S.2 `  (
x  e.  RR  |->  [_ ( Re `  ( ( f `  x )  /  ( _i ^
k ) ) )  /  y ]_ if ( ( x  e. 
dom  f  /\  0  <_  y ) ,  y ,  0 ) ) )  e.  RR }
2 ssrab2 3258 . . 3  |-  { f  e. MblFn  |  A. k  e.  ( 0 ... 3
) ( S.2 `  (
x  e.  RR  |->  [_ ( Re `  ( ( f `  x )  /  ( _i ^
k ) ) )  /  y ]_ if ( ( x  e. 
dom  f  /\  0  <_  y ) ,  y ,  0 ) ) )  e.  RR }  C_ MblFn
31, 2eqsstri 3208 . 2  |-  L ^1  C_ MblFn
43sseli 3176 1  |-  ( F  e.  L ^1  ->  F  e. MblFn )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   A.wral 2543   {crab 2547   [_csb 3081   ifcif 3565   class class class wbr 4023    e. cmpt 4077   dom cdm 4689   ` cfv 5255  (class class class)co 5858   RRcr 8736   0cc0 8737   _ici 8739    <_ cle 8868    / cdiv 9423   3c3 9796   ...cfz 10782   ^cexp 11104   Recre 11582  MblFncmbf 18969   S.2citg2 18971   L ^1cibl 18972
This theorem is referenced by:  iblcnlem  19143  itgcnlem  19144  itgcnval  19154  itgre  19155  itgim  19156  iblneg  19157  itgneg  19158  iblss  19159  iblss2  19160  itgge0  19165  itgss3  19169  itgless  19171  iblsub  19176  itgadd  19179  itgsub  19180  itgfsum  19181  iblabs  19183  iblmulc2  19185  itgmulc2  19188  itgabs  19189  itgsplit  19190  bddmulibl  19193  itggt0  19196  itgcn  19197  ditgswap  19209  ditgsplitlem  19210  ftc1a  19384  itgsubstlem  19395  iblulm  19783  itgulm  19784
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-in 3159  df-ss 3166  df-ibl 18978
  Copyright terms: Public domain W3C validator