Theorem coinflipspace

Description: The space of our coin-flip probability. (Contributed by Thierry Arnoux, 15-Jan-2017)

	Ref	Expression
Hypotheses	coinflip.h	⊢ 𝐻 ∈ V
	coinflip.t	⊢ 𝑇 ∈ V
	coinflip.th	⊢ 𝐻 ≠ 𝑇
	coinflip.2	⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 )
	coinflip.3	⊢ 𝑋 = { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ }
Assertion	coinflipspace	⊢ dom 𝑃 = 𝒫 { 𝐻 , 𝑇 }

Proof

Step	Hyp	Ref	Expression
1		coinflip.h	⊢ 𝐻 ∈ V
2		coinflip.t	⊢ 𝑇 ∈ V
3		coinflip.th	⊢ 𝐻 ≠ 𝑇
4		coinflip.2	⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 )
5		coinflip.3	⊢ 𝑋 = { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ }
6	4	dmeqi	⊢ dom 𝑃 = dom ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 )
7		hashresfn	⊢ ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) Fn 𝒫 { 𝐻 , 𝑇 }
8	7	a1i	⊢ ( 𝐻 ∈ V → ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) Fn 𝒫 { 𝐻 , 𝑇 } )
9		prex	⊢ { 𝐻 , 𝑇 } ∈ V
10		pwexg	⊢ ( { 𝐻 , 𝑇 } ∈ V → 𝒫 { 𝐻 , 𝑇 } ∈ V )
11	9 10	mp1i	⊢ ( 𝐻 ∈ V → 𝒫 { 𝐻 , 𝑇 } ∈ V )
12		2re	⊢ 2 ∈ ℝ
13	12	a1i	⊢ ( 𝐻 ∈ V → 2 ∈ ℝ )
14	8 11 13	ofcfn	⊢ ( 𝐻 ∈ V → ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 ) Fn 𝒫 { 𝐻 , 𝑇 } )
15		fndm	⊢ ( ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 ) Fn 𝒫 { 𝐻 , 𝑇 } → dom ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 ) = 𝒫 { 𝐻 , 𝑇 } )
16	1 14 15	mp2b	⊢ dom ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 ) = 𝒫 { 𝐻 , 𝑇 }
17	6 16	eqtri	⊢ dom 𝑃 = 𝒫 { 𝐻 , 𝑇 }