Metamath Proof Explorer

Theorem hashsng

Description: The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012) (Proof shortened by Mario Carneiro, 13-Feb-2013)

Ref Expression
Assertion hashsng 
|- ( A e. V -> ( # ` { A } ) = 1 )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 en2sn 
 |-  ( ( A e. V /\ 1 e. ZZ ) -> { A } ~~ { 1 } )
3 1 2 mpan2 
 |-  ( A e. V -> { A } ~~ { 1 } )
4 snfi 
 |-  { A } e. Fin
5 snfi 
 |-  { 1 } e. Fin
6 hashen 
 |-  ( ( { A } e. Fin /\ { 1 } e. Fin ) -> ( ( # ` { A } ) = ( # ` { 1 } ) <-> { A } ~~ { 1 } ) )
7 4 5 6 mp2an 
 |-  ( ( # ` { A } ) = ( # ` { 1 } ) <-> { A } ~~ { 1 } )
8 3 7 sylibr 
 |-  ( A e. V -> ( # ` { A } ) = ( # ` { 1 } ) )
9 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
10 9 fveq2d 
 |-  ( 1 e. ZZ -> ( # ` ( 1 ... 1 ) ) = ( # ` { 1 } ) )
11 1nn0 
 |-  1 e. NN0
12 hashfz1 
 |-  ( 1 e. NN0 -> ( # ` ( 1 ... 1 ) ) = 1 )
13 11 12 ax-mp 
 |-  ( # ` ( 1 ... 1 ) ) = 1
14 10 13 eqtr3di 
 |-  ( 1 e. ZZ -> ( # ` { 1 } ) = 1 )
15 1 14 ax-mp 
 |-  ( # ` { 1 } ) = 1
16 8 15 eqtrdi 
 |-  ( A e. V -> ( # ` { A } ) = 1 )