Theorem rrvmbfm

Description: A real-valued random variable is a measurable function from its sample space to the Borel sigma-algebra. (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Hypothesis	isrrvv.1	$$⊢\phi \to P\in \mathrm{Prob}$$
Assertion	rrvmbfm	$$⊢\phi \to \left(X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)\leftrightarrow X\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isrrvv.1	$$⊢\phi \to P\in \mathrm{Prob}$$
2		dmeq	$$⊢p=P\to \mathrm{dom}p=\mathrm{dom}P$$
3	2	oveq1d	$$⊢p=P\to \mathrm{dom}p{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}=\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}$$
4		df-rrv	$$⊢{\mathrm{RndVar}}_{ℝ}=\left(p\in \mathrm{Prob}⟼\mathrm{dom}p{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)$$
5		ovex	$$⊢\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢P\in \mathrm{Prob}\to {\mathrm{RndVar}}_{ℝ}\left(P\right)=\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}$$
7	1 6	syl	$$⊢\phi \to {\mathrm{RndVar}}_{ℝ}\left(P\right)=\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}$$
8	7	eleq2d	$$⊢\phi \to \left(X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)\leftrightarrow X\in \left(\mathrm{dom}P{\mathrm{MblFn}}_{\mu }{𝔅}_{ℝ}\right)\right)$$