Theorem iblmbf 25822

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3067  ⦋csb 3921  ifcif 4548   class class class wbr 5166   ↦ cmpt 5249  dom cdm 5700  ‘cfv 6573  (class class class)co 7448  ℝcr 11183  0cc0 11184  ici 11186   ≤ cle 11325   / cdiv 11947  3c3 12349  ...cfz 13567  ↑cexp 14112  ℜcre 15146  MblFncmbf 25668  ∫₂citg2 25670  𝐿¹cibl 25671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-ss 3993  df-ibl 25676

This theorem is referenced by:  iblcnlem  25844  itgcnlem  25845  itgcnval  25855  itgre  25856  itgim  25857  iblneg  25858  itgneg  25859  iblss  25860  iblss2  25861  itgge0  25866  itgss3  25870  itgless  25872  iblsub  25877  itgadd  25880  itgsub  25881  itgfsum  25882  iblabs  25884  iblmulc2  25886  itgmulc2  25889  itgabs  25890  itgsplit  25891  bddmulibl  25894  itggt0  25899  itgcn  25900  ditgswap  25914  ditgsplitlem  25915  ftc1a  26098  itgsubstlem  26109  iblulm  26468  itgulm  26469  ibladdnc  37637  itgaddnclem1  37638  itgaddnclem2  37639  itgaddnc  37640  iblsubnc  37641  itgsubnc  37642  iblabsnclem  37643  iblabsnc  37644  iblmulc2nc  37645  itgmulc2nclem2  37647  itgmulc2nc  37648  itgabsnc  37649  ftc1cnnclem  37651  ftc1anclem2  37654  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem8  37660