Theorem coinfliprv

Description: The X we defined for coin-flip is a random variable. (Contributed by Thierry Arnoux, 12-Jan-2017)

	Ref	Expression
Hypotheses	coinflip.h	$$⊢H\in \mathrm{V}$$
	coinflip.t	$$⊢T\in \mathrm{V}$$
	coinflip.th	$$⊢H\ne T$$
	coinflip.2	$$⊢P=\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2$$
	coinflip.3	$$⊢X=\left\{⟨H,1⟩,⟨T,0⟩\right\}$$
Assertion	coinfliprv	$$⊢X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		coinflip.h	$$⊢H\in \mathrm{V}$$
2		coinflip.t	$$⊢T\in \mathrm{V}$$
3		coinflip.th	$$⊢H\ne T$$
4		coinflip.2	$$⊢P=\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2$$
5		coinflip.3	$$⊢X=\left\{⟨H,1⟩,⟨T,0⟩\right\}$$
6		1ex	$$⊢1\in \mathrm{V}$$
7		c0ex	$$⊢0\in \mathrm{V}$$
8	1 2 6 7	fpr	$$⊢H\ne T\to \left\{⟨H,1⟩,⟨T,0⟩\right\}:\left\{H,T\right\}⟶\left\{1,0\right\}$$
9	3 8	ax-mp	$$⊢\left\{⟨H,1⟩,⟨T,0⟩\right\}:\left\{H,T\right\}⟶\left\{1,0\right\}$$
10	5	feq1i	$$⊢X:\left\{H,T\right\}⟶\left\{1,0\right\}\leftrightarrow \left\{⟨H,1⟩,⟨T,0⟩\right\}:\left\{H,T\right\}⟶\left\{1,0\right\}$$
11	9 10	mpbir	$$⊢X:\left\{H,T\right\}⟶\left\{1,0\right\}$$
12	1 2 3 4 5	coinflipuniv	$$⊢\bigcup \mathrm{dom}P=\left\{H,T\right\}$$
13	12	feq2i	$$⊢X:\bigcup \mathrm{dom}P⟶\left\{1,0\right\}\leftrightarrow X:\left\{H,T\right\}⟶\left\{1,0\right\}$$
14	11 13	mpbir	$$⊢X:\bigcup \mathrm{dom}P⟶\left\{1,0\right\}$$
15		1re	$$⊢1\in ℝ$$
16		0re	$$⊢0\in ℝ$$
17	15 16	pm3.2i	$$⊢\left(1\in ℝ\wedge 0\in ℝ\right)$$
18	6 7	prss	$$⊢\left(1\in ℝ\wedge 0\in ℝ\right)\leftrightarrow \left\{1,0\right\}\subseteq ℝ$$
19	17 18	mpbi	$$⊢\left\{1,0\right\}\subseteq ℝ$$
20		fss	$$⊢\left(X:\bigcup \mathrm{dom}P⟶\left\{1,0\right\}\wedge \left\{1,0\right\}\subseteq ℝ\right)\to X:\bigcup \mathrm{dom}P⟶ℝ$$
21	14 19 20	mp2an	$$⊢X:\bigcup \mathrm{dom}P⟶ℝ$$
22		imassrn	$$⊢X^{-1}\left[y\right]\subseteq \mathrm{ran}{X}^{-1}$$
23		dfdm4	$$⊢\mathrm{dom}X=\mathrm{ran}{X}^{-1}$$
24	11	fdmi	$$⊢\mathrm{dom}X=\left\{H,T\right\}$$
25	23 24	eqtr3i	$$⊢\mathrm{ran}{X}^{-1}=\left\{H,T\right\}$$
26	22 25	sseqtri	$$⊢X^{-1}\left[y\right]\subseteq \left\{H,T\right\}$$
27	1 2 3 4 5	coinflipspace	$$⊢\mathrm{dom}P=𝒫\left\{H,T\right\}$$
28	27	eleq2i	$$⊢X^{-1}\left[y\right]\in \mathrm{dom}P\leftrightarrow X^{-1}\left[y\right]\in 𝒫\left\{H,T\right\}$$
29		prex	$$⊢\left\{⟨H,1⟩,⟨T,0⟩\right\}\in \mathrm{V}$$
30	5 29	eqeltri	$$⊢X\in \mathrm{V}$$
31		cnvexg	$$⊢X\in \mathrm{V}\to X^{-1}\in \mathrm{V}$$
32		imaexg	$$⊢X^{-1}\in \mathrm{V}\to X^{-1}\left[y\right]\in \mathrm{V}$$
33	30 31 32	mp2b	$$⊢X^{-1}\left[y\right]\in \mathrm{V}$$
34	33	elpw	$$⊢X^{-1}\left[y\right]\in 𝒫\left\{H,T\right\}\leftrightarrow X^{-1}\left[y\right]\subseteq \left\{H,T\right\}$$
35	28 34	bitr2i	$$⊢X^{-1}\left[y\right]\subseteq \left\{H,T\right\}\leftrightarrow X^{-1}\left[y\right]\in \mathrm{dom}P$$
36	35	biimpi	$$⊢X^{-1}\left[y\right]\subseteq \left\{H,T\right\}\to X^{-1}\left[y\right]\in \mathrm{dom}P$$
37	26 36	mp1i	$$⊢y\in {𝔅}_{ℝ}\to X^{-1}\left[y\right]\in \mathrm{dom}P$$
38	37	rgen	$$⊢\forall y\in {𝔅}_{ℝ}{X}^{-1}\left[y\right]\in \mathrm{dom}P$$
39	1 2 3 4 5	coinflipprob	$$⊢P\in \mathrm{Prob}$$
40	39	a1i	$$⊢H\in \mathrm{V}\to P\in \mathrm{Prob}$$
41	40	isrrvv	$$⊢H\in \mathrm{V}\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)$$
42	1 41	ax-mp	$$⊢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)$$
43	21 38 42	mpbir2an	$$⊢X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$