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 φ P Prob
orrvccel.2 φ X RndVar P
orrvccel.4 φ A V
Assertion orrvcval4 φ X R RV/c A = X -1 y | y R A

Proof

Step Hyp Ref Expression
1 orrvccel.1 φ P Prob
2 orrvccel.2 φ X RndVar P
3 orrvccel.4 φ A V
4 domprobsiga P Prob dom P ran sigAlgebra
5 1 4 syl φ dom P ran sigAlgebra
6 retop topGen ran . Top
7 6 a1i φ topGen ran . Top
8 1 rrvmbfm φ X RndVar P X dom P MblFn μ 𝔅
9 2 8 mpbid φ X dom P MblFn μ 𝔅
10 df-brsiga 𝔅 = 𝛔 topGen ran .
11 10 oveq2i dom P MblFn μ 𝔅 = dom P MblFn μ 𝛔 topGen ran .
12 9 11 eleqtrdi φ X dom P MblFn μ 𝛔 topGen ran .
13 5 7 12 3 orvcval4 φ X R RV/c A = X -1 y topGen ran . | y R A
14 uniretop = topGen ran .
15 rabeq = topGen ran . y | y R A = y topGen ran . | y R A
16 14 15 ax-mp y | y R A = y topGen ran . | y R A
17 16 imaeq2i X -1 y | y R A = X -1 y topGen ran . | y R A
18 13 17 eqtr4di φ X R RV/c A = X -1 y | y R A