Theorem n0ssoldg

Description: The non-negative surreal integers are a subset of the old set of _om . To avoid the axiom of infinity, we include it as an antecedent. (Contributed by Scott Fenton, 20-Feb-2026)

	Ref	Expression
Assertion	n0ssoldg	⊢ ( ω ∈ V → ℕ0s ⊆ ( O ‘ ω ) )

Proof

Step	Hyp	Ref	Expression
1		n0sno	⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ No )
2		n0sbday	⊢ ( 𝑥 ∈ ℕ0s → ( bday ‘ 𝑥 ) ∈ ω )
3	1 2	jca	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑥 ∈ No ∧ ( bday ‘ 𝑥 ) ∈ ω ) )
4		omelon2	⊢ ( ω ∈ V → ω ∈ On )
5		oldbday	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ No ) → ( 𝑥 ∈ ( O ‘ ω ) ↔ ( bday ‘ 𝑥 ) ∈ ω ) )
6	5	biimprd	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ No ) → ( ( bday ‘ 𝑥 ) ∈ ω → 𝑥 ∈ ( O ‘ ω ) ) )
7	6	ex	⊢ ( ω ∈ On → ( 𝑥 ∈ No → ( ( bday ‘ 𝑥 ) ∈ ω → 𝑥 ∈ ( O ‘ ω ) ) ) )
8	4 7	syl	⊢ ( ω ∈ V → ( 𝑥 ∈ No → ( ( bday ‘ 𝑥 ) ∈ ω → 𝑥 ∈ ( O ‘ ω ) ) ) )
9	8	impd	⊢ ( ω ∈ V → ( ( 𝑥 ∈ No ∧ ( bday ‘ 𝑥 ) ∈ ω ) → 𝑥 ∈ ( O ‘ ω ) ) )
10	3 9	syl5	⊢ ( ω ∈ V → ( 𝑥 ∈ ℕ0s → 𝑥 ∈ ( O ‘ ω ) ) )
11	10	ssrdv	⊢ ( ω ∈ V → ℕ0s ⊆ ( O ‘ ω ) )