Theorem mbfima

Description: Definitional property of a measurable function: the preimage of an open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

	Ref	Expression
Assertion	mbfima	|- ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( B (,) C ) ) e. dom vol )

Proof

Step	Hyp	Ref	Expression
1		ismbf	|- ( F : A --> RR -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
2	1	biimpac	|- ( ( F e. MblFn /\ F : A --> RR ) -> A. x e. ran (,) ( `' F " x ) e. dom vol )
3		ioof	|- (,) : ( RR* X. RR* ) --> ~P RR
4		ffn	|- ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
5	3 4	ax-mp	|- (,) Fn ( RR* X. RR* )
6		fnovrn	|- ( ( (,) Fn ( RR* X. RR* ) /\ B e. RR* /\ C e. RR* ) -> ( B (,) C ) e. ran (,) )
7	5 6	mp3an1	|- ( ( B e. RR* /\ C e. RR* ) -> ( B (,) C ) e. ran (,) )
8		imaeq2	|- ( x = ( B (,) C ) -> ( `' F " x ) = ( `' F " ( B (,) C ) ) )
9	8	eleq1d	|- ( x = ( B (,) C ) -> ( ( `' F " x ) e. dom vol <-> ( `' F " ( B (,) C ) ) e. dom vol ) )
10	9	rspccva	|- ( ( A. x e. ran (,) ( `' F " x ) e. dom vol /\ ( B (,) C ) e. ran (,) ) -> ( `' F " ( B (,) C ) ) e. dom vol )
11	2 7 10	syl2an	|- ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR* /\ C e. RR* ) ) -> ( `' F " ( B (,) C ) ) e. dom vol )
12		ndmioo	|- ( -. ( B e. RR* /\ C e. RR* ) -> ( B (,) C ) = (/) )
13	12	imaeq2d	|- ( -. ( B e. RR* /\ C e. RR* ) -> ( `' F " ( B (,) C ) ) = ( `' F " (/) ) )
14		ima0	|- ( `' F " (/) ) = (/)
15	13 14	eqtrdi	|- ( -. ( B e. RR* /\ C e. RR* ) -> ( `' F " ( B (,) C ) ) = (/) )
16		0mbl	|- (/) e. dom vol
17	15 16	eqeltrdi	|- ( -. ( B e. RR* /\ C e. RR* ) -> ( `' F " ( B (,) C ) ) e. dom vol )
18	17	adantl	|- ( ( ( F e. MblFn /\ F : A --> RR ) /\ -. ( B e. RR* /\ C e. RR* ) ) -> ( `' F " ( B (,) C ) ) e. dom vol )
19	11 18	pm2.61dan	|- ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( B (,) C ) ) e. dom vol )