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 ( 𝐴 ∈ 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 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )