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

Theorem iblmbf 25135
Description: An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.)
Assertion
Ref Expression
iblmbf (š¹ āˆˆ šæ1 ā†’ š¹ āˆˆ MblFn)

Proof of Theorem iblmbf
Dummy variables š‘“ š‘˜ š‘„ š‘¦ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ibl 24989 . . 3 šæ1 = {š‘“ āˆˆ MblFn āˆ£ āˆ€š‘˜ āˆˆ (0...3)(āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ ā¦‹(ā„œā€˜((š‘“ā€˜š‘„) / (iā†‘š‘˜))) / š‘¦ā¦Œif((š‘„ āˆˆ dom š‘“ āˆ§ 0 ā‰¤ š‘¦), š‘¦, 0))) āˆˆ ā„}
21ssrab3 4041 . 2 šæ1 āŠ† MblFn
32sseli 3941 1 (š¹ āˆˆ šæ1 ā†’ š¹ āˆˆ MblFn)
Colors of variables: wff setvar class
Syntax hints:   ā†’ wi 4   āˆ§ wa 397   āˆˆ wcel 2107  āˆ€wral 3065  ā¦‹csb 3856  ifcif 4487   class class class wbr 5106   ā†¦ cmpt 5189  dom cdm 5634  ā€˜cfv 6497  (class class class)co 7358  ā„cr 11051  0cc0 11052  ici 11054   ā‰¤ cle 11191   / cdiv 11813  3c3 12210  ...cfz 13425  ā†‘cexp 13968  ā„œcre 14983  MblFncmbf 24981  āˆ«2citg2 24983  šæ1cibl 24984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-in 3918  df-ss 3928  df-ibl 24989
This theorem is referenced by:  iblcnlem  25156  itgcnlem  25157  itgcnval  25167  itgre  25168  itgim  25169  iblneg  25170  itgneg  25171  iblss  25172  iblss2  25173  itgge0  25178  itgss3  25182  itgless  25184  iblsub  25189  itgadd  25192  itgsub  25193  itgfsum  25194  iblabs  25196  iblmulc2  25198  itgmulc2  25201  itgabs  25202  itgsplit  25203  bddmulibl  25206  itggt0  25211  itgcn  25212  ditgswap  25226  ditgsplitlem  25227  ftc1a  25404  itgsubstlem  25415  iblulm  25769  itgulm  25770  ibladdnc  36138  itgaddnclem1  36139  itgaddnclem2  36140  itgaddnc  36141  iblsubnc  36142  itgsubnc  36143  iblabsnclem  36144  iblabsnc  36145  iblmulc2nc  36146  itgmulc2nclem2  36148  itgmulc2nc  36149  itgabsnc  36150  ftc1cnnclem  36152  ftc1anclem2  36155  ftc1anclem4  36157  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem8  36161
  Copyright terms: Public domain W3C validator