Theorem sibfima

Description: Any preimage of a singleton by a simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018)

	Ref	Expression
Hypotheses	sitgval.b	|- B = ( Base ` W )
	sitgval.j	|- J = ( TopOpen ` W )
	sitgval.s	|- S = ( sigaGen ` J )
	sitgval.0	|- .0. = ( 0g ` W )
	sitgval.x	|- .x. = ( .s ` W )
	sitgval.h	|- H = ( RRHom ` ( Scalar ` W ) )
	sitgval.1	|- ( ph -> W e. V )
	sitgval.2	|- ( ph -> M e. U. ran measures )
	sibfmbl.1	|- ( ph -> F e. dom ( W sitg M ) )
Assertion	sibfima	|- ( ( ph /\ A e. ( ran F \ { .0. } ) ) -> ( M ` ( `' F " { A } ) ) e. ( 0 [,) +oo ) )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	|- B = ( Base ` W )
2		sitgval.j	|- J = ( TopOpen ` W )
3		sitgval.s	|- S = ( sigaGen ` J )
4		sitgval.0	|- .0. = ( 0g ` W )
5		sitgval.x	|- .x. = ( .s ` W )
6		sitgval.h	|- H = ( RRHom ` ( Scalar ` W ) )
7		sitgval.1	|- ( ph -> W e. V )
8		sitgval.2	|- ( ph -> M e. U. ran measures )
9		sibfmbl.1	|- ( ph -> F e. dom ( W sitg M ) )
10	1 2 3 4 5 6 7 8	issibf	|- ( ph -> ( F e. dom ( W sitg M ) <-> ( F e. ( dom M MblFnM S ) /\ ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) ) )
11	9 10	mpbid	|- ( ph -> ( F e. ( dom M MblFnM S ) /\ ran F e. Fin /\ A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) ) )
12	11	simp3d	|- ( ph -> A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) )
13		sneq	|- ( x = A -> { x } = { A } )
14	13	imaeq2d	|- ( x = A -> ( `' F " { x } ) = ( `' F " { A } ) )
15	14	fveq2d	|- ( x = A -> ( M ` ( `' F " { x } ) ) = ( M ` ( `' F " { A } ) ) )
16	15	eleq1d	|- ( x = A -> ( ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) <-> ( M ` ( `' F " { A } ) ) e. ( 0 [,) +oo ) ) )
17	16	rspcv	|- ( A e. ( ran F \ { .0. } ) -> ( A. x e. ( ran F \ { .0. } ) ( M ` ( `' F " { x } ) ) e. ( 0 [,) +oo ) -> ( M ` ( `' F " { A } ) ) e. ( 0 [,) +oo ) ) )
18	12 17	mpan9	|- ( ( ph /\ A e. ( ran F \ { .0. } ) ) -> ( M ` ( `' F " { A } ) ) e. ( 0 [,) +oo ) )