Theorem iblmbf 25741

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052  ⦋csb 3851  ifcif 4481   class class class wbr 5100   ↦ cmpt 5181  dom cdm 5634  ‘cfv 6502  (class class class)co 7370  ℝcr 11039  0cc0 11040  ici 11042   ≤ cle 11181   / cdiv 11808  3c3 12215  ...cfz 13437  ↑cexp 13998  ℜcre 15034  MblFncmbf 25588  ∫₂citg2 25590  𝐿¹cibl 25591

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920  df-ibl 25596

This theorem is referenced by:  iblcnlem  25763  itgcnlem  25764  itgcnval  25774  itgre  25775  itgim  25776  iblneg  25777  itgneg  25778  iblss  25779  iblss2  25780  itgge0  25785  itgss3  25789  itgless  25791  iblsub  25796  itgadd  25799  itgsub  25800  itgfsum  25801  iblabs  25803  iblmulc2  25805  itgmulc2  25808  itgabs  25809  itgsplit  25810  bddmulibl  25813  itggt0  25818  itgcn  25819  ditgswap  25833  ditgsplitlem  25834  ftc1a  26017  itgsubstlem  26028  iblulm  26389  itgulm  26390  ibladdnc  37957  itgaddnclem1  37958  itgaddnclem2  37959  itgaddnc  37960  iblsubnc  37961  itgsubnc  37962  iblabsnclem  37963  iblabsnc  37964  iblmulc2nc  37965  itgmulc2nclem2  37967  itgmulc2nc  37968  itgabsnc  37969  ftc1cnnclem  37971  ftc1anclem2  37974  ftc1anclem4  37976  ftc1anclem5  37977  ftc1anclem6  37978  ftc1anclem8  37980