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