Definition df-zs

Description: Define the surreal integers. Compare dfz2 . (Contributed by Scott Fenton, 17-May-2025)

	Ref	Expression
Assertion	df-zs	$$⊢{\mathbb{Z}}_s={-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czs	$$class{\mathbb{Z}}_s$$
1		csubs	$$class{-}_s$$
2		cnns	$$class{\mathbb{N}}_s$$
3	2 2	cxp	$$class\left({\mathbb{N}}_s\times {\mathbb{N}}_s\right)$$
4	1 3	cima	$$class{-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]$$
5	0 4	wceq	$$wff{\mathbb{Z}}_s={-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]$$