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 φPProb
orrvccel.2 φXRndVarP
orrvccel.4 φAV
Assertion orrvcval4 φXRRV/cA=X-1y|yRA

Proof

Step Hyp Ref Expression
1 orrvccel.1 φPProb
2 orrvccel.2 φXRndVarP
3 orrvccel.4 φAV
4 domprobsiga PProbdomPransigAlgebra
5 1 4 syl φdomPransigAlgebra
6 retop topGenran.Top
7 6 a1i φtopGenran.Top
8 1 rrvmbfm φXRndVarPXdomPMblFnμ𝔅
9 2 8 mpbid φXdomPMblFnμ𝔅
10 df-brsiga 𝔅=𝛔topGenran.
11 10 oveq2i domPMblFnμ𝔅=domPMblFnμ𝛔topGenran.
12 9 11 eleqtrdi φXdomPMblFnμ𝛔topGenran.
13 5 7 12 3 orvcval4 φXRRV/cA=X-1ytopGenran.|yRA
14 uniretop =topGenran.
15 rabeq =topGenran.y|yRA=ytopGenran.|yRA
16 14 15 ax-mp y|yRA=ytopGenran.|yRA
17 16 imaeq2i X-1y|yRA=X-1ytopGenran.|yRA
18 13 17 eqtr4di φXRRV/cA=X-1y|yRA