Description: Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 1pi | |- 1o e. N. |
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. |