Theorem rrvfinvima

Description: For a real-value random variable X , any open interval in RR is the image of a measurable set. (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	rrvfinvima	$$⊢\phi \to \forall y\in {𝔅}_{ℝ}{X}^{-1}\left[y\right]\in \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	simprd	$$⊢\phi \to \forall y\in {𝔅}_{ℝ}{X}^{-1}\left[y\right]\in \mathrm{dom}P$$