Theorem orvcval

Description: Value of the preimage mapping operator applied on a given random variable and constant. (Contributed by Thierry Arnoux, 19-Jan-2017)

	Ref	Expression
Hypotheses	orvcval.1	|- ( ph -> Fun X )
	orvcval.2	|- ( ph -> X e. V )
	orvcval.3	|- ( ph -> A e. W )
Assertion	orvcval	|- ( ph -> ( X oRVC R A ) = ( `' X " { y | y R A } ) )

Proof

Step	Hyp	Ref	Expression
1		orvcval.1	|- ( ph -> Fun X )
2		orvcval.2	|- ( ph -> X e. V )
3		orvcval.3	|- ( ph -> A e. W )
4		df-orvc	|- oRVC R = ( x e. { x | Fun x } , a e. _V |-> ( `' x " { y | y R a } ) )
5	4	a1i	|- ( ph -> oRVC R = ( x e. { x | Fun x } , a e. _V |-> ( `' x " { y | y R a } ) ) )
6		simpl	|- ( ( x = X /\ a = A ) -> x = X )
7	6	cnveqd	|- ( ( x = X /\ a = A ) -> `' x = `' X )
8		simpr	|- ( ( x = X /\ a = A ) -> a = A )
9	8	breq2d	|- ( ( x = X /\ a = A ) -> ( y R a <-> y R A ) )
10	9	abbidv	|- ( ( x = X /\ a = A ) -> { y | y R a } = { y | y R A } )
11	7 10	imaeq12d	|- ( ( x = X /\ a = A ) -> ( `' x " { y | y R a } ) = ( `' X " { y | y R A } ) )
12	11	adantl	|- ( ( ph /\ ( x = X /\ a = A ) ) -> ( `' x " { y | y R a } ) = ( `' X " { y | y R A } ) )
13		funeq	|- ( x = X -> ( Fun x <-> Fun X ) )
14	2 1 13	elabd	|- ( ph -> X e. { x | Fun x } )
15		elex	|- ( A e. W -> A e. _V )
16	3 15	syl	|- ( ph -> A e. _V )
17		cnvexg	|- ( X e. V -> `' X e. _V )
18		imaexg	|- ( `' X e. _V -> ( `' X " { y | y R A } ) e. _V )
19	2 17 18	3syl	|- ( ph -> ( `' X " { y | y R A } ) e. _V )
20	5 12 14 16 19	ovmpod	|- ( ph -> ( X oRVC R A ) = ( `' X " { y | y R A } ) )