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

Theorem iblmbf 21267
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 21124 . . 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 3458 . . 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 3407 . 2  |-  L^1 
C_ MblFn
43sseli 3373 1  |-  ( F  e.  L^1  ->  F  e. MblFn )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   A.wral 2736   {crab 2740   [_csb 3309   ifcif 3812   class class class wbr 4313    e. cmpt 4371   dom cdm 4861   ` cfv 5439  (class class class)co 6112   RRcr 9302   0cc0 9303   _ici 9305    <_ cle 9440    / cdiv 10014   3c3 10393   ...cfz 11458   ^cexp 11886   Recre 12607  MblFncmbf 21116   S.2citg2 21118   L^1cibl 21119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-in 3356  df-ss 3363  df-ibl 21124
This theorem is referenced by:  iblcnlem  21288  itgcnlem  21289  itgcnval  21299  itgre  21300  itgim  21301  iblneg  21302  itgneg  21303  iblss  21304  iblss2  21305  itgge0  21310  itgss3  21314  itgless  21316  iblsub  21321  itgadd  21324  itgsub  21325  itgfsum  21326  iblabs  21328  iblmulc2  21330  itgmulc2  21333  itgabs  21334  itgsplit  21335  bddmulibl  21338  itggt0  21341  itgcn  21342  ditgswap  21356  ditgsplitlem  21357  ftc1a  21531  itgsubstlem  21542  iblulm  21894  itgulm  21895  ibladdnc  28475  itgaddnclem1  28476  itgaddnclem2  28477  itgaddnc  28478  iblsubnc  28479  itgsubnc  28480  iblabsnclem  28481  iblabsnc  28482  iblmulc2nc  28483  itgmulc2nclem2  28485  itgmulc2nc  28486  itgabsnc  28487  ftc1cnnclem  28491  ftc1anclem2  28494  ftc1anclem4  28496  ftc1anclem5  28497  ftc1anclem6  28498  ftc1anclem8  28500
  Copyright terms: Public domain W3C validator