Theorem iblmbf 26115

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∀wral 3080  ⦋csb 3851  ifcif 4485   class class class wbr 5106   ↦ cmpt 5189  dom cdm 5655  ‘cfv 6555  (class class class)co 7440  ℝcr 11223  0cc0 11224  ici 11226   ≤ cle 11368   / cdiv 11997  3c3 12422  ...cfz 13663  ↑cexp 14228  ℜcre 15290  MblFncmbf 25962  ∫₂citg2 25964  𝐿¹cibl 25965

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-ibl 25970

This theorem is used by:  iblcnlem  26136  itgcnlem  26137  itgcnval  26147  itgre  26148  itgim  26149  iblneg  26150  itgneg  26151  iblss  26152  iblss2  26153  itgge0  26158  itgss3  26162  itgless  26164  iblsub  26169  itgadd  26172  itgsub  26173  itgfsum  26174  iblabs  26176  iblmulc2  26178  itgmulc2  26181  itgabs  26182  itgsplit  26183  bddmulibl  26186  itggt0  26191  itgcn  26192  ditgswap  26206  ditgsplitlem  26207  ftc1a  26384  itgsubstlem  26395  iblulm  26761  itgulm  26762  ibladdnc  38786  itgaddnclem1  38787  itgaddnclem2  38788  itgaddnc  38789  iblsubnc  38790  itgsubnc  38791  iblabsnclem  38792  iblabsnc  38793  iblmulc2nc  38794  itgmulc2nclem2  38796  itgmulc2nc  38797  itgabsnc  38798  ftc1cnnclem  38800  ftc1anclem2  38803  ftc1anclem4  38805  ftc1anclem5  38806  ftc1anclem6  38807  ftc1anclem8  38809