Theorem iblmbf 25748

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052  ⦋csb 3838  ifcif 4467   class class class wbr 5086   ↦ cmpt 5167  dom cdm 5626  ‘cfv 6494  (class class class)co 7362  ℝcr 11032  0cc0 11033  ici 11035   ≤ cle 11175   / cdiv 11802  3c3 12232  ...cfz 13456  ↑cexp 14018  ℜcre 15054  MblFncmbf 25595  ∫₂citg2 25597  𝐿¹cibl 25598

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-ss 3907  df-ibl 25603

This theorem is referenced by:  iblcnlem  25770  itgcnlem  25771  itgcnval  25781  itgre  25782  itgim  25783  iblneg  25784  itgneg  25785  iblss  25786  iblss2  25787  itgge0  25792  itgss3  25796  itgless  25798  iblsub  25803  itgadd  25806  itgsub  25807  itgfsum  25808  iblabs  25810  iblmulc2  25812  itgmulc2  25815  itgabs  25816  itgsplit  25817  bddmulibl  25820  itggt0  25825  itgcn  25826  ditgswap  25840  ditgsplitlem  25841  ftc1a  26018  itgsubstlem  26029  iblulm  26389  itgulm  26390  ibladdnc  38016  itgaddnclem1  38017  itgaddnclem2  38018  itgaddnc  38019  iblsubnc  38020  itgsubnc  38021  iblabsnclem  38022  iblabsnc  38023  iblmulc2nc  38024  itgmulc2nclem2  38026  itgmulc2nc  38027  itgabsnc  38028  ftc1cnnclem  38030  ftc1anclem2  38033  ftc1anclem4  38035  ftc1anclem5  38036  ftc1anclem6  38037  ftc1anclem8  38039