Theorem coinflippvt

Description: The probability of tails is one-half. (Contributed by Thierry Arnoux, 5-Feb-2017)

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

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	coinflipprob	⊢ 𝑃 ∈ Prob
7	1	prid1	⊢ 𝐻 ∈ { 𝐻 , 𝑇 }
8		snelpwi	⊢ ( 𝐻 ∈ { 𝐻 , 𝑇 } → { 𝐻 } ∈ 𝒫 { 𝐻 , 𝑇 } )
9	7 8	ax-mp	⊢ { 𝐻 } ∈ 𝒫 { 𝐻 , 𝑇 }
10	1 2 3 4 5	coinflipspace	⊢ dom 𝑃 = 𝒫 { 𝐻 , 𝑇 }
11	9 10	eleqtrri	⊢ { 𝐻 } ∈ dom 𝑃
12		probdsb	⊢ ( ( 𝑃 ∈ Prob ∧ { 𝐻 } ∈ dom 𝑃 ) → ( 𝑃 ‘ ( ∪ dom 𝑃 ∖ { 𝐻 } ) ) = ( 1 − ( 𝑃 ‘ { 𝐻 } ) ) )
13	6 11 12	mp2an	⊢ ( 𝑃 ‘ ( ∪ dom 𝑃 ∖ { 𝐻 } ) ) = ( 1 − ( 𝑃 ‘ { 𝐻 } ) )
14	1 2 3 4 5	coinflipuniv	⊢ ∪ dom 𝑃 = { 𝐻 , 𝑇 }
15	14	difeq1i	⊢ ( ∪ dom 𝑃 ∖ { 𝐻 } ) = ( { 𝐻 , 𝑇 } ∖ { 𝐻 } )
16		difprsn1	⊢ ( 𝐻 ≠ 𝑇 → ( { 𝐻 , 𝑇 } ∖ { 𝐻 } ) = { 𝑇 } )
17	3 16	ax-mp	⊢ ( { 𝐻 , 𝑇 } ∖ { 𝐻 } ) = { 𝑇 }
18	15 17	eqtri	⊢ ( ∪ dom 𝑃 ∖ { 𝐻 } ) = { 𝑇 }
19	18	fveq2i	⊢ ( 𝑃 ‘ ( ∪ dom 𝑃 ∖ { 𝐻 } ) ) = ( 𝑃 ‘ { 𝑇 } )
20	1 2 3 4 5	coinflippv	⊢ ( 𝑃 ‘ { 𝐻 } ) = ( 1 / 2 )
21	20	oveq2i	⊢ ( 1 − ( 𝑃 ‘ { 𝐻 } ) ) = ( 1 − ( 1 / 2 ) )
22	13 19 21	3eqtr3i	⊢ ( 𝑃 ‘ { 𝑇 } ) = ( 1 − ( 1 / 2 ) )
23		1mhlfehlf	⊢ ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )
24	22 23	eqtri	⊢ ( 𝑃 ‘ { 𝑇 } ) = ( 1 / 2 )