Theorem iblmbf 25738

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ∀wral 3050  ⦋csb 3879  ifcif 4505   class class class wbr 5123   ↦ cmpt 5205  dom cdm 5665  ‘cfv 6541  (class class class)co 7413  ℝcr 11136  0cc0 11137  ici 11139   ≤ cle 11278   / cdiv 11902  3c3 12304  ...cfz 13529  ↑cexp 14084  ℜcre 15118  MblFncmbf 25585  ∫₂citg2 25587  𝐿¹cibl 25588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-ss 3948  df-ibl 25593

This theorem is referenced by:  iblcnlem  25760  itgcnlem  25761  itgcnval  25771  itgre  25772  itgim  25773  iblneg  25774  itgneg  25775  iblss  25776  iblss2  25777  itgge0  25782  itgss3  25786  itgless  25788  iblsub  25793  itgadd  25796  itgsub  25797  itgfsum  25798  iblabs  25800  iblmulc2  25802  itgmulc2  25805  itgabs  25806  itgsplit  25807  bddmulibl  25810  itggt0  25815  itgcn  25816  ditgswap  25830  ditgsplitlem  25831  ftc1a  26014  itgsubstlem  26025  iblulm  26386  itgulm  26387  ibladdnc  37643  itgaddnclem1  37644  itgaddnclem2  37645  itgaddnc  37646  iblsubnc  37647  itgsubnc  37648  iblabsnclem  37649  iblabsnc  37650  iblmulc2nc  37651  itgmulc2nclem2  37653  itgmulc2nc  37654  itgabsnc  37655  ftc1cnnclem  37657  ftc1anclem2  37660  ftc1anclem4  37662  ftc1anclem5  37663  ftc1anclem6  37664  ftc1anclem8  37666