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 ⊢ A ∈ Fin → 𝒫 A = 2 A

Proof

Step Hyp Ref Expression
1 pweq ⊢ x = A → 𝒫 x = 𝒫 A
2 1 fveq2d ⊢ x = A → 𝒫 x = 𝒫 A
3 fveq2 ⊢ x = A → x = A
4 3 oveq2d ⊢ x = A → 2 x = 2 A
5 2 4 eqeq12d ⊢ x = A → 𝒫 x = 2 x ↔ 𝒫 A = 2 A
6 vex ⊢ x ∈ V
7 6 pw2en ⊢ 𝒫 x ≈ 2 𝑜 x
8 pwfi ⊢ x ∈ Fin ↔ 𝒫 x ∈ Fin
9 8 biimpi ⊢ x ∈ Fin → 𝒫 x ∈ Fin
10 df2o2 ⊢ 2 𝑜 = ∅ ∅
11 prfi ⊢ ∅ ∅ ∈ Fin
12 10 11 eqeltri ⊢ 2 𝑜 ∈ Fin
13 mapfi ⊢ 2 𝑜 ∈ Fin ∧ x ∈ Fin → 2 𝑜 x ∈ Fin
14 12 13 mpan ⊢ x ∈ Fin → 2 𝑜 x ∈ Fin
15 hashen ⊢ 𝒫 x ∈ Fin ∧ 2 𝑜 x ∈ Fin → 𝒫 x = 2 𝑜 x ↔ 𝒫 x ≈ 2 𝑜 x
16 9 14 15 syl2anc ⊢ x ∈ Fin → 𝒫 x = 2 𝑜 x ↔ 𝒫 x ≈ 2 𝑜 x
17 7 16 mpbiri ⊢ x ∈ Fin → 𝒫 x = 2 𝑜 x
18 hashmap ⊢ 2 𝑜 ∈ Fin ∧ x ∈ Fin → 2 𝑜 x = 2 𝑜 x
19 12 18 mpan ⊢ x ∈ Fin → 2 𝑜 x = 2 𝑜 x
20 hash2 ⊢ 2 𝑜 = 2
21 20 oveq1i ⊢ 2 𝑜 x = 2 x
22 19 21 syl6eq ⊢ x ∈ Fin → 2 𝑜 x = 2 x
23 17 22 eqtrd ⊢ x ∈ Fin → 𝒫 x = 2 x
24 5 23 vtoclga ⊢ A ∈ Fin → 𝒫 A = 2 A