Theorem mbfmcnvima

Description: The preimage by a measurable function is a measurable set. (Contributed by Thierry Arnoux, 23-Jan-2017)

	Ref	Expression
Hypotheses	mbfmf.1	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
	mbfmf.2	$$⊢\phi \to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
	mbfmf.3	$$⊢\phi \to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$
	mbfmcnvima.4	$$⊢\phi \to A\in T$$
Assertion	mbfmcnvima	$$⊢\phi \to F^{-1}\left[A\right]\in S$$

Proof

Step	Hyp	Ref	Expression
1		mbfmf.1	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
2		mbfmf.2	$$⊢\phi \to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
3		mbfmf.3	$$⊢\phi \to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$
4		mbfmcnvima.4	$$⊢\phi \to A\in T$$
5		imaeq2	$$⊢x=A\to F^{-1}\left[x\right]=F^{-1}\left[A\right]$$
6	5	eleq1d	$$⊢x=A\to \left(F^{-1}\left[x\right]\in S\leftrightarrow F^{-1}\left[A\right]\in S\right)$$
7	1 2	ismbfm	$$⊢\phi \to \left(F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)\leftrightarrow \left(F\in \left({\bigcup T}^{\bigcup S}\right)\wedge \forall x\in T{F}^{-1}\left[x\right]\in S\right)\right)$$
8	3 7	mpbid	$$⊢\phi \to \left(F\in \left({\bigcup T}^{\bigcup S}\right)\wedge \forall x\in T{F}^{-1}\left[x\right]\in S\right)$$
9	8	simprd	$$⊢\phi \to \forall x\in T{F}^{-1}\left[x\right]\in S$$
10	6 9 4	rspcdva	$$⊢\phi \to F^{-1}\left[A\right]\in S$$