Theorem iblmbf 25728

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052  ⦋csb 3850  ifcif 4480   class class class wbr 5099   ↦ cmpt 5180  dom cdm 5625  ‘cfv 6493  (class class class)co 7360  ℝcr 11029  0cc0 11030  ici 11032   ≤ cle 11171   / cdiv 11798  3c3 12205  ...cfz 13427  ↑cexp 13988  ℜcre 15024  MblFncmbf 25575  ∫₂citg2 25577  𝐿¹cibl 25578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-ss 3919  df-ibl 25583

This theorem is referenced by:  iblcnlem  25750  itgcnlem  25751  itgcnval  25761  itgre  25762  itgim  25763  iblneg  25764  itgneg  25765  iblss  25766  iblss2  25767  itgge0  25772  itgss3  25776  itgless  25778  iblsub  25783  itgadd  25786  itgsub  25787  itgfsum  25788  iblabs  25790  iblmulc2  25792  itgmulc2  25795  itgabs  25796  itgsplit  25797  bddmulibl  25800  itggt0  25805  itgcn  25806  ditgswap  25820  ditgsplitlem  25821  ftc1a  26004  itgsubstlem  26015  iblulm  26376  itgulm  26377  ibladdnc  37880  itgaddnclem1  37881  itgaddnclem2  37882  itgaddnc  37883  iblsubnc  37884  itgsubnc  37885  iblabsnclem  37886  iblabsnc  37887  iblmulc2nc  37888  itgmulc2nclem2  37890  itgmulc2nc  37891  itgabsnc  37892  ftc1cnnclem  37894  ftc1anclem2  37897  ftc1anclem4  37899  ftc1anclem5  37900  ftc1anclem6  37901  ftc1anclem8  37903