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

Metamath Proof Explorer

Theorem 0npi

Description: The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion 0npi ⊢ ¬ ∅ ∈ 𝑵

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∅ = ∅
2 elni ⊢ ∅ ∈ 𝑵 ↔ ∅ ∈ ω ∧ ∅ ≠ ∅
3 2 simprbi ⊢ ∅ ∈ 𝑵 → ∅ ≠ ∅
4 3 necon2bi ⊢ ∅ = ∅ → ¬ ∅ ∈ 𝑵
5 1 4 ax-mp ⊢ ¬ ∅ ∈ 𝑵