Theorem coinflippv

Description: The probability of heads is one-half. (Contributed by Thierry Arnoux, 15-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	coinflippv	$$⊢P\left(\left\{H\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	4	fveq1i	$$⊢P\left(\left\{H\right\}\right)=\left(\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2\right)\left(\left\{H\right\}\right)$$
7		snsspr1	$$⊢\left\{H\right\}\subseteq \left\{H,T\right\}$$
8		prex	$$⊢\left\{H,T\right\}\in \mathrm{V}$$
9	8	elpw2	$$⊢\left\{H\right\}\in 𝒫\left\{H,T\right\}\leftrightarrow \left\{H\right\}\subseteq \left\{H,T\right\}$$
10	9	biimpri	$$⊢\left\{H\right\}\subseteq \left\{H,T\right\}\to \left\{H\right\}\in 𝒫\left\{H,T\right\}$$
11		fveq2	$$⊢x=\left\{H\right\}\to \left|x\right|=\left|\left\{H\right\}\right|$$
12		hashsng	$$⊢H\in \mathrm{V}\to \left|\left\{H\right\}\right|=1$$
13	1 12	ax-mp	$$⊢\left|\left\{H\right\}\right|=1$$
14	11 13	eqtrdi	$$⊢x=\left\{H\right\}\to \left|x\right|=1$$
15	14	oveq1d	$$⊢x=\left\{H\right\}\to \frac{\left|x\right|}{2}=\frac{1}{2}$$
16	8	pwex	$$⊢𝒫\left\{H,T\right\}\in \mathrm{V}$$
17	16	a1i	$$⊢H\in \mathrm{V}\to 𝒫\left\{H,T\right\}\in \mathrm{V}$$
18		2nn0	$$⊢2\in {\mathbb{N}}_0$$
19	18	a1i	$$⊢H\in \mathrm{V}\to 2\in {\mathbb{N}}_0$$
20		prfi	$$⊢\left\{H,T\right\}\in \mathrm{Fin}$$
21		elpwi	$$⊢x\in 𝒫\left\{H,T\right\}\to x\subseteq \left\{H,T\right\}$$
22		ssfi	$$⊢\left(\left\{H,T\right\}\in \mathrm{Fin}\wedge x\subseteq \left\{H,T\right\}\right)\to x\in \mathrm{Fin}$$
23	20 21 22	sylancr	$$⊢x\in 𝒫\left\{H,T\right\}\to x\in \mathrm{Fin}$$
24	23	adantl	$$⊢\left(H\in \mathrm{V}\wedge x\in 𝒫\left\{H,T\right\}\right)\to x\in \mathrm{Fin}$$
25		hashcl	$$⊢x\in \mathrm{Fin}\to \left|x\right|\in {\mathbb{N}}_0$$
26	24 25	syl	$$⊢\left(H\in \mathrm{V}\wedge x\in 𝒫\left\{H,T\right\}\right)\to \left|x\right|\in {\mathbb{N}}_0$$
27		hashf	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
28	27	a1i	$$⊢H\in \mathrm{V}\to \left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
29		ssv	$$⊢𝒫\left\{H,T\right\}\subseteq \mathrm{V}$$
30	29	a1i	$$⊢H\in \mathrm{V}\to 𝒫\left\{H,T\right\}\subseteq \mathrm{V}$$
31	28 30	feqresmpt	$$⊢H\in \mathrm{V}\to {\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}=\left(x\in 𝒫\left\{H,T\right\}⟼\left|x\right|\right)$$
32	17 19 26 31	ofcfval2	$$⊢H\in \mathrm{V}\to \left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2=\left(x\in 𝒫\left\{H,T\right\}⟼\frac{\left|x\right|}{2}\right)$$
33	1 32	ax-mp	$$⊢\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2=\left(x\in 𝒫\left\{H,T\right\}⟼\frac{\left|x\right|}{2}\right)$$
34		ovex	$$⊢\frac{1}{2}\in \mathrm{V}$$
35	15 33 34	fvmpt	$$⊢\left\{H\right\}\in 𝒫\left\{H,T\right\}\to \left(\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2\right)\left(\left\{H\right\}\right)=\frac{1}{2}$$
36	7 10 35	mp2b	$$⊢\left(\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2\right)\left(\left\{H\right\}\right)=\frac{1}{2}$$
37	6 36	eqtri	$$⊢P\left(\left\{H\right\}\right)=\frac{1}{2}$$