Theorem n0ssno

Description: The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	n0ssno	⊢ ℕ0s ⊆ No

Proof

Step	Hyp	Ref	Expression
1		df-n0s	⊢ ℕ0s = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 0s ) “ ω )
2	1	a1i	⊢ ( ⊤ → ℕ0s = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 0s ) “ ω ) )
3		0sno	⊢ 0s ∈ No
4	3	a1i	⊢ ( ⊤ → 0s ∈ No )
5	2 4	noseqssno	⊢ ( ⊤ → ℕ0s ⊆ No )
6	5	mptru	⊢ ℕ0s ⊆ No