Metamath Proof Explorer

Theorem elni2

Description: Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995) (New usage is discouraged.)

Ref Expression
Assertion elni2 ⊢ A ∈ 𝑵 ↔ A ∈ ω ∧ ∅ ∈ A

Proof

Step Hyp Ref Expression
1 elni ⊢ A ∈ 𝑵 ↔ A ∈ ω ∧ A ≠ ∅
2 nnord ⊢ A ∈ ω → Ord ⁡ A
3 ord0eln0 ⊢ Ord ⁡ A → ∅ ∈ A ↔ A ≠ ∅
4 2 3 syl ⊢ A ∈ ω → ∅ ∈ A ↔ A ≠ ∅
5 4 pm5.32i ⊢ A ∈ ω ∧ ∅ ∈ A ↔ A ∈ ω ∧ A ≠ ∅
6 1 5 bitr4i ⊢ A ∈ 𝑵 ↔ A ∈ ω ∧ ∅ ∈ A