Definition df-zs 28352

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

Assertion

Ref	Expression
df-zs	⊢ ℤs = ( -s “ (ℕs × ℕs))

Detailed syntax breakdown of Definition df-zs

Step	Hyp	Ref	Expression
1		czs 28351	. 2 class ℤs
2		csubs 28053	. . 3 class -s
3		cnns 28310	. . . 4 class ℕs
4	3, 3	cxp 5682	. . 3 class (ℕs × ℕs)
5	2, 4	cima 5687	. 2 class ( -s “ (ℕs × ℕs))
6	1, 5	wceq 1534	1 wff ℤs = ( -s “ (ℕs × ℕs))

This definition is referenced by:  zsex  28353  zssno  28354  elzs  28357