Theorem sibfmbl

Description: A simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018)

	Ref	Expression
Hypotheses	sitgval.b	$$⊢B={\mathrm{Base}}_W$$
	sitgval.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
	sitgval.s	$$⊢S=𝛔\left(J\right)$$
	sitgval.0	$$⊢\underset{\dot{}}{0}=0_W$$
	sitgval.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	sitgval.h	$$⊢H=\mathrm{ℝHom}\left(\mathrm{Scalar}\left(W\right)\right)$$
	sitgval.1	$$⊢\phi \to W\in V$$
	sitgval.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
	sibfmbl.1	$$⊢\phi \to F\in {\Im }_M^W$$
Assertion	sibfmbl	$$⊢\phi \to F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)$$

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	$$⊢B={\mathrm{Base}}_W$$
2		sitgval.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
3		sitgval.s	$$⊢S=𝛔\left(J\right)$$
4		sitgval.0	$$⊢\underset{\dot{}}{0}=0_W$$
5		sitgval.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		sitgval.h	$$⊢H=\mathrm{ℝHom}\left(\mathrm{Scalar}\left(W\right)\right)$$
7		sitgval.1	$$⊢\phi \to W\in V$$
8		sitgval.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
9		sibfmbl.1	$$⊢\phi \to F\in {\Im }_M^W$$
10	1 2 3 4 5 6 7 8	issibf	$$⊢\phi \to \left(F\in {\Im }_M^W\leftrightarrow \left(F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)\wedge \mathrm{ran}F\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)\right)$$
11	9 10	mpbid	$$⊢\phi \to \left(F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)\wedge \mathrm{ran}F\in \mathrm{Fin}\wedge \forall x\in \left(\mathrm{ran}F\setminus \left\{\underset{\dot{}}{0}\right\}\right)M\left(F^{-1}\left[\left\{x\right\}\right]\right)\in \left[0,\mathrm{+\infty }\right)\right)$$
12	11	simp1d	$$⊢\phi \to F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)$$