Metamath Proof Explorer

Theorem coinflippv

Description: The probability of heads is one-half. (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 coinflippv ( 𝑃 ‘ { 𝐻 } ) = ( 1 / 2 )

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 fveq1i ⊢ ( 𝑃 ‘ { 𝐻 } ) = ( ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 ) ‘ { 𝐻 } )
7 snsspr1 ⊢ { 𝐻 } ⊆ { 𝐻 , 𝑇 }
8 prex ⊢ { 𝐻 , 𝑇 } ∈ V
9 8 elpw2 ⊢ ( { 𝐻 } ∈ 𝒫 { 𝐻 , 𝑇 } ↔ { 𝐻 } ⊆ { 𝐻 , 𝑇 } )
10 9 biimpri ⊢ ( { 𝐻 } ⊆ { 𝐻 , 𝑇 } → { 𝐻 } ∈ 𝒫 { 𝐻 , 𝑇 } )
11 fveq2 ⊢ ( 𝑥 = { 𝐻 } → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ { 𝐻 } ) )
12 hashsng ⊢ ( 𝐻 ∈ V → ( ♯ ‘ { 𝐻 } ) = 1 )
13 1 12 ax-mp ⊢ ( ♯ ‘ { 𝐻 } ) = 1
14 11 13 eqtrdi ⊢ ( 𝑥 = { 𝐻 } → ( ♯ ‘ 𝑥 ) = 1 )
15 14 oveq1d ⊢ ( 𝑥 = { 𝐻 } → ( ( ♯ ‘ 𝑥 ) / 2 ) = ( 1 / 2 ) )
16 8 pwex ⊢ 𝒫 { 𝐻 , 𝑇 } ∈ V
17 16 a1i ⊢ ( 𝐻 ∈ V → 𝒫 { 𝐻 , 𝑇 } ∈ V )
18 2nn0 ⊢ 2 ∈ ℕ0
19 18 a1i ⊢ ( 𝐻 ∈ V → 2 ∈ ℕ0 )
20 prfi ⊢ { 𝐻 , 𝑇 } ∈ Fin
21 elpwi ⊢ ( 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } → 𝑥 ⊆ { 𝐻 , 𝑇 } )
22 ssfi ⊢ ( ( { 𝐻 , 𝑇 } ∈ Fin ∧ 𝑥 ⊆ { 𝐻 , 𝑇 } ) → 𝑥 ∈ Fin )
23 20 21 22 sylancr ⊢ ( 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } → 𝑥 ∈ Fin )
24 23 adantl ⊢ ( ( 𝐻 ∈ V ∧ 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ) → 𝑥 ∈ Fin )
25 hashcl ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
26 24 25 syl ⊢ ( ( 𝐻 ∈ V ∧ 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
27 hashf ⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
28 27 a1i ⊢ ( 𝐻 ∈ V → ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) )
29 ssv ⊢ 𝒫 { 𝐻 , 𝑇 } ⊆ V
30 29 a1i ⊢ ( 𝐻 ∈ V → 𝒫 { 𝐻 , 𝑇 } ⊆ V )
31 28 30 feqresmpt ⊢ ( 𝐻 ∈ V → ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) = ( 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ↦ ( ♯ ‘ 𝑥 ) ) )
32 17 19 26 31 ofcfval2 ⊢ ( 𝐻 ∈ V → ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 ) = ( 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ↦ ( ( ♯ ‘ 𝑥 ) / 2 ) ) )
33 1 32 ax-mp ⊢ ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 ) = ( 𝑥 ∈ 𝒫 { 𝐻 , 𝑇 } ↦ ( ( ♯ ‘ 𝑥 ) / 2 ) )
34 ovex ⊢ ( 1 / 2 ) ∈ V
35 15 33 34 fvmpt ⊢ ( { 𝐻 } ∈ 𝒫 { 𝐻 , 𝑇 } → ( ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 ) ‘ { 𝐻 } ) = ( 1 / 2 ) )
36 7 10 35 mp2b ⊢ ( ( ( ♯ ↾ 𝒫 { 𝐻 , 𝑇 } ) ∘f/c / 2 ) ‘ { 𝐻 } ) = ( 1 / 2 )
37 6 36 eqtri ⊢ ( 𝑃 ‘ { 𝐻 } ) = ( 1 / 2 )