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

Theorem iblmbf 21904
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 21761 . . 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 3580 . . 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 3529 . 2  |-  L^1 
C_ MblFn
43sseli 3495 1  |-  ( F  e.  L^1  ->  F  e. MblFn )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1762   A.wral 2809   {crab 2813   [_csb 3430   ifcif 3934   class class class wbr 4442    |-> cmpt 4500   dom cdm 4994   ` cfv 5581  (class class class)co 6277   RRcr 9482   0cc0 9483   _ici 9485    <_ cle 9620    / cdiv 10197   3c3 10577   ...cfz 11663   ^cexp 12124   Recre 12882  MblFncmbf 21753   S.2citg2 21755   L^1cibl 21756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818  df-in 3478  df-ss 3485  df-ibl 21761
This theorem is referenced by:  iblcnlem  21925  itgcnlem  21926  itgcnval  21936  itgre  21937  itgim  21938  iblneg  21939  itgneg  21940  iblss  21941  iblss2  21942  itgge0  21947  itgss3  21951  itgless  21953  iblsub  21958  itgadd  21961  itgsub  21962  itgfsum  21963  iblabs  21965  iblmulc2  21967  itgmulc2  21970  itgabs  21971  itgsplit  21972  bddmulibl  21975  itggt0  21978  itgcn  21979  ditgswap  21993  ditgsplitlem  21994  ftc1a  22168  itgsubstlem  22179  iblulm  22531  itgulm  22532  ibladdnc  29638  itgaddnclem1  29639  itgaddnclem2  29640  itgaddnc  29641  iblsubnc  29642  itgsubnc  29643  iblabsnclem  29644  iblabsnc  29645  iblmulc2nc  29646  itgmulc2nclem2  29648  itgmulc2nc  29649  itgabsnc  29650  ftc1cnnclem  29654  ftc1anclem2  29657  ftc1anclem4  29659  ftc1anclem5  29660  ftc1anclem6  29661  ftc1anclem8  29663
  Copyright terms: Public domain W3C validator