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