Theorem coinflipuniv

Description: The universe of our coin-flip probability is { H , T } . (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	coinflipuniv	$$⊢\bigcup \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	1 2 3 4 5	coinflipspace	$$⊢\mathrm{dom}P=𝒫\left\{H,T\right\}$$
7	6	unieqi	$$⊢\bigcup \mathrm{dom}P=\bigcup 𝒫\left\{H,T\right\}$$
8		unipw	$$⊢\bigcup 𝒫\left\{H,T\right\}=\left\{H,T\right\}$$
9	7 8	eqtri	$$⊢\bigcup \mathrm{dom}P=\left\{H,T\right\}$$