Theorem iblmbf 23534

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990  ∀wral 2912  {crab 2916  ⦋csb 3533  ifcif 4086   class class class wbr 4653   ↦ cmpt 4729  dom cdm 5114  ‘cfv 5888  (class class class)co 6650  ℝcr 9935  0cc0 9936  ici 9938   ≤ cle 10075   / cdiv 10684  3c3 11071  ...cfz 12326  ↑cexp 12860  ℜcre 13837  MblFncmbf 23383  ∫₂citg2 23385  𝐿¹cibl 23386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-in 3581  df-ss 3588  df-ibl 23391

This theorem is referenced by:  iblcnlem  23555  itgcnlem  23556  itgcnval  23566  itgre  23567  itgim  23568  iblneg  23569  itgneg  23570  iblss  23571  iblss2  23572  itgge0  23577  itgss3  23581  itgless  23583  iblsub  23588  itgadd  23591  itgsub  23592  itgfsum  23593  iblabs  23595  iblmulc2  23597  itgmulc2  23600  itgabs  23601  itgsplit  23602  bddmulibl  23605  itggt0  23608  itgcn  23609  ditgswap  23623  ditgsplitlem  23624  ftc1a  23800  itgsubstlem  23811  iblulm  24161  itgulm  24162  ibladdnc  33467  itgaddnclem1  33468  itgaddnclem2  33469  itgaddnc  33470  iblsubnc  33471  itgsubnc  33472  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  itgmulc2nclem2  33477  itgmulc2nc  33478  itgabsnc  33479  ftc1cnnclem  33483  ftc1anclem2  33486  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem8  33492