Theorem iblmbf 25720

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3051  ⦋csb 3874  ifcif 4500   class class class wbr 5119   ↦ cmpt 5201  dom cdm 5654  ‘cfv 6531  (class class class)co 7405  ℝcr 11128  0cc0 11129  ici 11131   ≤ cle 11270   / cdiv 11894  3c3 12296  ...cfz 13524  ↑cexp 14079  ℜcre 15116  MblFncmbf 25567  ∫₂citg2 25569  𝐿¹cibl 25570

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-ss 3943  df-ibl 25575

This theorem is referenced by:  iblcnlem  25742  itgcnlem  25743  itgcnval  25753  itgre  25754  itgim  25755  iblneg  25756  itgneg  25757  iblss  25758  iblss2  25759  itgge0  25764  itgss3  25768  itgless  25770  iblsub  25775  itgadd  25778  itgsub  25779  itgfsum  25780  iblabs  25782  iblmulc2  25784  itgmulc2  25787  itgabs  25788  itgsplit  25789  bddmulibl  25792  itggt0  25797  itgcn  25798  ditgswap  25812  ditgsplitlem  25813  ftc1a  25996  itgsubstlem  26007  iblulm  26368  itgulm  26369  ibladdnc  37701  itgaddnclem1  37702  itgaddnclem2  37703  itgaddnc  37704  iblsubnc  37705  itgsubnc  37706  iblabsnclem  37707  iblabsnc  37708  iblmulc2nc  37709  itgmulc2nclem2  37711  itgmulc2nc  37712  itgabsnc  37713  ftc1cnnclem  37715  ftc1anclem2  37718  ftc1anclem4  37720  ftc1anclem5  37721  ftc1anclem6  37722  ftc1anclem8  37724