Theorem coinflipspace

Description: The space of our coin-flip probability. (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	coinflipspace	$$⊢\mathrm{dom}P=𝒫\left\{H,T\right\}$$

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	dmeqi	$$⊢\mathrm{dom}P=\mathrm{dom}\left(\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2\right)$$
7		hashresfn	$$⊢\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)Fn𝒫\left\{H,T\right\}$$
8	7	a1i	$$⊢H\in \mathrm{V}\to \left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)Fn𝒫\left\{H,T\right\}$$
9		prex	$$⊢\left\{H,T\right\}\in \mathrm{V}$$
10		pwexg	$$⊢\left\{H,T\right\}\in \mathrm{V}\to 𝒫\left\{H,T\right\}\in \mathrm{V}$$
11	9 10	mp1i	$$⊢H\in \mathrm{V}\to 𝒫\left\{H,T\right\}\in \mathrm{V}$$
12		2re	$$⊢2\in ℝ$$
13	12	a1i	$$⊢H\in \mathrm{V}\to 2\in ℝ$$
14	8 11 13	ofcfn	$$⊢H\in \mathrm{V}\to \left(\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2\right)Fn𝒫\left\{H,T\right\}$$
15		fndm	$$⊢\left(\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2\right)Fn𝒫\left\{H,T\right\}\to \mathrm{dom}\left(\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2\right)=𝒫\left\{H,T\right\}$$
16	1 14 15	mp2b	$$⊢\mathrm{dom}\left(\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2\right)=𝒫\left\{H,T\right\}$$
17	6 16	eqtri	$$⊢\mathrm{dom}P=𝒫\left\{H,T\right\}$$