elorrvc

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

	Ref	Expression
Hypotheses	orrvccel.1	$⊢ φ \to P \in Prob$
	orrvccel.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
	orrvccel.4	$⊢ φ \to A \in V$
Assertion	elorrvc	$⊢ (φ \land z \in ⋃ dom P) \to (z \in (X R_{RV/c} A) \leftrightarrow X (z) R A)$

Step	Hyp	Ref	Expression
1		orrvccel.1	$⊢ φ \to P \in Prob$
2		orrvccel.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
3		orrvccel.4	$⊢ φ \to A \in V$
4	1 2	rrvdm	$⊢ φ \to dom X = ⋃ dom P$
5	4	eleq2d	$⊢ φ \to (z \in dom X \leftrightarrow z \in ⋃ dom P)$
6	5	biimprd	$⊢ φ \to (z \in ⋃ dom P \to z \in dom X)$
7	6	imdistani	$⊢ (φ \land z \in ⋃ dom P) \to (φ \land z \in dom X)$
8	1 2	rrvfn	$⊢ φ \to X Fn ⋃ dom P$
9		fnfun	$⊢ X Fn ⋃ dom P \to Fun X$
10	8 9	syl	$⊢ φ \to Fun X$
11	10 2 3	elorvc	$⊢ (φ \land z \in dom X) \to (z \in (X R_{RV/c} A) \leftrightarrow X (z) R A)$
12	7 11	syl	$⊢ (φ \land z \in ⋃ dom P) \to (z \in (X R_{RV/c} A) \leftrightarrow X (z) R A)$

Metamath Proof Explorer