Metamath Proof Explorer

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 ⊆ Old ⁡ ω

Proof

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