Theorem coinflippvt

Description: The probability of tails is one-half. (Contributed by Thierry Arnoux, 5-Feb-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	coinflippvt	$$⊢P\left(\left\{T\right\}\right)=\frac{1}{2}$$

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	1 2 3 4 5	coinflipprob	$$⊢P\in \mathrm{Prob}$$
7	1	prid1	$$⊢H\in \left\{H,T\right\}$$
8		snelpwi	$$⊢H\in \left\{H,T\right\}\to \left\{H\right\}\in 𝒫\left\{H,T\right\}$$
9	7 8	ax-mp	$$⊢\left\{H\right\}\in 𝒫\left\{H,T\right\}$$
10	1 2 3 4 5	coinflipspace	$$⊢\mathrm{dom}P=𝒫\left\{H,T\right\}$$
11	9 10	eleqtrri	$$⊢\left\{H\right\}\in \mathrm{dom}P$$
12		probdsb	$$⊢\left(P\in \mathrm{Prob}\wedge \left\{H\right\}\in \mathrm{dom}P\right)\to P\left(\bigcup \mathrm{dom}P\setminus \left\{H\right\}\right)=1-P\left(\left\{H\right\}\right)$$
13	6 11 12	mp2an	$$⊢P\left(\bigcup \mathrm{dom}P\setminus \left\{H\right\}\right)=1-P\left(\left\{H\right\}\right)$$
14	1 2 3 4 5	coinflipuniv	$$⊢\bigcup \mathrm{dom}P=\left\{H,T\right\}$$
15	14	difeq1i	$$⊢\bigcup \mathrm{dom}P\setminus \left\{H\right\}=\left\{H,T\right\}\setminus \left\{H\right\}$$
16		difprsn1	$$⊢H\ne T\to \left\{H,T\right\}\setminus \left\{H\right\}=\left\{T\right\}$$
17	3 16	ax-mp	$$⊢\left\{H,T\right\}\setminus \left\{H\right\}=\left\{T\right\}$$
18	15 17	eqtri	$$⊢\bigcup \mathrm{dom}P\setminus \left\{H\right\}=\left\{T\right\}$$
19	18	fveq2i	$$⊢P\left(\bigcup \mathrm{dom}P\setminus \left\{H\right\}\right)=P\left(\left\{T\right\}\right)$$
20	1 2 3 4 5	coinflippv	$$⊢P\left(\left\{H\right\}\right)=\frac{1}{2}$$
21	20	oveq2i	$$⊢1-P\left(\left\{H\right\}\right)=1-\left(\frac{1}{2}\right)$$
22	13 19 21	3eqtr3i	$$⊢P\left(\left\{T\right\}\right)=1-\left(\frac{1}{2}\right)$$
23		1mhlfehlf	$$⊢1-\left(\frac{1}{2}\right)=\frac{1}{2}$$
24	22 23	eqtri	$$⊢P\left(\left\{T\right\}\right)=\frac{1}{2}$$