Theorem peano2n0s

Description: Peano postulate: the successor of a non-negative surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	peano2n0s	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 1s ) ∈ ℕ0s )

Proof

Step	Hyp	Ref	Expression
1		df-n0s	⊢ ℕ0s = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 0s ) “ ω )
2	1	a1i	⊢ ( 𝐴 ∈ ℕ0s → ℕ0s = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 0s ) “ ω ) )
3		0sno	⊢ 0s ∈ No
4	3	a1i	⊢ ( 𝐴 ∈ ℕ0s → 0s ∈ No )
5		id	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ ℕ0s )
6	2 4 5	noseqp1	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 1s ) ∈ ℕ0s )