Theorem mbfimaopn

Description: The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf , which explains why A e. dom vol is too weak a condition for this theorem.) (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypothesis	mbfimaopn.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	mbfimaopn	$$⊢\left(F\in MblFn\wedge A\in J\right)\to F^{-1}\left[A\right]\in \mathrm{dom}vol$$

Proof

Step	Hyp	Ref	Expression
1		mbfimaopn.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		oveq1	$$⊢t=x\to t+\mathrm{i}w=x+\mathrm{i}w$$
3		oveq2	$$⊢w=y\to \mathrm{i}w=\mathrm{i}y$$
4	3	oveq2d	$$⊢w=y\to x+\mathrm{i}w=x+\mathrm{i}y$$
5	2 4	cbvmpov	$$⊢\left(t\in ℝ,w\in ℝ⟼t+\mathrm{i}w\right)=\left(x\in ℝ,y\in ℝ⟼x+\mathrm{i}y\right)$$
6		eqid	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]=\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]$$
7		eqid	$$⊢\mathrm{ran}\left(x\in \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right],y\in \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]⟼x\times y\right)=\mathrm{ran}\left(x\in \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right],y\in \left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]⟼x\times y\right)$$
8	1 5 6 7	mbfimaopnlem	$$⊢\left(F\in MblFn\wedge A\in J\right)\to F^{-1}\left[A\right]\in \mathrm{dom}vol$$