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