Theorem n0ssold

Description: The non-negative surreal integers are a subset of the old set of _om . (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Assertion	n0ssold	⊢ ℕ0s ⊆ ( O ‘ ω )

Proof

Step	Hyp	Ref	Expression
1		n0sbday	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ 𝑛 ) ∈ ω )
2		omelon	⊢ ω ∈ On
3		n0sno	⊢ ( 𝑛 ∈ ℕ0s → 𝑛 ∈ No )
4		oldbday	⊢ ( ( ω ∈ On ∧ 𝑛 ∈ No ) → ( 𝑛 ∈ ( O ‘ ω ) ↔ ( bday ‘ 𝑛 ) ∈ ω ) )
5	2 3 4	sylancr	⊢ ( 𝑛 ∈ ℕ0s → ( 𝑛 ∈ ( O ‘ ω ) ↔ ( bday ‘ 𝑛 ) ∈ ω ) )
6	1 5	mpbird	⊢ ( 𝑛 ∈ ℕ0s → 𝑛 ∈ ( O ‘ ω ) )
7	6	ssriv	⊢ ℕ0s ⊆ ( O ‘ ω )