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	⊢ 𝐻 ∈ V
	coinflip.t	⊢ 𝑇 ∈ V
	coinflip.th	⊢ 𝐻 ≠ 𝑇
	coinflip.2	⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 )
	coinflip.3	⊢ 𝑋 = { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ }
Assertion	coinfliprv	⊢ 𝑋 ∈ ( rRndVar ‘ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		coinflip.h	⊢ 𝐻 ∈ V
2		coinflip.t	⊢ 𝑇 ∈ V
3		coinflip.th	⊢ 𝐻 ≠ 𝑇
4		coinflip.2	⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 )
5		coinflip.3	⊢ 𝑋 = { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ }
6		1ex	⊢ 1 ∈ V
7		c0ex	⊢ 0 ∈ V
8	1 2 6 7	fpr	⊢ ( 𝐻 ≠ 𝑇 → { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ } : { 𝐻 , 𝑇 } ⟶ { 1 , 0 } )
9	3 8	ax-mp	⊢ { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ } : { 𝐻 , 𝑇 } ⟶ { 1 , 0 }
10	5	feq1i	⊢ ( 𝑋 : { 𝐻 , 𝑇 } ⟶ { 1 , 0 } ↔ { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ } : { 𝐻 , 𝑇 } ⟶ { 1 , 0 } )
11	9 10	mpbir	⊢ 𝑋 : { 𝐻 , 𝑇 } ⟶ { 1 , 0 }
12	1 2 3 4 5	coinflipuniv	⊢ ∪ dom 𝑃 = { 𝐻 , 𝑇 }
13	12	feq2i	⊢ ( 𝑋 : ∪ dom 𝑃 ⟶ { 1 , 0 } ↔ 𝑋 : { 𝐻 , 𝑇 } ⟶ { 1 , 0 } )
14	11 13	mpbir	⊢ 𝑋 : ∪ dom 𝑃 ⟶ { 1 , 0 }
15		1re	⊢ 1 ∈ ℝ
16		0re	⊢ 0 ∈ ℝ
17	15 16	pm3.2i	⊢ ( 1 ∈ ℝ ∧ 0 ∈ ℝ )
18	6 7	prss	⊢ ( ( 1 ∈ ℝ ∧ 0 ∈ ℝ ) ↔ { 1 , 0 } ⊆ ℝ )
19	17 18	mpbi	⊢ { 1 , 0 } ⊆ ℝ
20		fss	⊢ ( ( 𝑋 : ∪ dom 𝑃 ⟶ { 1 , 0 } ∧ { 1 , 0 } ⊆ ℝ ) → 𝑋 : ∪ dom 𝑃 ⟶ ℝ )
21	14 19 20	mp2an	⊢ 𝑋 : ∪ dom 𝑃 ⟶ ℝ
22		imassrn	⊢ ( ◡ 𝑋 “ 𝑦 ) ⊆ ran ◡ 𝑋
23		dfdm4	⊢ dom 𝑋 = ran ◡ 𝑋
24	11	fdmi	⊢ dom 𝑋 = { 𝐻 , 𝑇 }
25	23 24	eqtr3i	⊢ ran ◡ 𝑋 = { 𝐻 , 𝑇 }
26	22 25	sseqtri	⊢ ( ◡ 𝑋 “ 𝑦 ) ⊆ { 𝐻 , 𝑇 }
27	1 2 3 4 5	coinflipspace	⊢ dom 𝑃 = 𝒫 { 𝐻 , 𝑇 }
28	27	eleq2i	⊢ ( ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ↔ ( ◡ 𝑋 “ 𝑦 ) ∈ 𝒫 { 𝐻 , 𝑇 } )
29		prex	⊢ { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ } ∈ V
30	5 29	eqeltri	⊢ 𝑋 ∈ V
31		cnvexg	⊢ ( 𝑋 ∈ V → ◡ 𝑋 ∈ V )
32		imaexg	⊢ ( ◡ 𝑋 ∈ V → ( ◡ 𝑋 “ 𝑦 ) ∈ V )
33	30 31 32	mp2b	⊢ ( ◡ 𝑋 “ 𝑦 ) ∈ V
34	33	elpw	⊢ ( ( ◡ 𝑋 “ 𝑦 ) ∈ 𝒫 { 𝐻 , 𝑇 } ↔ ( ◡ 𝑋 “ 𝑦 ) ⊆ { 𝐻 , 𝑇 } )
35	28 34	bitr2i	⊢ ( ( ◡ 𝑋 “ 𝑦 ) ⊆ { 𝐻 , 𝑇 } ↔ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 )
36	35	biimpi	⊢ ( ( ◡ 𝑋 “ 𝑦 ) ⊆ { 𝐻 , 𝑇 } → ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 )
37	26 36	mp1i	⊢ ( 𝑦 ∈ 𝔅ℝ → ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 )
38	37	rgen	⊢ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃
39	1 2 3 4 5	coinflipprob	⊢ 𝑃 ∈ Prob
40	39	a1i	⊢ ( 𝐻 ∈ V → 𝑃 ∈ Prob )
41	40	isrrvv	⊢ ( 𝐻 ∈ V → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ ( 𝑋 : ∪ dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ) ) )
42	1 41	ax-mp	⊢ ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ ( 𝑋 : ∪ dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ) )
43	21 38 42	mpbir2an	⊢ 𝑋 ∈ ( rRndVar ‘ 𝑃 )