Theorem orvcelval

Description: Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-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	orvcelval	$$⊢\phi \to X{\mathrm{E}}_{\mathrm{RV/c}}A=X^{-1}\left[A\right]$$

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	orrvcval4	$$⊢\phi \to X{\mathrm{E}}_{\mathrm{RV/c}}A=X^{-1}\left[\left\{x\in ℝ|x\mathrm{E}A\right\}\right]$$
5		epelg	$$⊢A\in {𝔅}_{ℝ}\to \left(x\mathrm{E}A\leftrightarrow x\in A\right)$$
6	3 5	syl	$$⊢\phi \to \left(x\mathrm{E}A\leftrightarrow x\in A\right)$$
7	6	rabbidv	$$⊢\phi \to \left\{x\in ℝ|x\mathrm{E}A\right\}=\left\{x\in ℝ|x\in A\right\}$$
8		dfin5	$$⊢ℝ\cap A=\left\{x\in ℝ|x\in A\right\}$$
9	8	a1i	$$⊢\phi \to ℝ\cap A=\left\{x\in ℝ|x\in A\right\}$$
10		elssuni	$$⊢A\in {𝔅}_{ℝ}\to A\subseteq \bigcup {𝔅}_{ℝ}$$
11		unibrsiga	$$⊢\bigcup {𝔅}_{ℝ}=ℝ$$
12	10 11	sseqtrdi	$$⊢A\in {𝔅}_{ℝ}\to A\subseteq ℝ$$
13	3 12	syl	$$⊢\phi \to A\subseteq ℝ$$
14		sseqin2	$$⊢A\subseteq ℝ\leftrightarrow ℝ\cap A=A$$
15	13 14	sylib	$$⊢\phi \to ℝ\cap A=A$$
16	7 9 15	3eqtr2d	$$⊢\phi \to \left\{x\in ℝ|x\mathrm{E}A\right\}=A$$
17	16	imaeq2d	$$⊢\phi \to X^{-1}\left[\left\{x\in ℝ|x\mathrm{E}A\right\}\right]=X^{-1}\left[A\right]$$
18	4 17	eqtrd	$$⊢\phi \to X{\mathrm{E}}_{\mathrm{RV/c}}A=X^{-1}\left[A\right]$$