Theorem iblmbf 24932

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3064  ⦋csb 3832  ifcif 4459   class class class wbr 5074   ↦ cmpt 5157  dom cdm 5589  ‘cfv 6433  (class class class)co 7275  ℝcr 10870  0cc0 10871  ici 10873   ≤ cle 11010   / cdiv 11632  3c3 12029  ...cfz 13239  ↑cexp 13782  ℜcre 14808  MblFncmbf 24778  ∫₂citg2 24780  𝐿¹cibl 24781

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-ibl 24786

This theorem is referenced by:  iblcnlem  24953  itgcnlem  24954  itgcnval  24964  itgre  24965  itgim  24966  iblneg  24967  itgneg  24968  iblss  24969  iblss2  24970  itgge0  24975  itgss3  24979  itgless  24981  iblsub  24986  itgadd  24989  itgsub  24990  itgfsum  24991  iblabs  24993  iblmulc2  24995  itgmulc2  24998  itgabs  24999  itgsplit  25000  bddmulibl  25003  itggt0  25008  itgcn  25009  ditgswap  25023  ditgsplitlem  25024  ftc1a  25201  itgsubstlem  25212  iblulm  25566  itgulm  25567  ibladdnc  35834  itgaddnclem1  35835  itgaddnclem2  35836  itgaddnc  35837  iblsubnc  35838  itgsubnc  35839  iblabsnclem  35840  iblabsnc  35841  iblmulc2nc  35842  itgmulc2nclem2  35844  itgmulc2nc  35845  itgabsnc  35846  ftc1cnnclem  35848  ftc1anclem2  35851  ftc1anclem4  35853  ftc1anclem5  35854  ftc1anclem6  35855  ftc1anclem8  35857