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 𝒫 𝑥 ≈ ( 2om 𝑥 )
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 ) → ( 2om 𝑥 ) ∈ Fin )
14 12 13 mpan ( 𝑥 ∈ Fin → ( 2om 𝑥 ) ∈ Fin )
15 hashen ( ( 𝒫 𝑥 ∈ Fin ∧ ( 2om 𝑥 ) ∈ Fin ) → ( ( ♯ ‘ 𝒫 𝑥 ) = ( ♯ ‘ ( 2om 𝑥 ) ) ↔ 𝒫 𝑥 ≈ ( 2om 𝑥 ) ) )
16 9 14 15 syl2anc ( 𝑥 ∈ Fin → ( ( ♯ ‘ 𝒫 𝑥 ) = ( ♯ ‘ ( 2om 𝑥 ) ) ↔ 𝒫 𝑥 ≈ ( 2om 𝑥 ) ) )
17 7 16 mpbiri ( 𝑥 ∈ Fin → ( ♯ ‘ 𝒫 𝑥 ) = ( ♯ ‘ ( 2om 𝑥 ) ) )
18 hashmap ( ( 2o ∈ Fin ∧ 𝑥 ∈ Fin ) → ( ♯ ‘ ( 2om 𝑥 ) ) = ( ( ♯ ‘ 2o ) ↑ ( ♯ ‘ 𝑥 ) ) )
19 12 18 mpan ( 𝑥 ∈ Fin → ( ♯ ‘ ( 2om 𝑥 ) ) = ( ( ♯ ‘ 2o ) ↑ ( ♯ ‘ 𝑥 ) ) )
20 hash2 ( ♯ ‘ 2o ) = 2
21 20 oveq1i ( ( ♯ ‘ 2o ) ↑ ( ♯ ‘ 𝑥 ) ) = ( 2 ↑ ( ♯ ‘ 𝑥 ) )
22 19 21 eqtrdi ( 𝑥 ∈ Fin → ( ♯ ‘ ( 2om 𝑥 ) ) = ( 2 ↑ ( ♯ ‘ 𝑥 ) ) )
23 17 22 eqtrd ( 𝑥 ∈ Fin → ( ♯ ‘ 𝒫 𝑥 ) = ( 2 ↑ ( ♯ ‘ 𝑥 ) ) )
24 5 23 vtoclga ( 𝐴 ∈ Fin → ( ♯ ‘ 𝒫 𝐴 ) = ( 2 ↑ ( ♯ ‘ 𝐴 ) ) )