Metamath Proof Explorer

Theorem pion

Description: A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion pion 
|- ( A e. N. -> A e. On )

Proof

Step Hyp Ref Expression
1 pinn 
 |-  ( A e. N. -> A e. _om )
2 nnon 
 |-  ( A e. _om -> A e. On )
3 1 2 syl 
 |-  ( A e. N. -> A e. On )