Theorem coinflipprob

Description: The P we defined for coin-flip is a probability law. (Contributed by Thierry Arnoux, 15-Jan-2017)

	Ref	Expression
Hypotheses	coinflip.h	⊢ 𝐻 ∈ V
	coinflip.t	⊢ 𝑇 ∈ V
	coinflip.th	⊢ 𝐻 ≠ 𝑇
	coinflip.2	⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 )
	coinflip.3	⊢ 𝑋 = { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ }
Assertion	coinflipprob	⊢ 𝑃 ∈ Prob

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	1 2 3 4 5	coinfliplem	⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c /𝑒 2 )
7		unipw	⊢ ∪ 𝒫 { 𝐻 , 𝑇 } = { 𝐻 , 𝑇 }
8		prex	⊢ { 𝐻 , 𝑇 } ∈ V
9	8	pwid	⊢ { 𝐻 , 𝑇 } ∈ 𝒫 { 𝐻 , 𝑇 }
10	7 9	eqeltri	⊢ ∪ 𝒫 { 𝐻 , 𝑇 } ∈ 𝒫 { 𝐻 , 𝑇 }
11		fvres	⊢ ( ∪ 𝒫 { 𝐻 , 𝑇 } ∈ 𝒫 { 𝐻 , 𝑇 } → ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) = ( ♯ ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) )
12	10 11	ax-mp	⊢ ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) = ( ♯ ‘ ∪ 𝒫 { 𝐻 , 𝑇 } )
13	7	fveq2i	⊢ ( ♯ ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) = ( ♯ ‘ { 𝐻 , 𝑇 } )
14		hashprg	⊢ ( ( 𝐻 ∈ V ∧ 𝑇 ∈ V ) → ( 𝐻 ≠ 𝑇 ↔ ( ♯ ‘ { 𝐻 , 𝑇 } ) = 2 ) )
15	1 2 14	mp2an	⊢ ( 𝐻 ≠ 𝑇 ↔ ( ♯ ‘ { 𝐻 , 𝑇 } ) = 2 )
16	3 15	mpbi	⊢ ( ♯ ‘ { 𝐻 , 𝑇 } ) = 2
17	12 13 16	3eqtri	⊢ ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) = 2
18	17	oveq2i	⊢ ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c /𝑒 ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) ) = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c /𝑒 2 )
19	6 18	eqtr4i	⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c /𝑒 ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) )
20		pwcntmeas	⊢ ( { 𝐻 , 𝑇 } ∈ V → ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∈ ( measures ‘ 𝒫 { 𝐻 , 𝑇 } ) )
21	8 20	ax-mp	⊢ ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∈ ( measures ‘ 𝒫 { 𝐻 , 𝑇 } )
22		2rp	⊢ 2 ∈ ℝ+
23	17 22	eqeltri	⊢ ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) ∈ ℝ+
24		probfinmeasb	⊢ ( ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∈ ( measures ‘ 𝒫 { 𝐻 , 𝑇 } ) ∧ ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) ∈ ℝ+ ) → ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c /𝑒 ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) ) ∈ Prob )
25	21 23 24	mp2an	⊢ ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c /𝑒 ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ‘ ∪ 𝒫 { 𝐻 , 𝑇 } ) ) ∈ Prob
26	19 25	eqeltri	⊢ 𝑃 ∈ Prob