Theorem iblmbf 26049

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3076  ⦋csb 3846  ifcif 4481   class class class wbr 5102   ↦ cmpt 5185  dom cdm 5647  ‘cfv 6527  (class class class)co 7408  ℝcr 11170  0cc0 11171  ici 11173   ≤ cle 11315   / cdiv 11942  3c3 12367  ...cfz 13608  ↑cexp 14172  ℜcre 15231  MblFncmbf 25896  ∫₂citg2 25898  𝐿¹cibl 25899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3915  df-ibl 25904

This theorem is used by:  iblcnlem  26070  itgcnlem  26071  itgcnval  26081  itgre  26082  itgim  26083  iblneg  26084  itgneg  26085  iblss  26086  iblss2  26087  itgge0  26092  itgss3  26096  itgless  26098  iblsub  26103  itgadd  26106  itgsub  26107  itgfsum  26108  iblabs  26110  iblmulc2  26112  itgmulc2  26115  itgabs  26116  itgsplit  26117  bddmulibl  26120  itggt0  26125  itgcn  26126  ditgswap  26140  ditgsplitlem  26141  ftc1a  26318  itgsubstlem  26329  iblulm  26697  itgulm  26698  ibladdnc  38515  itgaddnclem1  38516  itgaddnclem2  38517  itgaddnc  38518  iblsubnc  38519  itgsubnc  38520  iblabsnclem  38521  iblabsnc  38522  iblmulc2nc  38523  itgmulc2nclem2  38525  itgmulc2nc  38526  itgabsnc  38527  ftc1cnnclem  38529  ftc1anclem2  38532  ftc1anclem4  38534  ftc1anclem5  38535  ftc1anclem6  38536  ftc1anclem8  38538