Description: Define the set of non-negative surreal integers. This set behaves similarly to _om and NN0 , but it is a set of surreal numbers. Like those two sets, it satisfies the Peano axioms and is closed under (surreal) addition and multiplication. Compare df-nn . (Contributed by Scott Fenton, 17-Mar-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-n0s | |- NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cnn0s | |- NN0_s |
|
| 1 | vx | |- x |
|
| 2 | cvv | |- _V |
|
| 3 | 1 | cv | |- x |
| 4 | cadds | |- +s |
|
| 5 | c1s | |- 1s |
|
| 6 | 3 5 4 | co | |- ( x +s 1s ) |
| 7 | 1 2 6 | cmpt | |- ( x e. _V |-> ( x +s 1s ) ) |
| 8 | c0s | |- 0s |
|
| 9 | 7 8 | crdg | |- rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |
| 10 | com | |- _om |
|
| 11 | 9 10 | cima | |- ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) |
| 12 | 0 11 | wceq | |- NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) |