Theorem iblmbf

Description: An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014)

	Ref	Expression
Assertion	iblmbf	⊢ ( 𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn )

Proof

Step	Hyp	Ref	Expression
1		df-ibl	⊢ 𝐿1 = { 𝑓 ∈ MblFn ∣ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ∈ ℝ }
2	1	ssrab3	⊢ 𝐿1 ⊆ MblFn
3	2	sseli	⊢ ( 𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn )