Theorem iblmbf 25756

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  ∀wral 3055  ⦋csb 3833  ifcif 4457   class class class wbr 5075   ↦ cmpt 5156  dom cdm 5621  ‘cfv 6489  (class class class)co 7360  ℝcr 11032  0cc0 11033  ici 11035   ≤ cle 11175   / cdiv 11802  3c3 12232  ...cfz 13456  ↑cexp 14018  ℜcre 15054  MblFncmbf 25603  ∫₂citg2 25605  𝐿¹cibl 25606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-ss 3902  df-ibl 25611

This theorem is referenced by:  iblcnlem  25778  itgcnlem  25779  itgcnval  25789  itgre  25790  itgim  25791  iblneg  25792  itgneg  25793  iblss  25794  iblss2  25795  itgge0  25800  itgss3  25804  itgless  25806  iblsub  25811  itgadd  25814  itgsub  25815  itgfsum  25816  iblabs  25818  iblmulc2  25820  itgmulc2  25823  itgabs  25824  itgsplit  25825  bddmulibl  25828  itggt0  25833  itgcn  25834  ditgswap  25848  ditgsplitlem  25849  ftc1a  26026  itgsubstlem  26037  iblulm  26394  itgulm  26395  ibladdnc  38059  itgaddnclem1  38060  itgaddnclem2  38061  itgaddnc  38062  iblsubnc  38063  itgsubnc  38064  iblabsnclem  38065  iblabsnc  38066  iblmulc2nc  38067  itgmulc2nclem2  38069  itgmulc2nc  38070  itgabsnc  38071  ftc1cnnclem  38073  ftc1anclem2  38076  ftc1anclem4  38078  ftc1anclem5  38079  ftc1anclem6  38080  ftc1anclem8  38082