Theorem rrvdmss

Description: The domain of a random variable. This is useful to shorten proofs. (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	rrvdmss	$$⊢\phi \to \bigcup \mathrm{dom}P\subseteq \mathrm{dom}X$$

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 2	rrvdm	$$⊢\phi \to \mathrm{dom}X=\bigcup \mathrm{dom}P$$
4		eqimss2	$$⊢\mathrm{dom}X=\bigcup \mathrm{dom}P\to \bigcup \mathrm{dom}P\subseteq \mathrm{dom}X$$
5	3 4	syl	$$⊢\phi \to \bigcup \mathrm{dom}P\subseteq \mathrm{dom}X$$