Theorem peano2ons

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

	Ref	Expression
Assertion	peano2ons	$$⊢A\in {On}_s\to A{+}_s{1}_s\in {On}_s$$

Proof

Step	Hyp	Ref	Expression
1		1ons	$$⊢1_s\in {On}_s$$
2		onaddscl	$$⊢\left(A\in {On}_s\wedge 1_s\in {On}_s\right)\to A{+}_s{1}_s\in {On}_s$$
3	1 2	mpan2	$$⊢A\in {On}_s\to A{+}_s{1}_s\in {On}_s$$