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 e. _V
	coinflip.t	|- T e. _V
	coinflip.th	|- H =/= T
	coinflip.2	|- P = ( ( # |` ~P { H , T } ) oFC / 2 )
	coinflip.3	|- X = { <. H , 1 >. , <. T , 0 >. }
Assertion	coinflipuniv	|- U. dom P = { H , T }

Proof

Step	Hyp	Ref	Expression
1		coinflip.h	|- H e. _V
2		coinflip.t	|- T e. _V
3		coinflip.th	|- H =/= T
4		coinflip.2	|- P = ( ( # |` ~P { H , T } ) oFC / 2 )
5		coinflip.3	|- X = { <. H , 1 >. , <. T , 0 >. }
6	1 2 3 4 5	coinflipspace	|- dom P = ~P { H , T }
7	6	unieqi	|- U. dom P = U. ~P { H , T }
8		unipw	|- U. ~P { H , T } = { H , T }
9	7 8	eqtri	|- U. dom P = { H , T }