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

Theorem iblmbf 21086
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 20943 . . 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 3425 . . 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 3374 . 2  |-  L^1 
C_ MblFn
43sseli 3340 1  |-  ( F  e.  L^1  ->  F  e. MblFn )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1755   A.wral 2705   {crab 2709   [_csb 3276   ifcif 3779   class class class wbr 4280    e. cmpt 4338   dom cdm 4827   ` cfv 5406  (class class class)co 6080   RRcr 9268   0cc0 9269   _ici 9271    <_ cle 9406    / cdiv 9980   3c3 10359   ...cfz 11423   ^cexp 11848   Recre 12569  MblFncmbf 20935   S.2citg2 20937   L^1cibl 20938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-in 3323  df-ss 3330  df-ibl 20943
This theorem is referenced by:  iblcnlem  21107  itgcnlem  21108  itgcnval  21118  itgre  21119  itgim  21120  iblneg  21121  itgneg  21122  iblss  21123  iblss2  21124  itgge0  21129  itgss3  21133  itgless  21135  iblsub  21140  itgadd  21143  itgsub  21144  itgfsum  21145  iblabs  21147  iblmulc2  21149  itgmulc2  21152  itgabs  21153  itgsplit  21154  bddmulibl  21157  itggt0  21160  itgcn  21161  ditgswap  21175  ditgsplitlem  21176  ftc1a  21350  itgsubstlem  21361  iblulm  21756  itgulm  21757  ibladdnc  28290  itgaddnclem1  28291  itgaddnclem2  28292  itgaddnc  28293  iblsubnc  28294  itgsubnc  28295  iblabsnclem  28296  iblabsnc  28297  iblmulc2nc  28298  itgmulc2nclem2  28300  itgmulc2nc  28301  itgabsnc  28302  ftc1cnnclem  28306  ftc1anclem2  28309  ftc1anclem4  28311  ftc1anclem5  28312  ftc1anclem6  28313  ftc1anclem8  28315
  Copyright terms: Public domain W3C validator