Definition df-n0s

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	⊢ ℕ0s = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 0s ) “ ω )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnn0s	⊢ ℕ0s
1		vx	⊢ 𝑥
2		cvv	⊢ V
3	1	cv	⊢ 𝑥
4		cadds	⊢ +s
5		c1s	⊢ 1s
6	3 5 4	co	⊢ ( 𝑥 +s 1s )
7	1 2 6	cmpt	⊢ ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) )
8		c0s	⊢ 0s
9	7 8	crdg	⊢ rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 0s )
10		com	⊢ ω
11	9 10	cima	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 0s ) “ ω )
12	0 11	wceq	⊢ ℕ0s = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 0s ) “ ω )