Theorem iblmbf 25284

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3061  ⦋csb 3893  ifcif 4528   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676  ‘cfv 6543  (class class class)co 7408  ℝcr 11108  0cc0 11109  ici 11111   ≤ cle 11248   / cdiv 11870  3c3 12267  ...cfz 13483  ↑cexp 14026  ℜcre 15043  MblFncmbf 25130  ∫₂citg2 25132  𝐿¹cibl 25133

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965  df-ibl 25138

This theorem is referenced by:  iblcnlem  25305  itgcnlem  25306  itgcnval  25316  itgre  25317  itgim  25318  iblneg  25319  itgneg  25320  iblss  25321  iblss2  25322  itgge0  25327  itgss3  25331  itgless  25333  iblsub  25338  itgadd  25341  itgsub  25342  itgfsum  25343  iblabs  25345  iblmulc2  25347  itgmulc2  25350  itgabs  25351  itgsplit  25352  bddmulibl  25355  itggt0  25360  itgcn  25361  ditgswap  25375  ditgsplitlem  25376  ftc1a  25553  itgsubstlem  25564  iblulm  25918  itgulm  25919  ibladdnc  36540  itgaddnclem1  36541  itgaddnclem2  36542  itgaddnc  36543  iblsubnc  36544  itgsubnc  36545  iblabsnclem  36546  iblabsnc  36547  iblmulc2nc  36548  itgmulc2nclem2  36550  itgmulc2nc  36551  itgabsnc  36552  ftc1cnnclem  36554  ftc1anclem2  36557  ftc1anclem4  36559  ftc1anclem5  36560  ftc1anclem6  36561  ftc1anclem8  36563