This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashpw

Description: The size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by Paul Chapman, 30-Nov-2012) (Proof shortened by Mario Carneiro, 5-Aug-2014)

Ref Expression
Assertion hashpw ( 𝐴 ∈ Fin → ( ♯ ‘ 𝒫 𝐴 ) = ( 2 ↑ ( ♯ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 pweq ⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
2 1 fveq2d ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ 𝒫 𝑥 ) = ( ♯ ‘ 𝒫 𝐴 ) )
3 fveq2 ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) )
4 3 oveq2d ⊢ ( 𝑥 = 𝐴 → ( 2 ↑ ( ♯ ‘ 𝑥 ) ) = ( 2 ↑ ( ♯ ‘ 𝐴 ) ) )
5 2 4 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝒫 𝑥 ) = ( 2 ↑ ( ♯ ‘ 𝑥 ) ) ↔ ( ♯ ‘ 𝒫 𝐴 ) = ( 2 ↑ ( ♯ ‘ 𝐴 ) ) ) )
6 vex ⊢ 𝑥 ∈ V
7 6 pw2en ⊢ 𝒫 𝑥 ≈ ( 2o ↑m 𝑥 )
8 pwfi ⊢ ( 𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Fin )
9 8 biimpi ⊢ ( 𝑥 ∈ Fin → 𝒫 𝑥 ∈ Fin )
10 df2o2 ⊢ 2o = { ∅ , { ∅ } }
11 prfi ⊢ { ∅ , { ∅ } } ∈ Fin
12 10 11 eqeltri ⊢ 2o ∈ Fin
13 mapfi ⊢ ( ( 2o ∈ Fin ∧ 𝑥 ∈ Fin ) → ( 2o ↑m 𝑥 ) ∈ Fin )
14 12 13 mpan ⊢ ( 𝑥 ∈ Fin → ( 2o ↑m 𝑥 ) ∈ Fin )
15 hashen ⊢ ( ( 𝒫 𝑥 ∈ Fin ∧ ( 2o ↑m 𝑥 ) ∈ Fin ) → ( ( ♯ ‘ 𝒫 𝑥 ) = ( ♯ ‘ ( 2o ↑m 𝑥 ) ) ↔ 𝒫 𝑥 ≈ ( 2o ↑m 𝑥 ) ) )
16 9 14 15 syl2anc ⊢ ( 𝑥 ∈ Fin → ( ( ♯ ‘ 𝒫 𝑥 ) = ( ♯ ‘ ( 2o ↑m 𝑥 ) ) ↔ 𝒫 𝑥 ≈ ( 2o ↑m 𝑥 ) ) )
17 7 16 mpbiri ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝒫 𝑥 ) = ( ♯ ‘ ( 2o ↑m 𝑥 ) ) )
18 hashmap ⊢ ( ( 2o ∈ Fin ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 2o ↑m 𝑥 ) ) = ( ( ♯ ‘ 2o ) ↑ ( ♯ ‘ 𝑥 ) ) )
19 12 18 mpan ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ ( 2o ↑m 𝑥 ) ) = ( ( ♯ ‘ 2o ) ↑ ( ♯ ‘ 𝑥 ) ) )
20 hash2 ⊢ ( ♯ ‘ 2o ) = 2
21 20 oveq1i ⊢ ( ( ♯ ‘ 2o ) ↑ ( ♯ ‘ 𝑥 ) ) = ( 2 ↑ ( ♯ ‘ 𝑥 ) )
22 19 21 eqtrdi ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ ( 2o ↑m 𝑥 ) ) = ( 2 ↑ ( ♯ ‘ 𝑥 ) ) )
23 17 22 eqtrd ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝒫 𝑥 ) = ( 2 ↑ ( ♯ ‘ 𝑥 ) ) )
24 5 23 vtoclga ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝒫 𝐴 ) = ( 2 ↑ ( ♯ ‘ 𝐴 ) ) )