Theorem orvcelval

Description: Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017)

	Ref	Expression
Hypotheses	dstrvprob.1	|- ( ph -> P e. Prob )
	dstrvprob.2	|- ( ph -> X e. ( rRndVar ` P ) )
	orvcelel.1	|- ( ph -> A e. BrSiga )
Assertion	orvcelval	|- ( ph -> ( X oRVC _E A ) = ( `' X " A ) )

Proof

Step	Hyp	Ref	Expression
1		dstrvprob.1	|- ( ph -> P e. Prob )
2		dstrvprob.2	|- ( ph -> X e. ( rRndVar ` P ) )
3		orvcelel.1	|- ( ph -> A e. BrSiga )
4	1 2 3	orrvcval4	|- ( ph -> ( X oRVC _E A ) = ( `' X " { x e. RR | x _E A } ) )
5		epelg	|- ( A e. BrSiga -> ( x _E A <-> x e. A ) )
6	3 5	syl	|- ( ph -> ( x _E A <-> x e. A ) )
7	6	rabbidv	|- ( ph -> { x e. RR | x _E A } = { x e. RR | x e. A } )
8		dfin5	|- ( RR i^i A ) = { x e. RR | x e. A }
9	8	a1i	|- ( ph -> ( RR i^i A ) = { x e. RR | x e. A } )
10		elssuni	|- ( A e. BrSiga -> A C_ U. BrSiga )
11		unibrsiga	|- U. BrSiga = RR
12	10 11	sseqtrdi	|- ( A e. BrSiga -> A C_ RR )
13	3 12	syl	|- ( ph -> A C_ RR )
14		sseqin2	|- ( A C_ RR <-> ( RR i^i A ) = A )
15	13 14	sylib	|- ( ph -> ( RR i^i A ) = A )
16	7 9 15	3eqtr2d	|- ( ph -> { x e. RR | x _E A } = A )
17	16	imaeq2d	|- ( ph -> ( `' X " { x e. RR | x _E A } ) = ( `' X " A ) )
18	4 17	eqtrd	|- ( ph -> ( X oRVC _E A ) = ( `' X " A ) )