Metamath Proof Explorer

Theorem 6onn

Description: The ordinal 6 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026)

Ref Expression
Assertion 6onn 
|- 6o e. _om

Proof

Step Hyp Ref Expression
1 df-6o 
 |-  6o = suc 5o
2 5onn 
 |-  5o e. _om
3 peano2 
 |-  ( 5o e. _om -> suc 5o e. _om )
4 2 3 ax-mp 
 |-  suc 5o e. _om
5 1 4 eqeltri 
 |-  6o e. _om