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	⊢ 𝐻 ∈ V
	coinflip.t	⊢ 𝑇 ∈ V
	coinflip.th	⊢ 𝐻 ≠ 𝑇
	coinflip.2	⊢ 𝑃 = ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 )
	coinflip.3	⊢ 𝑋 = { ⟨ 𝐻 , 1 ⟩ , ⟨ 𝑇 , 0 ⟩ }
Assertion	coinflipuniv	⊢ ∪ 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	1 2 3 4 5	coinflipspace	⊢ dom 𝑃 = 𝒫 { 𝐻 , 𝑇 }
7	6	unieqi	⊢ ∪ dom 𝑃 = ∪ 𝒫 { 𝐻 , 𝑇 }
8		unipw	⊢ ∪ 𝒫 { 𝐻 , 𝑇 } = { 𝐻 , 𝑇 }
9	7 8	eqtri	⊢ ∪ dom 𝑃 = { 𝐻 , 𝑇 }