# Metamath Proof Explorer

## 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}|{y}{R}{A}\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}|{y}{R}{a}\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}|{y}{R}{a}\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({y}{R}{a}↔{y}{R}{A}\right)$
10 9 abbidv ${⊢}\left({x}={X}\wedge {a}={A}\right)\to \left\{{y}|{y}{R}{a}\right\}=\left\{{y}|{y}{R}{A}\right\}$
11 7 10 imaeq12d ${⊢}\left({x}={X}\wedge {a}={A}\right)\to {{x}}^{-1}\left[\left\{{y}|{y}{R}{a}\right\}\right]={{X}}^{-1}\left[\left\{{y}|{y}{R}{A}\right\}\right]$
12 11 adantl ${⊢}\left({\phi }\wedge \left({x}={X}\wedge {a}={A}\right)\right)\to {{x}}^{-1}\left[\left\{{y}|{y}{R}{a}\right\}\right]={{X}}^{-1}\left[\left\{{y}|{y}{R}{A}\right\}\right]$
13 funeq ${⊢}{x}={X}\to \left(\mathrm{Fun}{x}↔\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}|{y}{R}{A}\right\}\right]\in \mathrm{V}$
19 2 17 18 3syl ${⊢}{\phi }\to {{X}}^{-1}\left[\left\{{y}|{y}{R}{A}\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}|{y}{R}{A}\right\}\right]$