Theorem peano2ons

Description: The successor of a surreal ordinal is a surreal ordinal. (Contributed by Scott Fenton, 22-Aug-2025)

	Ref	Expression
Assertion	peano2ons	⊢ ( 𝐴 ∈ Ons → ( 𝐴 +s 1s ) ∈ Ons )

Proof

Step	Hyp	Ref	Expression
1		1ons	⊢ 1s ∈ Ons
2		onaddscl	⊢ ( ( 𝐴 ∈ Ons ∧ 1s ∈ Ons ) → ( 𝐴 +s 1s ) ∈ Ons )
3	1 2	mpan2	⊢ ( 𝐴 ∈ Ons → ( 𝐴 +s 1s ) ∈ Ons )