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 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 syl6eq 
 |-  ( 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 ) ) )