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

Theorem iblmbf 19117
Description: An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.)
Assertion
Ref Expression
iblmbf  |-  ( F  e.  L ^1  ->  F  e. MblFn )
Dummy variables  f 
k  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem iblmbf
StepHypRef Expression
1 df-ibl 18973 . . 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 3260 . . 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 3210 . 2  |-  L ^1  C_ MblFn
43sseli 3178 1  |-  ( F  e.  L ^1  ->  F  e. MblFn )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1685   A.wral 2545   {crab 2549   [_csb 3083   ifcif 3567   class class class wbr 4025    e. cmpt 4079   dom cdm 4689   ` cfv 5222  (class class class)co 5820   RRcr 8732   0cc0 8733   _ici 8735    <_ cle 8864    / cdiv 9419   3c3 9792   ...cfz 10777   ^cexp 11099   Recre 11577  MblFncmbf 18964   S.2citg2 18966   L ^1cibl 18967
This theorem is referenced by:  iblcnlem  19138  itgcnlem  19139  itgcnval  19149  itgre  19150  itgim  19151  iblneg  19152  itgneg  19153  iblss  19154  iblss2  19155  itgge0  19160  itgss3  19164  itgless  19166  iblsub  19171  itgadd  19174  itgsub  19175  itgfsum  19176  iblabs  19178  iblmulc2  19180  itgmulc2  19183  itgabs  19184  itgsplit  19185  bddmulibl  19188  itggt0  19191  itgcn  19192  ditgswap  19204  ditgsplitlem  19205  ftc1a  19379  itgsubstlem  19390  iblulm  19778  itgulm  19779
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-in 3161  df-ss 3168  df-ibl 18973
  Copyright terms: Public domain W3C validator