Theorem iblmbf 24371

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 24226	. . 3 ⊢ 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
2	1	ssrab3 4008	. 2 ⊢ 𝐿1 ⊆ MblFn
3	2	sseli 3911	1 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3106  ⦋csb 3828  ifcif 4425   class class class wbr 5030   ↦ cmpt 5110  dom cdm 5519  ‘cfv 6324  (class class class)co 7135  ℝcr 10525  0cc0 10526  ici 10528   ≤ cle 10665   / cdiv 11286  3c3 11681  ...cfz 12885  ↑cexp 13425  ℜcre 14448  MblFncmbf 24218  ∫₂citg2 24220  𝐿¹cibl 24221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-ibl 24226

This theorem is referenced by:  iblcnlem  24392  itgcnlem  24393  itgcnval  24403  itgre  24404  itgim  24405  iblneg  24406  itgneg  24407  iblss  24408  iblss2  24409  itgge0  24414  itgss3  24418  itgless  24420  iblsub  24425  itgadd  24428  itgsub  24429  itgfsum  24430  iblabs  24432  iblmulc2  24434  itgmulc2  24437  itgabs  24438  itgsplit  24439  bddmulibl  24442  itggt0  24447  itgcn  24448  ditgswap  24462  ditgsplitlem  24463  ftc1a  24640  itgsubstlem  24651  iblulm  25002  itgulm  25003  ibladdnc  35114  itgaddnclem1  35115  itgaddnclem2  35116  itgaddnc  35117  iblsubnc  35118  itgsubnc  35119  iblabsnclem  35120  iblabsnc  35121  iblmulc2nc  35122  itgmulc2nclem2  35124  itgmulc2nc  35125  itgabsnc  35126  ftc1cnnclem  35128  ftc1anclem2  35131  ftc1anclem4  35133  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem8  35137