Description: The ordinal 1 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un , see 1onnALT . Lemma 2.2 of Schloeder p. 4. (Contributed by NM, 29-Oct-1995) Avoid ax-un . (Revised by BTernaryTau, 1-Dec-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 1onn | |- 1o e. _om |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1on | |- 1o e. On |
|
| 2 | 1ellim | |- ( Lim x -> 1o e. x ) |
|
| 3 | 2 | ax-gen | |- A. x ( Lim x -> 1o e. x ) |
| 4 | elom | |- ( 1o e. _om <-> ( 1o e. On /\ A. x ( Lim x -> 1o e. x ) ) ) |
|
| 5 | 1 3 4 | mpbir2an | |- 1o e. _om |