Theorem iblmbf 25996

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3078  ⦋csb 3850  ifcif 4485   class class class wbr 5107   ↦ cmpt 5190  dom cdm 5659  ‘cfv 6537  (class class class)co 7416  ℝcr 11126  0cc0 11127  ici 11129   ≤ cle 11271   / cdiv 11898  3c3 12323  ...cfz 13563  ↑cexp 14127  ℜcre 15186  MblFncmbf 25843  ∫₂citg2 25845  𝐿¹cibl 25846

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3919  df-ibl 25851

This theorem is used by:  iblcnlem  26018  itgcnlem  26019  itgcnval  26029  itgre  26030  itgim  26031  iblneg  26032  itgneg  26033  iblss  26034  iblss2  26035  itgge0  26040  itgss3  26044  itgless  26046  iblsub  26051  itgadd  26054  itgsub  26055  itgfsum  26056  iblabs  26058  iblmulc2  26060  itgmulc2  26063  itgabs  26064  itgsplit  26065  bddmulibl  26068  itggt0  26073  itgcn  26074  ditgswap  26088  ditgsplitlem  26089  ftc1a  26266  itgsubstlem  26277  iblulm  26640  itgulm  26641  ibladdnc  38413  itgaddnclem1  38414  itgaddnclem2  38415  itgaddnc  38416  iblsubnc  38417  itgsubnc  38418  iblabsnclem  38419  iblabsnc  38420  iblmulc2nc  38421  itgmulc2nclem2  38423  itgmulc2nc  38424  itgabsnc  38425  ftc1cnnclem  38427  ftc1anclem2  38430  ftc1anclem4  38432  ftc1anclem5  38433  ftc1anclem6  38434  ftc1anclem8  38436