# Metamath Proof Explorer

## Theorem orrvcval4

Description: The value of the preimage mapping operator can be restricted to preimages of subsets of RR. (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Hypotheses orrvccel.1 ${⊢}{\phi }\to {P}\in \mathrm{Prob}$
orrvccel.2 ${⊢}{\phi }\to {X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)$
orrvccel.4 ${⊢}{\phi }\to {A}\in {V}$
Assertion orrvcval4 ${⊢}{\phi }\to {X}{{R}}_{\mathrm{RV/c}}{A}={{X}}^{-1}\left[\left\{{y}\in ℝ|{y}{R}{A}\right\}\right]$

### Proof

Step Hyp Ref Expression
1 orrvccel.1 ${⊢}{\phi }\to {P}\in \mathrm{Prob}$
2 orrvccel.2 ${⊢}{\phi }\to {X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)$
3 orrvccel.4 ${⊢}{\phi }\to {A}\in {V}$
4 domprobsiga ${⊢}{P}\in \mathrm{Prob}\to \mathrm{dom}{P}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
5 1 4 syl ${⊢}{\phi }\to \mathrm{dom}{P}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
6 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
7 6 a1i ${⊢}{\phi }\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
8 1 rrvmbfm ${⊢}{\phi }\to \left({X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)↔{X}\in \left(\mathrm{dom}{P}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)\right)$
9 2 8 mpbid ${⊢}{\phi }\to {X}\in \left(\mathrm{dom}{P}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$
10 df-brsiga ${⊢}{𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
11 10 oveq2i ${⊢}\mathrm{dom}{P}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}=\mathrm{dom}{P}{\mathrm{MblFn}}_{\mu }𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
12 9 11 eleqtrdi ${⊢}{\phi }\to {X}\in \left(\mathrm{dom}{P}{\mathrm{MblFn}}_{\mu }𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\right)$
13 5 7 12 3 orvcval4 ${⊢}{\phi }\to {X}{{R}}_{\mathrm{RV/c}}{A}={{X}}^{-1}\left[\left\{{y}\in \bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)|{y}{R}{A}\right\}\right]$
14 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
15 rabeq ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\to \left\{{y}\in ℝ|{y}{R}{A}\right\}=\left\{{y}\in \bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)|{y}{R}{A}\right\}$
16 14 15 ax-mp ${⊢}\left\{{y}\in ℝ|{y}{R}{A}\right\}=\left\{{y}\in \bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)|{y}{R}{A}\right\}$
17 16 imaeq2i ${⊢}{{X}}^{-1}\left[\left\{{y}\in ℝ|{y}{R}{A}\right\}\right]={{X}}^{-1}\left[\left\{{y}\in \bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)|{y}{R}{A}\right\}\right]$
18 13 17 syl6eqr ${⊢}{\phi }\to {X}{{R}}_{\mathrm{RV/c}}{A}={{X}}^{-1}\left[\left\{{y}\in ℝ|{y}{R}{A}\right\}\right]$