Metamath Proof Explorer

Theorem 5olt9o

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

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

Proof

Step Hyp Ref Expression
1 5on 
 |-  5o e. On
2 sucidg 
 |-  ( 5o e. On -> 5o e. suc 5o )
3 1 2 ax-mp 
 |-  5o e. suc 5o
4 df-6o 
 |-  6o = suc 5o
5 3 4 eleqtrri 
 |-  5o e. 6o
6 6olt9o 
 |-  6o e. 9o
7 9on 
 |-  9o e. On
8 ontr1 
 |-  ( 9o e. On -> ( ( 5o e. 6o /\ 6o e. 9o ) -> 5o e. 9o ) )
9 7 8 ax-mp 
 |-  ( ( 5o e. 6o /\ 6o e. 9o ) -> 5o e. 9o )
10 5 6 9 mp2an 
 |-  5o e. 9o