Theorem orvcelel

Description: Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017)

	Ref	Expression
Hypotheses	dstrvprob.1	$$⊢\phi \to P\in \mathrm{Prob}$$
	dstrvprob.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
	orvcelel.1	$$⊢\phi \to A\in {𝔅}_{ℝ}$$
Assertion	orvcelel	$$⊢\phi \to X{\mathrm{E}}_{\mathrm{RV/c}}A\in \mathrm{dom}P$$

Proof

Step	Hyp	Ref	Expression
1		dstrvprob.1	$$⊢\phi \to P\in \mathrm{Prob}$$
2		dstrvprob.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
3		orvcelel.1	$$⊢\phi \to A\in {𝔅}_{ℝ}$$
4	1 2 3	orvcelval	$$⊢\phi \to X{\mathrm{E}}_{\mathrm{RV/c}}A=X^{-1}\left[A\right]$$
5	1 2	rrvfinvima	$$⊢\phi \to \forall a\in {𝔅}_{ℝ}{X}^{-1}\left[a\right]\in \mathrm{dom}P$$
6		simpr	$$⊢\left(\phi \wedge a=A\right)\to a=A$$
7	6	imaeq2d	$$⊢\left(\phi \wedge a=A\right)\to X^{-1}\left[a\right]=X^{-1}\left[A\right]$$
8	7	eleq1d	$$⊢\left(\phi \wedge a=A\right)\to \left(X^{-1}\left[a\right]\in \mathrm{dom}P\leftrightarrow X^{-1}\left[A\right]\in \mathrm{dom}P\right)$$
9	3 8	rspcdv	$$⊢\phi \to \left(\forall a\in {𝔅}_{ℝ}{X}^{-1}\left[a\right]\in \mathrm{dom}P\to X^{-1}\left[A\right]\in \mathrm{dom}P\right)$$
10	5 9	mpd	$$⊢\phi \to X^{-1}\left[A\right]\in \mathrm{dom}P$$
11	4 10	eqeltrd	$$⊢\phi \to X{\mathrm{E}}_{\mathrm{RV/c}}A\in \mathrm{dom}P$$