Theorem iblmbf 25509

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 25363	. . 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 7411  ℝcr 11111  0cc0 11112  ici 11114   ≤ cle 11253   / cdiv 11875  3c3 12272  ...cfz 13488  ↑cexp 14031  ℜcre 15048  MblFncmbf 25355  ∫₂citg2 25357  𝐿¹cibl 25358

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 25363

This theorem is referenced by:  iblcnlem  25530  itgcnlem  25531  itgcnval  25541  itgre  25542  itgim  25543  iblneg  25544  itgneg  25545  iblss  25546  iblss2  25547  itgge0  25552  itgss3  25556  itgless  25558  iblsub  25563  itgadd  25566  itgsub  25567  itgfsum  25568  iblabs  25570  iblmulc2  25572  itgmulc2  25575  itgabs  25576  itgsplit  25577  bddmulibl  25580  itggt0  25585  itgcn  25586  ditgswap  25600  ditgsplitlem  25601  ftc1a  25778  itgsubstlem  25789  iblulm  26143  itgulm  26144  ibladdnc  36848  itgaddnclem1  36849  itgaddnclem2  36850  itgaddnc  36851  iblsubnc  36852  itgsubnc  36853  iblabsnclem  36854  iblabsnc  36855  iblmulc2nc  36856  itgmulc2nclem2  36858  itgmulc2nc  36859  itgabsnc  36860  ftc1cnnclem  36862  ftc1anclem2  36865  ftc1anclem4  36867  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem8  36871