Theorem iblmbf 24837

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3063  ⦋csb 3828  ifcif 4456   class class class wbr 5070   ↦ cmpt 5153  dom cdm 5580  ‘cfv 6418  (class class class)co 7255  ℝcr 10801  0cc0 10802  ici 10804   ≤ cle 10941   / cdiv 11562  3c3 11959  ...cfz 13168  ↑cexp 13710  ℜcre 14736  MblFncmbf 24683  ∫₂citg2 24685  𝐿¹cibl 24686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-ibl 24691

This theorem is referenced by:  iblcnlem  24858  itgcnlem  24859  itgcnval  24869  itgre  24870  itgim  24871  iblneg  24872  itgneg  24873  iblss  24874  iblss2  24875  itgge0  24880  itgss3  24884  itgless  24886  iblsub  24891  itgadd  24894  itgsub  24895  itgfsum  24896  iblabs  24898  iblmulc2  24900  itgmulc2  24903  itgabs  24904  itgsplit  24905  bddmulibl  24908  itggt0  24913  itgcn  24914  ditgswap  24928  ditgsplitlem  24929  ftc1a  25106  itgsubstlem  25117  iblulm  25471  itgulm  25472  ibladdnc  35761  itgaddnclem1  35762  itgaddnclem2  35763  itgaddnc  35764  iblsubnc  35765  itgsubnc  35766  iblabsnclem  35767  iblabsnc  35768  iblmulc2nc  35769  itgmulc2nclem2  35771  itgmulc2nc  35772  itgabsnc  35773  ftc1cnnclem  35775  ftc1anclem2  35778  ftc1anclem4  35780  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem8  35784