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		omex	⊢ ω ∈ V
2		n0sexg	⊢ ( ω ∈ V → ℕ0s ∈ V )
3	1 2	ax-mp	⊢ ℕ0s ∈ V