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 =/= (/) ) )