Metamath Proof Explorer


Theorem elorrvc

Description: Elementhood of a preimage for a real-valued random variable. (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Hypotheses orrvccel.1 φ P Prob
orrvccel.2 φ X RndVar P
orrvccel.4 φ A V
Assertion elorrvc φ z dom P z X R RV/c A X z R A

Proof

Step Hyp Ref Expression
1 orrvccel.1 φ P Prob
2 orrvccel.2 φ X RndVar P
3 orrvccel.4 φ A V
4 1 2 rrvdm φ dom X = dom P
5 4 eleq2d φ z dom X z dom P
6 5 biimprd φ z dom P z dom X
7 6 imdistani φ z dom P φ z dom X
8 1 2 rrvfn φ X Fn dom P
9 fnfun X Fn dom P Fun X
10 8 9 syl φ Fun X
11 10 2 3 elorvc φ z dom X z X R RV/c A X z R A
12 7 11 syl φ z dom P z X R RV/c A X z R A