Metamath Proof Explorer

Theorem piord

Description: A positive integer is ordinal. (Contributed by NM, 29-Jan-1996) (New usage is discouraged.)

Ref Expression
Assertion piord 
|- ( A e. N. -> Ord A )

Proof

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