Theorem iblmbf 24943

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2110  ∀wral 3066  ⦋csb 3837  ifcif 4465   class class class wbr 5079   ↦ cmpt 5162  dom cdm 5590  ‘cfv 6432  (class class class)co 7272  ℝcr 10881  0cc0 10882  ici 10884   ≤ cle 11021   / cdiv 11643  3c3 12040  ...cfz 13250  ↑cexp 13793  ℜcre 14819  MblFncmbf 24789  ∫₂citg2 24791  𝐿¹cibl 24792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-in 3899  df-ss 3909  df-ibl 24797

This theorem is referenced by:  iblcnlem  24964  itgcnlem  24965  itgcnval  24975  itgre  24976  itgim  24977  iblneg  24978  itgneg  24979  iblss  24980  iblss2  24981  itgge0  24986  itgss3  24990  itgless  24992  iblsub  24997  itgadd  25000  itgsub  25001  itgfsum  25002  iblabs  25004  iblmulc2  25006  itgmulc2  25009  itgabs  25010  itgsplit  25011  bddmulibl  25014  itggt0  25019  itgcn  25020  ditgswap  25034  ditgsplitlem  25035  ftc1a  25212  itgsubstlem  25223  iblulm  25577  itgulm  25578  ibladdnc  35843  itgaddnclem1  35844  itgaddnclem2  35845  itgaddnc  35846  iblsubnc  35847  itgsubnc  35848  iblabsnclem  35849  iblabsnc  35850  iblmulc2nc  35851  itgmulc2nclem2  35853  itgmulc2nc  35854  itgabsnc  35855  ftc1cnnclem  35857  ftc1anclem2  35860  ftc1anclem4  35862  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem8  35866