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

Metamath Proof Explorer

Theorem pinn

Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion pinn ( 𝐴 ∈ N → 𝐴 ∈ ω )

Proof

Step Hyp Ref Expression
1 df-ni ⊢ N = ( ω ∖ { ∅ } )
2 difss ⊢ ( ω ∖ { ∅ } ) ⊆ ω
3 1 2 eqsstri ⊢ N ⊆ ω
4 3 sseli ⊢ ( 𝐴 ∈ N → 𝐴 ∈ ω )