Theorem zssno

Description: The surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-May-2025)

	Ref	Expression
Assertion	zssno	$$⊢{\mathbb{Z}}_s\subseteq \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		imassrn	$$⊢{-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]\subseteq \mathrm{ran}{-}_s$$
2		df-zs	$$⊢{\mathbb{Z}}_s={-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]$$
3		subsfo	$$⊢{-}_s:\mathrm{No}\times \mathrm{No}\underset{onto}{⟶}\mathrm{No}$$
4		forn	$$⊢{-}_s:\mathrm{No}\times \mathrm{No}\underset{onto}{⟶}\mathrm{No}\to \mathrm{ran}{-}_s=\mathrm{No}$$
5	3 4	ax-mp	$$⊢\mathrm{ran}{-}_s=\mathrm{No}$$
6	5	eqcomi	$$⊢\mathrm{No}=\mathrm{ran}{-}_s$$
7	1 2 6	3sstr4i	$$⊢{\mathbb{Z}}_s\subseteq \mathrm{No}$$