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 
|- 2o = suc 1o

Detailed syntax breakdown

Step Hyp Ref Expression
0 c2o 
 |-  2o
1 c1o 
 |-  1o
2 1 csuc 
 |-  suc 1o
3 0 2 wceq 
 |-  2o = suc 1o