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	$$⊢{\mathbb{N}}_{\mathrm{0s}}\subseteq \mathrm{Old}\left(\mathrm{\omega }\right)$$

Proof

Step	Hyp	Ref	Expression
1		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
2		n0ssoldg	$$⊢\mathrm{\omega }\in \mathrm{V}\to {\mathbb{N}}_{\mathrm{0s}}\subseteq \mathrm{Old}\left(\mathrm{\omega }\right)$$
3	1 2	ax-mp	$$⊢{\mathbb{N}}_{\mathrm{0s}}\subseteq \mathrm{Old}\left(\mathrm{\omega }\right)$$