![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-n0s | Structured version Visualization version GIF version |
Description: Define the set of non-negative surreal integers. This set behaves similarly to ω and ℕ0, 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 12265. (Contributed by Scott Fenton, 17-Mar-2025.) |
Ref | Expression |
---|---|
df-n0s | ⊢ ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnn0s 28333 | . 2 class ℕ0s | |
2 | vx | . . . . 5 setvar 𝑥 | |
3 | cvv 3478 | . . . . 5 class V | |
4 | 2 | cv 1536 | . . . . . 6 class 𝑥 |
5 | c1s 27883 | . . . . . 6 class 1s | |
6 | cadds 28007 | . . . . . 6 class +s | |
7 | 4, 5, 6 | co 7431 | . . . . 5 class (𝑥 +s 1s ) |
8 | 2, 3, 7 | cmpt 5231 | . . . 4 class (𝑥 ∈ V ↦ (𝑥 +s 1s )) |
9 | c0s 27882 | . . . 4 class 0s | |
10 | 8, 9 | crdg 8448 | . . 3 class rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) |
11 | com 7887 | . . 3 class ω | |
12 | 10, 11 | cima 5692 | . 2 class (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω) |
13 | 1, 12 | wceq 1537 | 1 wff ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω) |
Colors of variables: wff setvar class |
This definition is referenced by: n0sex 28337 peano5n0s 28339 n0ssno 28340 0n0s 28349 peano2n0s 28350 n0sind 28352 seqn0sfn 28372 |
Copyright terms: Public domain | W3C validator |