![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-zs | Structured version Visualization version GIF version |
Description: Define the surreal integers. Compare dfz2 12658. (Contributed by Scott Fenton, 17-May-2025.) |
Ref | Expression |
---|---|
df-zs | ⊢ ℤs = ( -s “ (ℕs × ℕs)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | czs 28382 | . 2 class ℤs | |
2 | csubs 28070 | . . 3 class -s | |
3 | cnns 28337 | . . . 4 class ℕs | |
4 | 3, 3 | cxp 5698 | . . 3 class (ℕs × ℕs) |
5 | 2, 4 | cima 5703 | . 2 class ( -s “ (ℕs × ℕs)) |
6 | 1, 5 | wceq 1537 | 1 wff ℤs = ( -s “ (ℕs × ℕs)) |
Colors of variables: wff setvar class |
This definition is referenced by: zsex 28384 zssno 28385 elzs 28388 |
Copyright terms: Public domain | W3C validator |