Theorem iblmbf 23340

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896  {crab 2900  ⦋csb 3499  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038  ‘cfv 5804  (class class class)co 6549  ℝcr 9814  0cc0 9815  ici 9817   ≤ cle 9954   / cdiv 10563  3c3 10948  ...cfz 12197  ↑cexp 12722  ℜcre 13685  MblFncmbf 23189  ∫₂citg2 23191  𝐿¹cibl 23192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-ss 3554  df-ibl 23197

This theorem is referenced by:  iblcnlem  23361  itgcnlem  23362  itgcnval  23372  itgre  23373  itgim  23374  iblneg  23375  itgneg  23376  iblss  23377  iblss2  23378  itgge0  23383  itgss3  23387  itgless  23389  iblsub  23394  itgadd  23397  itgsub  23398  itgfsum  23399  iblabs  23401  iblmulc2  23403  itgmulc2  23406  itgabs  23407  itgsplit  23408  bddmulibl  23411  itggt0  23414  itgcn  23415  ditgswap  23429  ditgsplitlem  23430  ftc1a  23604  itgsubstlem  23615  iblulm  23965  itgulm  23966  ibladdnc  32637  itgaddnclem1  32638  itgaddnclem2  32639  itgaddnc  32640  iblsubnc  32641  itgsubnc  32642  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  itgmulc2nclem2  32647  itgmulc2nc  32648  itgabsnc  32649  ftc1cnnclem  32653  ftc1anclem2  32656  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem8  32662