Theorem iblmbf 25675

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3045  ⦋csb 3865  ifcif 4491   class class class wbr 5110   ↦ cmpt 5191  dom cdm 5641  ‘cfv 6514  (class class class)co 7390  ℝcr 11074  0cc0 11075  ici 11077   ≤ cle 11216   / cdiv 11842  3c3 12249  ...cfz 13475  ↑cexp 14033  ℜcre 15070  MblFncmbf 25522  ∫₂citg2 25524  𝐿¹cibl 25525

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934  df-ibl 25530

This theorem is referenced by:  iblcnlem  25697  itgcnlem  25698  itgcnval  25708  itgre  25709  itgim  25710  iblneg  25711  itgneg  25712  iblss  25713  iblss2  25714  itgge0  25719  itgss3  25723  itgless  25725  iblsub  25730  itgadd  25733  itgsub  25734  itgfsum  25735  iblabs  25737  iblmulc2  25739  itgmulc2  25742  itgabs  25743  itgsplit  25744  bddmulibl  25747  itggt0  25752  itgcn  25753  ditgswap  25767  ditgsplitlem  25768  ftc1a  25951  itgsubstlem  25962  iblulm  26323  itgulm  26324  ibladdnc  37678  itgaddnclem1  37679  itgaddnclem2  37680  itgaddnc  37681  iblsubnc  37682  itgsubnc  37683  iblabsnclem  37684  iblabsnc  37685  iblmulc2nc  37686  itgmulc2nclem2  37688  itgmulc2nc  37689  itgabsnc  37690  ftc1cnnclem  37692  ftc1anclem2  37695  ftc1anclem4  37697  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem8  37701