Theorem iblmbf 25701

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  ⦋csb 3859  ifcif 4484   class class class wbr 5102   ↦ cmpt 5183  dom cdm 5631  ‘cfv 6499  (class class class)co 7369  ℝcr 11043  0cc0 11044  ici 11046   ≤ cle 11185   / cdiv 11811  3c3 12218  ...cfz 13444  ↑cexp 14002  ℜcre 15039  MblFncmbf 25548  ∫₂citg2 25550  𝐿¹cibl 25551

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-ss 3928  df-ibl 25556

This theorem is referenced by:  iblcnlem  25723  itgcnlem  25724  itgcnval  25734  itgre  25735  itgim  25736  iblneg  25737  itgneg  25738  iblss  25739  iblss2  25740  itgge0  25745  itgss3  25749  itgless  25751  iblsub  25756  itgadd  25759  itgsub  25760  itgfsum  25761  iblabs  25763  iblmulc2  25765  itgmulc2  25768  itgabs  25769  itgsplit  25770  bddmulibl  25773  itggt0  25778  itgcn  25779  ditgswap  25793  ditgsplitlem  25794  ftc1a  25977  itgsubstlem  25988  iblulm  26349  itgulm  26350  ibladdnc  37664  itgaddnclem1  37665  itgaddnclem2  37666  itgaddnc  37667  iblsubnc  37668  itgsubnc  37669  iblabsnclem  37670  iblabsnc  37671  iblmulc2nc  37672  itgmulc2nclem2  37674  itgmulc2nc  37675  itgabsnc  37676  ftc1cnnclem  37678  ftc1anclem2  37681  ftc1anclem4  37683  ftc1anclem5  37684  ftc1anclem6  37685  ftc1anclem8  37687