Theorem iblmbf 25722

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3049  ⦋csb 3847  ifcif 4477   class class class wbr 5096   ↦ cmpt 5177  dom cdm 5622  ‘cfv 6490  (class class class)co 7356  ℝcr 11023  0cc0 11024  ici 11026   ≤ cle 11165   / cdiv 11792  3c3 12199  ...cfz 13421  ↑cexp 13982  ℜcre 15018  MblFncmbf 25569  ∫₂citg2 25571  𝐿¹cibl 25572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-ss 3916  df-ibl 25577

This theorem is referenced by:  iblcnlem  25744  itgcnlem  25745  itgcnval  25755  itgre  25756  itgim  25757  iblneg  25758  itgneg  25759  iblss  25760  iblss2  25761  itgge0  25766  itgss3  25770  itgless  25772  iblsub  25777  itgadd  25780  itgsub  25781  itgfsum  25782  iblabs  25784  iblmulc2  25786  itgmulc2  25789  itgabs  25790  itgsplit  25791  bddmulibl  25794  itggt0  25799  itgcn  25800  ditgswap  25814  ditgsplitlem  25815  ftc1a  25998  itgsubstlem  26009  iblulm  26370  itgulm  26371  ibladdnc  37817  itgaddnclem1  37818  itgaddnclem2  37819  itgaddnc  37820  iblsubnc  37821  itgsubnc  37822  iblabsnclem  37823  iblabsnc  37824  iblmulc2nc  37825  itgmulc2nclem2  37827  itgmulc2nc  37828  itgabsnc  37829  ftc1cnnclem  37831  ftc1anclem2  37834  ftc1anclem4  37836  ftc1anclem5  37837  ftc1anclem6  37838  ftc1anclem8  37840