Metamath Proof Explorer

Theorem 1pi

Description: Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995) (New usage is discouraged.)

Ref Expression
Assertion 1pi 
|- 1o e. N.

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 1n0 
 |-  1o =/= (/)
3 elni 
 |-  ( 1o e. N. <-> ( 1o e. _om /\ 1o =/= (/) ) )
4 1 2 3 mpbir2an 
 |-  1o e. N.