Theorem iblmbf 23824

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 2155  ∀wral 3054  {crab 3058  ⦋csb 3690  ifcif 4242   class class class wbr 4808   ↦ cmpt 4887  dom cdm 5276  ‘cfv 6067  (class class class)co 6841  ℝcr 10187  0cc0 10188  ici 10190   ≤ cle 10328   / cdiv 10937  3c3 11327  ...cfz 12532  ↑cexp 13066  ℜcre 14123  MblFncmbf 23671  ∫₂citg2 23673  𝐿¹cibl 23674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-rab 3063  df-in 3738  df-ss 3745  df-ibl 23679

This theorem is referenced by:  iblcnlem  23845  itgcnlem  23846  itgcnval  23856  itgre  23857  itgim  23858  iblneg  23859  itgneg  23860  iblss  23861  iblss2  23862  itgge0  23867  itgss3  23871  itgless  23873  iblsub  23878  itgadd  23881  itgsub  23882  itgfsum  23883  iblabs  23885  iblmulc2  23887  itgmulc2  23890  itgabs  23891  itgsplit  23892  bddmulibl  23895  itggt0  23898  itgcn  23899  ditgswap  23913  ditgsplitlem  23914  ftc1a  24090  itgsubstlem  24101  iblulm  24451  itgulm  24452  ibladdnc  33822  itgaddnclem1  33823  itgaddnclem2  33824  itgaddnc  33825  iblsubnc  33826  itgsubnc  33827  iblabsnclem  33828  iblabsnc  33829  iblmulc2nc  33830  itgmulc2nclem2  33832  itgmulc2nc  33833  itgabsnc  33834  ftc1cnnclem  33838  ftc1anclem2  33841  ftc1anclem4  33843  ftc1anclem5  33844  ftc1anclem6  33845  ftc1anclem8  33847