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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  ∀wral 3050  ⦋csb 3889  ifcif 4530   class class class wbr 5149   ↦ cmpt 5232  dom cdm 5678  ‘cfv 6549  (class class class)co 7419  ℝcr 11139  0cc0 11140  ici 11142   ≤ cle 11281   / cdiv 11903  3c3 12301  ...cfz 13519  ↑cexp 14062  ℜcre 15080  MblFncmbf 25587  ∫₂citg2 25589  𝐿¹cibl 25590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-ss 3961  df-ibl 25595

This theorem is referenced by:  iblcnlem  25762  itgcnlem  25763  itgcnval  25773  itgre  25774  itgim  25775  iblneg  25776  itgneg  25777  iblss  25778  iblss2  25779  itgge0  25784  itgss3  25788  itgless  25790  iblsub  25795  itgadd  25798  itgsub  25799  itgfsum  25800  iblabs  25802  iblmulc2  25804  itgmulc2  25807  itgabs  25808  itgsplit  25809  bddmulibl  25812  itggt0  25817  itgcn  25818  ditgswap  25832  ditgsplitlem  25833  ftc1a  26016  itgsubstlem  26027  iblulm  26388  itgulm  26389  ibladdnc  37281  itgaddnclem1  37282  itgaddnclem2  37283  itgaddnc  37284  iblsubnc  37285  itgsubnc  37286  iblabsnclem  37287  iblabsnc  37288  iblmulc2nc  37289  itgmulc2nclem2  37291  itgmulc2nc  37292  itgabsnc  37293  ftc1cnnclem  37295  ftc1anclem2  37298  ftc1anclem4  37300  ftc1anclem5  37301  ftc1anclem6  37302  ftc1anclem8  37304