Description: Define the ordinal number 1. Definition 2.1 of Schloeder p. 4. (Contributed by NM, 29-Oct-1995)
Ref | Expression | ||
---|---|---|---|
Assertion | df-1o | ⊢ 1o = suc ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | c1o | ⊢ 1o | |
1 | c0 | ⊢ ∅ | |
2 | 1 | csuc | ⊢ suc ∅ |
3 | 0 2 | wceq | ⊢ 1o = suc ∅ |