Metamath Proof Explorer

Definition df-4o

Description: Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion df-4o 
|- 4o = suc 3o

Detailed syntax breakdown

Step Hyp Ref Expression
0 c4o 
 |-  4o
1 c3o 
 |-  3o
2 1 csuc 
 |-  suc 3o
3 0 2 wceq 
 |-  4o = suc 3o