Theorem iblmbf 25895

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.

Step	Hyp	Ref	Expression
1		df-ibl 25750	. . 3 ⊢ 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
2	1	ssrab3 4042	. 2 ⊢ 𝐿1 ⊆ MblFn
3	2	sseli 3939	1 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∀wral 3085  ⦋csb 3859  ifcif 4490   class class class wbr 5111   ↦ cmpt 5194  dom cdm 5662  ‘cfv 6537  (class class class)co 7411  ℝcr 11099  0cc0 11100  ici 11102   ≤ cle 11244   / cdiv 11871  3c3 12296  ...cfz 13535  ↑cexp 14097  ℜcre 15148  MblFncmbf 25742  ∫₂citg2 25744  𝐿¹cibl 25745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-ss 3928  df-ibl 25750

This theorem is referenced by:  iblcnlem  25917  itgcnlem  25918  itgcnval  25928  itgre  25929  itgim  25930  iblneg  25931  itgneg  25932  iblss  25933  iblss2  25934  itgge0  25939  itgss3  25943  itgless  25945  iblsub  25950  itgadd  25953  itgsub  25954  itgfsum  25955  iblabs  25957  iblmulc2  25959  itgmulc2  25962  itgabs  25963  itgsplit  25964  bddmulibl  25967  itggt0  25972  itgcn  25973  ditgswap  25987  ditgsplitlem  25988  ftc1a  26165  itgsubstlem  26176  iblulm  26536  itgulm  26537  ibladdnc  38251  itgaddnclem1  38252  itgaddnclem2  38253  itgaddnc  38254  iblsubnc  38255  itgsubnc  38256  iblabsnclem  38257  iblabsnc  38258  iblmulc2nc  38259  itgmulc2nclem2  38261  itgmulc2nc  38262  itgabsnc  38263  ftc1cnnclem  38265  ftc1anclem2  38268  ftc1anclem4  38270  ftc1anclem5  38271  ftc1anclem6  38272  ftc1anclem8  38274