Metamath Proof Explorer

Theorem iblmbf

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

		Ref	Expression
	Assertion	iblmbf	\|- ( F e. L^1 -> F e. MblFn )

Proof

Step	Hyp	Ref	Expression
1		df-ibl	\|- L^1 = { f e. MblFn \| A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR \|-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR }
2	1	ssrab3	\|- L^1 C_ MblFn
3	2	sseli	\|- ( F e. L^1 -> F e. MblFn )

Step

Hyp

Ref

Expression

df-ibl

 |-  L^1 = { f e. MblFn | A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR }

ssrab3

 |-  L^1 C_ MblFn

sseli

 |-  ( F e. L^1 -> F e. MblFn )