Theorem n0sex

Description: The set of all non-negative surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	n0sex	⊢ ℕ0s ∈ V

Proof

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