Theorem iblmbf 25734

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3051  ⦋csb 3837  ifcif 4466   class class class wbr 5085   ↦ cmpt 5166  dom cdm 5631  ‘cfv 6498  (class class class)co 7367  ℝcr 11037  0cc0 11038  ici 11040   ≤ cle 11180   / cdiv 11807  3c3 12237  ...cfz 13461  ↑cexp 14023  ℜcre 15059  MblFncmbf 25581  ∫₂citg2 25583  𝐿¹cibl 25584

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906  df-ibl 25589

This theorem is referenced by:  iblcnlem  25756  itgcnlem  25757  itgcnval  25767  itgre  25768  itgim  25769  iblneg  25770  itgneg  25771  iblss  25772  iblss2  25773  itgge0  25778  itgss3  25782  itgless  25784  iblsub  25789  itgadd  25792  itgsub  25793  itgfsum  25794  iblabs  25796  iblmulc2  25798  itgmulc2  25801  itgabs  25802  itgsplit  25803  bddmulibl  25806  itggt0  25811  itgcn  25812  ditgswap  25826  ditgsplitlem  25827  ftc1a  26004  itgsubstlem  26015  iblulm  26372  itgulm  26373  ibladdnc  37998  itgaddnclem1  37999  itgaddnclem2  38000  itgaddnc  38001  iblsubnc  38002  itgsubnc  38003  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  itgmulc2nclem2  38008  itgmulc2nc  38009  itgabsnc  38010  ftc1cnnclem  38012  ftc1anclem2  38015  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem8  38021