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		n0sbday	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left(n\right)\in \mathrm{\omega }$$
2		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
3		n0sno	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to n\in \mathrm{No}$$
4		oldbday	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge n\in \mathrm{No}\right)\to \left(n\in \mathrm{Old}\left(\mathrm{\omega }\right)\leftrightarrow \mathrm{bday}\left(n\right)\in \mathrm{\omega }\right)$$
5	2 3 4	sylancr	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to \left(n\in \mathrm{Old}\left(\mathrm{\omega }\right)\leftrightarrow \mathrm{bday}\left(n\right)\in \mathrm{\omega }\right)$$
6	1 5	mpbird	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to n\in \mathrm{Old}\left(\mathrm{\omega }\right)$$
7	6	ssriv	$$⊢{\mathbb{N}}_{\mathrm{0s}}\subseteq \mathrm{Old}\left(\mathrm{\omega }\right)$$