# Metamath Proof Explorer

## Theorem orrvccel

Description: If the relation produces closed sets, preimage maps are measurable sets. (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}$
orrvccel.5 ${⊢}{\phi }\to \left\{{y}\in ℝ|{y}{R}{A}\right\}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
Assertion orrvccel ${⊢}{\phi }\to {X}{{R}}_{\mathrm{RV/c}}{A}\in \mathrm{dom}{P}$

### 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 orrvccel.5 ${⊢}{\phi }\to \left\{{y}\in ℝ|{y}{R}{A}\right\}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
5 domprobsiga ${⊢}{P}\in \mathrm{Prob}\to \mathrm{dom}{P}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
6 1 5 syl ${⊢}{\phi }\to \mathrm{dom}{P}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
7 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
8 7 a1i ${⊢}{\phi }\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
9 1 rrvmbfm ${⊢}{\phi }\to \left({X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)↔{X}\in \left(\mathrm{dom}{P}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)\right)$
10 2 9 mpbid ${⊢}{\phi }\to {X}\in \left(\mathrm{dom}{P}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$
11 df-brsiga ${⊢}{𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
12 11 oveq2i ${⊢}\mathrm{dom}{P}{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}=\mathrm{dom}{P}{\mathrm{MblFn}}_{\mu }𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
13 10 12 eleqtrdi ${⊢}{\phi }\to {X}\in \left(\mathrm{dom}{P}{\mathrm{MblFn}}_{\mu }𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\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 4 eqeltrrid ${⊢}{\phi }\to \left\{{y}\in \bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)|{y}{R}{A}\right\}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
18 6 8 13 3 17 orvccel ${⊢}{\phi }\to {X}{{R}}_{\mathrm{RV/c}}{A}\in \mathrm{dom}{P}$