Theorem orvcval

Description: Value of the preimage mapping operator applied on a given random variable and constant. (Contributed by Thierry Arnoux, 19-Jan-2017)

	Ref	Expression
Hypotheses	orvcval.1	$$⊢\phi \to \mathrm{Fun}X$$
	orvcval.2	$$⊢\phi \to X\in V$$
	orvcval.3	$$⊢\phi \to A\in W$$
Assertion	orvcval	$$⊢\phi \to X{R}_{\mathrm{RV/c}}A=X^{-1}\left[\left\{y|yRA\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		orvcval.1	$$⊢\phi \to \mathrm{Fun}X$$
2		orvcval.2	$$⊢\phi \to X\in V$$
3		orvcval.3	$$⊢\phi \to A\in W$$
4		df-orvc	$$⊢{\circ }_{\mathrm{RV/c}}R=\left(x\in \left\{x|\mathrm{Fun}x\right\},a\in \mathrm{V}⟼x^{-1}\left[\left\{y|yRa\right\}\right]\right)$$
5	4	a1i	$$⊢\phi \to {\circ }_{\mathrm{RV/c}}R=\left(x\in \left\{x|\mathrm{Fun}x\right\},a\in \mathrm{V}⟼x^{-1}\left[\left\{y|yRa\right\}\right]\right)$$
6		simpl	$$⊢\left(x=X\wedge a=A\right)\to x=X$$
7	6	cnveqd	$$⊢\left(x=X\wedge a=A\right)\to x^{-1}=X^{-1}$$
8		simpr	$$⊢\left(x=X\wedge a=A\right)\to a=A$$
9	8	breq2d	$$⊢\left(x=X\wedge a=A\right)\to \left(yRa\leftrightarrow yRA\right)$$
10	9	abbidv	$$⊢\left(x=X\wedge a=A\right)\to \left\{y|yRa\right\}=\left\{y|yRA\right\}$$
11	7 10	imaeq12d	$$⊢\left(x=X\wedge a=A\right)\to x^{-1}\left[\left\{y|yRa\right\}\right]=X^{-1}\left[\left\{y|yRA\right\}\right]$$
12	11	adantl	$$⊢\left(\phi \wedge \left(x=X\wedge a=A\right)\right)\to x^{-1}\left[\left\{y|yRa\right\}\right]=X^{-1}\left[\left\{y|yRA\right\}\right]$$
13		funeq	$$⊢x=X\to \left(\mathrm{Fun}x\leftrightarrow \mathrm{Fun}X\right)$$
14	2 1 13	elabd	$$⊢\phi \to X\in \left\{x|\mathrm{Fun}x\right\}$$
15		elex	$$⊢A\in W\to A\in \mathrm{V}$$
16	3 15	syl	$$⊢\phi \to A\in \mathrm{V}$$
17		cnvexg	$$⊢X\in V\to X^{-1}\in \mathrm{V}$$
18		imaexg	$$⊢X^{-1}\in \mathrm{V}\to X^{-1}\left[\left\{y|yRA\right\}\right]\in \mathrm{V}$$
19	2 17 18	3syl	$$⊢\phi \to X^{-1}\left[\left\{y|yRA\right\}\right]\in \mathrm{V}$$
20	5 12 14 16 19	ovmpod	$$⊢\phi \to X{R}_{\mathrm{RV/c}}A=X^{-1}\left[\left\{y|yRA\right\}\right]$$