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.