Metamath Proof Explorer
Definition df-2o
Description: Define the ordinal number 2. Lemma 3.17 of Schloeder p. 10.
(Contributed by NM, 18-Feb-2004)
|
|
Ref |
Expression |
|
Assertion |
df-2o |
|
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
c2o |
|
1 |
|
c1o |
|
2 |
1
|
csuc |
|
3 |
0 2
|
wceq |
|