Metamath Proof Explorer


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 𝑃 = { 𝐻 , 𝑇 }