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

Theorem iblmbf 22152
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 22009 . . 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 3570 . . 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 3519 . 2  |-  L^1 
C_ MblFn
43sseli 3485 1  |-  ( F  e.  L^1  ->  F  e. MblFn )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804   A.wral 2793   {crab 2797   [_csb 3420   ifcif 3926   class class class wbr 4437    |-> cmpt 4495   dom cdm 4989   ` cfv 5578  (class class class)co 6281   RRcr 9494   0cc0 9495   _ici 9497    <_ cle 9632    / cdiv 10213   3c3 10593   ...cfz 11683   ^cexp 12148   Recre 12912  MblFncmbf 22001   S.2citg2 22003   L^1cibl 22004
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-in 3468  df-ss 3475  df-ibl 22009
This theorem is referenced by:  iblcnlem  22173  itgcnlem  22174  itgcnval  22184  itgre  22185  itgim  22186  iblneg  22187  itgneg  22188  iblss  22189  iblss2  22190  itgge0  22195  itgss3  22199  itgless  22201  iblsub  22206  itgadd  22209  itgsub  22210  itgfsum  22211  iblabs  22213  iblmulc2  22215  itgmulc2  22218  itgabs  22219  itgsplit  22220  bddmulibl  22223  itggt0  22226  itgcn  22227  ditgswap  22241  ditgsplitlem  22242  ftc1a  22416  itgsubstlem  22427  iblulm  22780  itgulm  22781  ibladdnc  30048  itgaddnclem1  30049  itgaddnclem2  30050  itgaddnc  30051  iblsubnc  30052  itgsubnc  30053  iblabsnclem  30054  iblabsnc  30055  iblmulc2nc  30056  itgmulc2nclem2  30058  itgmulc2nc  30059  itgabsnc  30060  ftc1cnnclem  30064  ftc1anclem2  30067  ftc1anclem4  30069  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem8  30073
  Copyright terms: Public domain W3C validator