df-zs - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-zs		Structured version Visualization version GIF version

Definition df-zs 28267

Description: Define the surreal integers. Compare dfz2 12548. (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 28266	. 2 class ℤ_s
2		csubs 27926	. . 3 class -_s
3		cnns 28207	. . . 4 class ℕ_s
4	3, 3	cxp 5636	. . 3 class (ℕ_s × ℕ_s)
5	2, 4	cima 5641	. 2 class ( -_s “ (ℕ_s × ℕ_s))
6	1, 5	wceq 1540	1 wff ℤ_s = ( -_s “ (ℕ_s × ℕ_s))

Colors of variables: wff setvar class

This definition is referenced by: zsex 28268 zssno 28269 elzs 28272