Theorem isrrvv

Description: Elementhood to the set of real-valued random variables with respect to the probability P . (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Hypothesis	isrrvv.1	|- ( ph -> P e. Prob )
Assertion	isrrvv	|- ( ph -> ( X e. ( rRndVar ` P ) <-> ( X : U. dom P --> RR /\ A. y e. BrSiga ( `' X " y ) e. dom P ) ) )

Proof

Step	Hyp	Ref	Expression
1		isrrvv.1	|- ( ph -> P e. Prob )
2	1	rrvmbfm	|- ( ph -> ( X e. ( rRndVar ` P ) <-> X e. ( dom P MblFnM BrSiga ) ) )
3		domprobsiga	|- ( P e. Prob -> dom P e. U. ran sigAlgebra )
4	1 3	syl	|- ( ph -> dom P e. U. ran sigAlgebra )
5		brsigarn	|- BrSiga e. ( sigAlgebra ` RR )
6		elrnsiga	|- ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra )
7	5 6	mp1i	|- ( ph -> BrSiga e. U. ran sigAlgebra )
8	4 7	ismbfm	|- ( ph -> ( X e. ( dom P MblFnM BrSiga ) <-> ( X e. ( U. BrSiga ^m U. dom P ) /\ A. y e. BrSiga ( `' X " y ) e. dom P ) ) )
9		unibrsiga	|- U. BrSiga = RR
10	9	oveq1i	|- ( U. BrSiga ^m U. dom P ) = ( RR ^m U. dom P )
11	10	eleq2i	|- ( X e. ( U. BrSiga ^m U. dom P ) <-> X e. ( RR ^m U. dom P ) )
12		reex	|- RR e. _V
13	4	uniexd	|- ( ph -> U. dom P e. _V )
14		elmapg	|- ( ( RR e. _V /\ U. dom P e. _V ) -> ( X e. ( RR ^m U. dom P ) <-> X : U. dom P --> RR ) )
15	12 13 14	sylancr	|- ( ph -> ( X e. ( RR ^m U. dom P ) <-> X : U. dom P --> RR ) )
16	11 15	syl5bb	|- ( ph -> ( X e. ( U. BrSiga ^m U. dom P ) <-> X : U. dom P --> RR ) )
17	16	anbi1d	|- ( ph -> ( ( X e. ( U. BrSiga ^m U. dom P ) /\ A. y e. BrSiga ( `' X " y ) e. dom P ) <-> ( X : U. dom P --> RR /\ A. y e. BrSiga ( `' X " y ) e. dom P ) ) )
18	2 8 17	3bitrd	|- ( ph -> ( X e. ( rRndVar ` P ) <-> ( X : U. dom P --> RR /\ A. y e. BrSiga ( `' X " y ) e. dom P ) ) )