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	|- ( ph -> P e. Prob )
	orrvccel.2	|- ( ph -> X e. ( rRndVar ` P ) )
	orrvccel.4	|- ( ph -> A e. V )
Assertion	elorrvc	|- ( ( ph /\ z e. U. dom P ) -> ( z e. ( X oRVC R A ) <-> ( X ` z ) R A ) )

Proof

Step	Hyp	Ref	Expression
1		orrvccel.1	|- ( ph -> P e. Prob )
2		orrvccel.2	|- ( ph -> X e. ( rRndVar ` P ) )
3		orrvccel.4	|- ( ph -> A e. V )
4	1 2	rrvdm	|- ( ph -> dom X = U. dom P )
5	4	eleq2d	|- ( ph -> ( z e. dom X <-> z e. U. dom P ) )
6	5	biimprd	|- ( ph -> ( z e. U. dom P -> z e. dom X ) )
7	6	imdistani	|- ( ( ph /\ z e. U. dom P ) -> ( ph /\ z e. dom X ) )
8	1 2	rrvfn	|- ( ph -> X Fn U. dom P )
9		fnfun	|- ( X Fn U. dom P -> Fun X )
10	8 9	syl	|- ( ph -> Fun X )
11	10 2 3	elorvc	|- ( ( ph /\ z e. dom X ) -> ( z e. ( X oRVC R A ) <-> ( X ` z ) R A ) )
12	7 11	syl	|- ( ( ph /\ z e. U. dom P ) -> ( z e. ( X oRVC R A ) <-> ( X ` z ) R A ) )