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

Theorem iblmbf 19226
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 19082 . . 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 3334 . . 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 3284 . 2  |-  L ^1  C_ MblFn
43sseli 3252 1  |-  ( F  e.  L ^1  ->  F  e. MblFn )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1710   A.wral 2619   {crab 2623   [_csb 3157   ifcif 3641   class class class wbr 4104    e. cmpt 4158   dom cdm 4771   ` cfv 5337  (class class class)co 5945   RRcr 8826   0cc0 8827   _ici 8829    <_ cle 8958    / cdiv 9513   3c3 9886   ...cfz 10874   ^cexp 11197   Recre 11678  MblFncmbf 19073   S.2citg2 19075   L ^1cibl 19076
This theorem is referenced by:  iblcnlem  19247  itgcnlem  19248  itgcnval  19258  itgre  19259  itgim  19260  iblneg  19261  itgneg  19262  iblss  19263  iblss2  19264  itgge0  19269  itgss3  19273  itgless  19275  iblsub  19280  itgadd  19283  itgsub  19284  itgfsum  19285  iblabs  19287  iblmulc2  19289  itgmulc2  19292  itgabs  19293  itgsplit  19294  bddmulibl  19297  itggt0  19300  itgcn  19301  ditgswap  19313  ditgsplitlem  19314  ftc1a  19488  itgsubstlem  19499  iblulm  19890  itgulm  19891  ibladdnc  25497  itgaddnclem1  25498  itgaddnclem2  25499  itgaddnc  25500  iblsubnc  25501  itgsubnc  25502  iblabsnclem  25503  iblabsnc  25504  iblmulc2nc  25505  itgmulc2nclem2  25507  itgmulc2nc  25508  itgabsnc  25509  ftc1cnnclem  25513
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-in 3235  df-ss 3242  df-ibl 19082
  Copyright terms: Public domain W3C validator