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

Theorem iblmbf 19647
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 19503 . . 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 3420 . . 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 3370 . 2  |-  L ^1  C_ MblFn
43sseli 3336 1  |-  ( F  e.  L ^1  ->  F  e. MblFn )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   A.wral 2697   {crab 2701   [_csb 3243   ifcif 3731   class class class wbr 4204    e. cmpt 4258   dom cdm 4869   ` cfv 5445  (class class class)co 6072   RRcr 8978   0cc0 8979   _ici 8981    <_ cle 9110    / cdiv 9666   3c3 10039   ...cfz 11032   ^cexp 11370   Recre 11890  MblFncmbf 19494   S.2citg2 19496   L ^1cibl 19497
This theorem is referenced by:  iblcnlem  19668  itgcnlem  19669  itgcnval  19679  itgre  19680  itgim  19681  iblneg  19682  itgneg  19683  iblss  19684  iblss2  19685  itgge0  19690  itgss3  19694  itgless  19696  iblsub  19701  itgadd  19704  itgsub  19705  itgfsum  19706  iblabs  19708  iblmulc2  19710  itgmulc2  19713  itgabs  19714  itgsplit  19715  bddmulibl  19718  itggt0  19721  itgcn  19722  ditgswap  19734  ditgsplitlem  19735  ftc1a  19909  itgsubstlem  19920  iblulm  20311  itgulm  20312  ibladdnc  26208  itgaddnclem1  26209  itgaddnclem2  26210  itgaddnc  26211  iblsubnc  26212  itgsubnc  26213  iblabsnclem  26214  iblabsnc  26215  iblmulc2nc  26216  itgmulc2nclem2  26218  itgmulc2nc  26219  itgabsnc  26220  ftc1cnnclem  26224
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-in 3319  df-ss 3326  df-ibl 19503
  Copyright terms: Public domain W3C validator