Definition df-zs 28774

Description: Define the surreal integers. Compare dfz2 12719. (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 28773	. 2 class ℤs
2		csubs 28415	. . 3 class −s
3		cnns 28708	. . . 4 class ℕs
4	3, 3	cxp 5649	. . 3 class (ℕs × ℕs)
5	2, 4	cima 5654	. 2 class ( −s “ (ℕs × ℕs))
6	1, 5	wceq 1569	1 wff ℤs = ( −s “ (ℕs × ℕs))

This definition is used by:  zsex  28775  zssno  28776  elzs  28779