Theorem orvcoel

Description: If the relation produces open sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017)

	Ref	Expression
Hypotheses	orvccel.1	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
	orvccel.2	$$⊢\phi \to J\in \mathrm{Top}$$
	orvccel.3	$$⊢\phi \to X\in \left(S{\mathrm{MblFn}}_{\mu }𝛔\left(J\right)\right)$$
	orvccel.4	$$⊢\phi \to A\in V$$
	orvcoel.5	$$⊢\phi \to \left\{y\in \bigcup J|yRA\right\}\in J$$
Assertion	orvcoel	$$⊢\phi \to X{R}_{\mathrm{RV/c}}A\in S$$

Proof

Step	Hyp	Ref	Expression
1		orvccel.1	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
2		orvccel.2	$$⊢\phi \to J\in \mathrm{Top}$$
3		orvccel.3	$$⊢\phi \to X\in \left(S{\mathrm{MblFn}}_{\mu }𝛔\left(J\right)\right)$$
4		orvccel.4	$$⊢\phi \to A\in V$$
5		orvcoel.5	$$⊢\phi \to \left\{y\in \bigcup J|yRA\right\}\in J$$
6	1 2 3 4	orvcval4	$$⊢\phi \to X{R}_{\mathrm{RV/c}}A=X^{-1}\left[\left\{y\in \bigcup J|yRA\right\}\right]$$
7	2	sgsiga	$$⊢\phi \to 𝛔\left(J\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
8		sssigagen	$$⊢J\in \mathrm{Top}\to J\subseteq 𝛔\left(J\right)$$
9	2 8	syl	$$⊢\phi \to J\subseteq 𝛔\left(J\right)$$
10	9 5	sseldd	$$⊢\phi \to \left\{y\in \bigcup J|yRA\right\}\in 𝛔\left(J\right)$$
11	1 7 3 10	mbfmcnvima	$$⊢\phi \to X^{-1}\left[\left\{y\in \bigcup J|yRA\right\}\right]\in S$$
12	6 11	eqeltrd	$$⊢\phi \to X{R}_{\mathrm{RV/c}}A\in S$$