Metamath Proof Explorer

Definition df-7o

Description: Define the ordinal number 7. (Contributed by BTernaryTau, 2-Sep-2026)

Ref Expression
Assertion df-7o 
|- 7o = suc 6o

Detailed syntax breakdown

Step Hyp Ref Expression
0 c7o 
 |-  7o
1 c6o 
 |-  6o
2 1 csuc 
 |-  suc 6o
3 0 2 wceq 
 |-  7o = suc 6o