Theorem 6onn

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

	Ref	Expression
Assertion	6onn	⊢ 6o ∈ ω

Proof

Step	Hyp	Ref	Expression
1		df-6o	⊢ 6o = suc 5o
2		5onn	⊢ 5o ∈ ω
3		peano2	⊢ ( 5o ∈ ω → suc 5o ∈ ω )
4	2 3	ax-mp	⊢ suc 5o ∈ ω
5	1 4	eqeltri	⊢ 6o ∈ ω