Theorem rrvvf

Description: A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Hypotheses	isrrvv.1	$$⊢\phi \to P\in \mathrm{Prob}$$
	rrvvf.1	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
Assertion	rrvvf	$$⊢\phi \to X:\bigcup \mathrm{dom}P⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		isrrvv.1	$$⊢\phi \to P\in \mathrm{Prob}$$
2		rrvvf.1	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
3	1	isrrvv	$$⊢\phi \to \left(X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)\leftrightarrow \left(X:\bigcup \mathrm{dom}P⟶ℝ\wedge \forall y\in {𝔅}_{ℝ}{X}^{-1}\left[y\right]\in \mathrm{dom}P\right)\right)$$
4	2 3	mpbid	$$⊢\phi \to \left(X:\bigcup \mathrm{dom}P⟶ℝ\wedge \forall y\in {𝔅}_{ℝ}{X}^{-1}\left[y\right]\in \mathrm{dom}P\right)$$
5	4	simpld	$$⊢\phi \to X:\bigcup \mathrm{dom}P⟶ℝ$$