Theorem n0ssold

Description: The non-negative surreal integers are a subset of the old set of _om . (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Assertion	n0ssold	⊢ ℕ0s ⊆ ( O ‘ ω )

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		n0ssoldg	⊢ ( ω ∈ V → ℕ0s ⊆ ( O ‘ ω ) )
3	1 2	ax-mp	⊢ ℕ0s ⊆ ( O ‘ ω )