Definition df-zs

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czs	⊢ ℤs
1		csubs	⊢ -s
2		cnns	⊢ ℕs
3	2 2	cxp	⊢ ( ℕs × ℕs )
4	1 3	cima	⊢ ( -s “ ( ℕs × ℕs ) )
5	0 4	wceq	⊢ ℤs = ( -s “ ( ℕs × ℕs ) )