Theorem iblmbf 25802

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3061  ⦋csb 3899  ifcif 4525   class class class wbr 5143   ↦ cmpt 5225  dom cdm 5685  ‘cfv 6561  (class class class)co 7431  ℝcr 11154  0cc0 11155  ici 11157   ≤ cle 11296   / cdiv 11920  3c3 12322  ...cfz 13547  ↑cexp 14102  ℜcre 15136  MblFncmbf 25649  ∫₂citg2 25651  𝐿¹cibl 25652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-ss 3968  df-ibl 25657

This theorem is referenced by:  iblcnlem  25824  itgcnlem  25825  itgcnval  25835  itgre  25836  itgim  25837  iblneg  25838  itgneg  25839  iblss  25840  iblss2  25841  itgge0  25846  itgss3  25850  itgless  25852  iblsub  25857  itgadd  25860  itgsub  25861  itgfsum  25862  iblabs  25864  iblmulc2  25866  itgmulc2  25869  itgabs  25870  itgsplit  25871  bddmulibl  25874  itggt0  25879  itgcn  25880  ditgswap  25894  ditgsplitlem  25895  ftc1a  26078  itgsubstlem  26089  iblulm  26450  itgulm  26451  ibladdnc  37684  itgaddnclem1  37685  itgaddnclem2  37686  itgaddnc  37687  iblsubnc  37688  itgsubnc  37689  iblabsnclem  37690  iblabsnc  37691  iblmulc2nc  37692  itgmulc2nclem2  37694  itgmulc2nc  37695  itgabsnc  37696  ftc1cnnclem  37698  ftc1anclem2  37701  ftc1anclem4  37703  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem8  37707