Theorem iblmbf 26088

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∀wral 3076  ⦋csb 3846  ifcif 4481   class class class wbr 5102   ↦ cmpt 5185  dom cdm 5650  ‘cfv 6538  (class class class)co 7420  ℝcr 11199  0cc0 11200  ici 11202   ≤ cle 11344   / cdiv 11973  3c3 12398  ...cfz 13639  ↑cexp 14204  ℜcre 15264  MblFncmbf 25935  ∫₂citg2 25937  𝐿¹cibl 25938

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896  df-ibl 25943

This theorem is used by:  iblcnlem  26109  itgcnlem  26110  itgcnval  26120  itgre  26121  itgim  26122  iblneg  26123  itgneg  26124  iblss  26125  iblss2  26126  itgge0  26131  itgss3  26135  itgless  26137  iblsub  26142  itgadd  26145  itgsub  26146  itgfsum  26147  iblabs  26149  iblmulc2  26151  itgmulc2  26154  itgabs  26155  itgsplit  26156  bddmulibl  26159  itggt0  26164  itgcn  26165  ditgswap  26179  ditgsplitlem  26180  ftc1a  26357  itgsubstlem  26368  iblulm  26734  itgulm  26735  ibladdnc  38596  itgaddnclem1  38597  itgaddnclem2  38598  itgaddnc  38599  iblsubnc  38600  itgsubnc  38601  iblabsnclem  38602  iblabsnc  38603  iblmulc2nc  38604  itgmulc2nclem2  38606  itgmulc2nc  38607  itgabsnc  38608  ftc1cnnclem  38610  ftc1anclem2  38613  ftc1anclem4  38615  ftc1anclem5  38616  ftc1anclem6  38617  ftc1anclem8  38619