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 e. Fin -> ( # ` ~P A ) = ( 2 ^ ( # ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		pweq	|- ( x = A -> ~P x = ~P A )
2	1	fveq2d	|- ( x = A -> ( # ` ~P x ) = ( # ` ~P A ) )
3		fveq2	|- ( x = A -> ( # ` x ) = ( # ` A ) )
4	3	oveq2d	|- ( x = A -> ( 2 ^ ( # ` x ) ) = ( 2 ^ ( # ` A ) ) )
5	2 4	eqeq12d	|- ( x = A -> ( ( # ` ~P x ) = ( 2 ^ ( # ` x ) ) <-> ( # ` ~P A ) = ( 2 ^ ( # ` A ) ) ) )
6		vex	|- x e. _V
7	6	pw2en	|- ~P x ~~ ( 2o ^m x )
8		pwfi	|- ( x e. Fin <-> ~P x e. Fin )
9	8	biimpi	|- ( x e. Fin -> ~P x e. Fin )
10		df2o2	|- 2o = { (/) , { (/) } }
11		prfi	|- { (/) , { (/) } } e. Fin
12	10 11	eqeltri	|- 2o e. Fin
13		mapfi	|- ( ( 2o e. Fin /\ x e. Fin ) -> ( 2o ^m x ) e. Fin )
14	12 13	mpan	|- ( x e. Fin -> ( 2o ^m x ) e. Fin )
15		hashen	|- ( ( ~P x e. Fin /\ ( 2o ^m x ) e. Fin ) -> ( ( # ` ~P x ) = ( # ` ( 2o ^m x ) ) <-> ~P x ~~ ( 2o ^m x ) ) )
16	9 14 15	syl2anc	|- ( x e. Fin -> ( ( # ` ~P x ) = ( # ` ( 2o ^m x ) ) <-> ~P x ~~ ( 2o ^m x ) ) )
17	7 16	mpbiri	|- ( x e. Fin -> ( # ` ~P x ) = ( # ` ( 2o ^m x ) ) )
18		hashmap	|- ( ( 2o e. Fin /\ x e. Fin ) -> ( # ` ( 2o ^m x ) ) = ( ( # ` 2o ) ^ ( # ` x ) ) )
19	12 18	mpan	|- ( x e. Fin -> ( # ` ( 2o ^m x ) ) = ( ( # ` 2o ) ^ ( # ` x ) ) )
20		hash2	|- ( # ` 2o ) = 2
21	20	oveq1i	|- ( ( # ` 2o ) ^ ( # ` x ) ) = ( 2 ^ ( # ` x ) )
22	19 21	eqtrdi	|- ( x e. Fin -> ( # ` ( 2o ^m x ) ) = ( 2 ^ ( # ` x ) ) )
23	17 22	eqtrd	|- ( x e. Fin -> ( # ` ~P x ) = ( 2 ^ ( # ` x ) ) )
24	5 23	vtoclga	|- ( A e. Fin -> ( # ` ~P A ) = ( 2 ^ ( # ` A ) ) )