Theorem 0n0s

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

	Ref	Expression
Assertion	0n0s	⊢ 0s ∈ ℕ0s

Proof

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