Metamath Proof Explorer

Theorem 8olt9o

Description: Ordinal 8 is less than ordinal 9. (Contributed by BTernaryTau, 17-Oct-2026)

Ref Expression
Assertion 8olt9o 
|- 8o e. 9o

Proof

Step Hyp Ref Expression
1 8on 
 |-  8o e. On
2 sucidg 
 |-  ( 8o e. On -> 8o e. suc 8o )
3 1 2 ax-mp 
 |-  8o e. suc 8o
4 df-9o 
 |-  9o = suc 8o
5 3 4 eleqtrri 
 |-  8o e. 9o