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

Definition df-n0s 28321
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 12268. (Contributed by Scott Fenton, 17-Mar-2025.)
Assertion
Ref Expression
df-n0s 0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)

Detailed syntax breakdown of Definition df-n0s
StepHypRef Expression
1 cnn0s 28319 . 2 class 0s
2 vx . . . . 5 setvar 𝑥
3 cvv 3479 . . . . 5 class V
42cv 1538 . . . . . 6 class 𝑥
5 c1s 27869 . . . . . 6 class 1s
6 cadds 27993 . . . . . 6 class +s
74, 5, 6co 7432 . . . . 5 class (𝑥 +s 1s )
82, 3, 7cmpt 5224 . . . 4 class (𝑥 ∈ V ↦ (𝑥 +s 1s ))
9 c0s 27868 . . . 4 class 0s
108, 9crdg 8450 . . 3 class rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s )
11 com 7888 . . 3 class ω
1210, 11cima 5687 . 2 class (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)
131, 12wceq 1539 1 wff 0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)
Colors of variables: wff setvar class
This definition is referenced by:  n0sex  28323  peano5n0s  28325  n0ssno  28326  0n0s  28335  peano2n0s  28336  n0sind  28338  seqn0sfn  28358
  Copyright terms: Public domain W3C validator