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 ↑ ( ♯ ‘ 𝐴 ) ) )