Theorem iblmbf 25668

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  ⦋csb 3862  ifcif 4488   class class class wbr 5107   ↦ cmpt 5188  dom cdm 5638  ‘cfv 6511  (class class class)co 7387  ℝcr 11067  0cc0 11068  ici 11070   ≤ cle 11209   / cdiv 11835  3c3 12242  ...cfz 13468  ↑cexp 14026  ℜcre 15063  MblFncmbf 25515  ∫₂citg2 25517  𝐿¹cibl 25518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-ss 3931  df-ibl 25523

This theorem is referenced by:  iblcnlem  25690  itgcnlem  25691  itgcnval  25701  itgre  25702  itgim  25703  iblneg  25704  itgneg  25705  iblss  25706  iblss2  25707  itgge0  25712  itgss3  25716  itgless  25718  iblsub  25723  itgadd  25726  itgsub  25727  itgfsum  25728  iblabs  25730  iblmulc2  25732  itgmulc2  25735  itgabs  25736  itgsplit  25737  bddmulibl  25740  itggt0  25745  itgcn  25746  ditgswap  25760  ditgsplitlem  25761  ftc1a  25944  itgsubstlem  25955  iblulm  26316  itgulm  26317  ibladdnc  37671  itgaddnclem1  37672  itgaddnclem2  37673  itgaddnc  37674  iblsubnc  37675  itgsubnc  37676  iblabsnclem  37677  iblabsnc  37678  iblmulc2nc  37679  itgmulc2nclem2  37681  itgmulc2nc  37682  itgabsnc  37683  ftc1cnnclem  37685  ftc1anclem2  37688  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem8  37694