Theorem coinflippvt

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

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	coinflipprob	|- P e. Prob
7	1	prid1	|- H e. { H , T }
8		snelpwi	|- ( H e. { H , T } -> { H } e. ~P { H , T } )
9	7 8	ax-mp	|- { H } e. ~P { H , T }
10	1 2 3 4 5	coinflipspace	|- dom P = ~P { H , T }
11	9 10	eleqtrri	|- { H } e. dom P
12		probdsb	|- ( ( P e. Prob /\ { H } e. dom P ) -> ( P ` ( U. dom P \ { H } ) ) = ( 1 - ( P ` { H } ) ) )
13	6 11 12	mp2an	|- ( P ` ( U. dom P \ { H } ) ) = ( 1 - ( P ` { H } ) )
14	1 2 3 4 5	coinflipuniv	|- U. dom P = { H , T }
15	14	difeq1i	|- ( U. dom P \ { H } ) = ( { H , T } \ { H } )
16		difprsn1	|- ( H =/= T -> ( { H , T } \ { H } ) = { T } )
17	3 16	ax-mp	|- ( { H , T } \ { H } ) = { T }
18	15 17	eqtri	|- ( U. dom P \ { H } ) = { T }
19	18	fveq2i	|- ( P ` ( U. dom P \ { H } ) ) = ( P ` { T } )
20	1 2 3 4 5	coinflippv	|- ( P ` { H } ) = ( 1 / 2 )
21	20	oveq2i	|- ( 1 - ( P ` { H } ) ) = ( 1 - ( 1 / 2 ) )
22	13 19 21	3eqtr3i	|- ( P ` { T } ) = ( 1 - ( 1 / 2 ) )
23		1mhlfehlf	|- ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
24	22 23	eqtri	|- ( P ` { T } ) = ( 1 / 2 )