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 ( 𝜑𝑃 ∈ Prob )
orrvccel.2 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
orrvccel.4 ( 𝜑𝐴𝑉 )
Assertion elorrvc ( ( 𝜑𝑧 dom 𝑃 ) → ( 𝑧 ∈ ( 𝑋RV/𝑐 𝑅 𝐴 ) ↔ ( 𝑋𝑧 ) 𝑅 𝐴 ) )

Proof

Step Hyp Ref Expression
1 orrvccel.1 ( 𝜑𝑃 ∈ Prob )
2 orrvccel.2 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3 orrvccel.4 ( 𝜑𝐴𝑉 )
4 1 2 rrvdm ( 𝜑 → dom 𝑋 = dom 𝑃 )
5 4 eleq2d ( 𝜑 → ( 𝑧 ∈ dom 𝑋𝑧 dom 𝑃 ) )
6 5 biimprd ( 𝜑 → ( 𝑧 dom 𝑃𝑧 ∈ dom 𝑋 ) )
7 6 imdistani ( ( 𝜑𝑧 dom 𝑃 ) → ( 𝜑𝑧 ∈ dom 𝑋 ) )
8 1 2 rrvfn ( 𝜑𝑋 Fn dom 𝑃 )
9 fnfun ( 𝑋 Fn dom 𝑃 → Fun 𝑋 )
10 8 9 syl ( 𝜑 → Fun 𝑋 )
11 10 2 3 elorvc ( ( 𝜑𝑧 ∈ dom 𝑋 ) → ( 𝑧 ∈ ( 𝑋RV/𝑐 𝑅 𝐴 ) ↔ ( 𝑋𝑧 ) 𝑅 𝐴 ) )
12 7 11 syl ( ( 𝜑𝑧 dom 𝑃 ) → ( 𝑧 ∈ ( 𝑋RV/𝑐 𝑅 𝐴 ) ↔ ( 𝑋𝑧 ) 𝑅 𝐴 ) )