This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashnncl

Description: Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Assertion hashnncl 
|- ( A e. Fin -> ( ( # ` A ) e. NN <-> A =/= (/) ) )

Proof

Step Hyp Ref Expression
1 nnne0 
 |-  ( ( # ` A ) e. NN -> ( # ` A ) =/= 0 )
2 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
3 elnn0 
 |-  ( ( # ` A ) e. NN0 <-> ( ( # ` A ) e. NN \/ ( # ` A ) = 0 ) )
4 2 3 sylib 
 |-  ( A e. Fin -> ( ( # ` A ) e. NN \/ ( # ` A ) = 0 ) )
5 4 ord 
 |-  ( A e. Fin -> ( -. ( # ` A ) e. NN -> ( # ` A ) = 0 ) )
6 5 necon1ad 
 |-  ( A e. Fin -> ( ( # ` A ) =/= 0 -> ( # ` A ) e. NN ) )
7 1 6 impbid2 
 |-  ( A e. Fin -> ( ( # ` A ) e. NN <-> ( # ` A ) =/= 0 ) )
8 hasheq0 
 |-  ( A e. Fin -> ( ( # ` A ) = 0 <-> A = (/) ) )
9 8 necon3bid 
 |-  ( A e. Fin -> ( ( # ` A ) =/= 0 <-> A =/= (/) ) )
10 7 9 bitrd 
 |-  ( A e. Fin -> ( ( # ` A ) e. NN <-> A =/= (/) ) )