Theorem iblmbf 25937

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142  ∀wral 3078  ⦋csb 3852  ifcif 4486   class class class wbr 5108   ↦ cmpt 5191  dom cdm 5660  ‘cfv 6536  (class class class)co 7412  ℝcr 11105  0cc0 11106  ici 11108   ≤ cle 11250   / cdiv 11877  3c3 12302  ...cfz 13541  ↑cexp 14104  ℜcre 15155  MblFncmbf 25784  ∫₂citg2 25786  𝐿¹cibl 25787

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-ss 3921  df-ibl 25792

This theorem is used by:  iblcnlem  25959  itgcnlem  25960  itgcnval  25970  itgre  25971  itgim  25972  iblneg  25973  itgneg  25974  iblss  25975  iblss2  25976  itgge0  25981  itgss3  25985  itgless  25987  iblsub  25992  itgadd  25995  itgsub  25996  itgfsum  25997  iblabs  25999  iblmulc2  26001  itgmulc2  26004  itgabs  26005  itgsplit  26006  bddmulibl  26009  itggt0  26014  itgcn  26015  ditgswap  26029  ditgsplitlem  26030  ftc1a  26207  itgsubstlem  26218  iblulm  26581  itgulm  26582  ibladdnc  38356  itgaddnclem1  38357  itgaddnclem2  38358  itgaddnc  38359  iblsubnc  38360  itgsubnc  38361  iblabsnclem  38362  iblabsnc  38363  iblmulc2nc  38364  itgmulc2nclem2  38366  itgmulc2nc  38367  itgabsnc  38368  ftc1cnnclem  38370  ftc1anclem2  38373  ftc1anclem4  38375  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anclem8  38379