Theorem orvcelel

Description: Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-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	orvcelel	|- ( ph -> ( X oRVC _E A ) e. dom P )

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	orvcelval	|- ( ph -> ( X oRVC _E A ) = ( `' X " A ) )
5	1 2	rrvfinvima	|- ( ph -> A. a e. BrSiga ( `' X " a ) e. dom P )
6		simpr	|- ( ( ph /\ a = A ) -> a = A )
7	6	imaeq2d	|- ( ( ph /\ a = A ) -> ( `' X " a ) = ( `' X " A ) )
8	7	eleq1d	|- ( ( ph /\ a = A ) -> ( ( `' X " a ) e. dom P <-> ( `' X " A ) e. dom P ) )
9	3 8	rspcdv	|- ( ph -> ( A. a e. BrSiga ( `' X " a ) e. dom P -> ( `' X " A ) e. dom P ) )
10	5 9	mpd	|- ( ph -> ( `' X " A ) e. dom P )
11	4 10	eqeltrd	|- ( ph -> ( X oRVC _E A ) e. dom P )