Theorem iblmbf 25285

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062  ⦋csb 3894  ifcif 4529   class class class wbr 5149   ↦ cmpt 5232  dom cdm 5677  ‘cfv 6544  (class class class)co 7409  ℝcr 11109  0cc0 11110  ici 11112   ≤ cle 11249   / cdiv 11871  3c3 12268  ...cfz 13484  ↑cexp 14027  ℜcre 15044  MblFncmbf 25131  ∫₂citg2 25133  𝐿¹cibl 25134

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-ibl 25139

This theorem is referenced by:  iblcnlem  25306  itgcnlem  25307  itgcnval  25317  itgre  25318  itgim  25319  iblneg  25320  itgneg  25321  iblss  25322  iblss2  25323  itgge0  25328  itgss3  25332  itgless  25334  iblsub  25339  itgadd  25342  itgsub  25343  itgfsum  25344  iblabs  25346  iblmulc2  25348  itgmulc2  25351  itgabs  25352  itgsplit  25353  bddmulibl  25356  itggt0  25361  itgcn  25362  ditgswap  25376  ditgsplitlem  25377  ftc1a  25554  itgsubstlem  25565  iblulm  25919  itgulm  25920  ibladdnc  36545  itgaddnclem1  36546  itgaddnclem2  36547  itgaddnc  36548  iblsubnc  36549  itgsubnc  36550  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  itgmulc2nclem2  36555  itgmulc2nc  36556  itgabsnc  36557  ftc1cnnclem  36559  ftc1anclem2  36562  ftc1anclem4  36564  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem8  36568