Theorem hashnncl

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

	Ref	Expression
Assertion	hashnncl	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		nnne0	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) ≠ 0 )
2		hashcl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
3		elnn0	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∨ ( ♯ ‘ 𝐴 ) = 0 ) )
4	2 3	sylib	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∨ ( ♯ ‘ 𝐴 ) = 0 ) )
5	4	ord	⊢ ( 𝐴 ∈ Fin → ( ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) = 0 ) )
6	5	necon1ad	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ≠ 0 → ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
7	1 6	impbid2	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ ( ♯ ‘ 𝐴 ) ≠ 0 ) )
8		hasheq0	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )
9	8	necon3bid	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ ∅ ) )
10	7 9	bitrd	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )