Metamath Proof Explorer

Theorem onltn0s

Description: A surreal ordinal that is less than a non-negative integer is a non-negative integer. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion onltn0s ⊢ A ∈ On s ∧ B ∈ ℕ 0s ∧ A < s B → A ∈ ℕ 0s

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ On s ∧ B ∈ ℕ 0s ∧ A < s B → A ∈ On s
2 n0ons ⊢ B ∈ ℕ 0s → B ∈ On s
3 onslt ⊢ A ∈ On s ∧ B ∈ On s → A < s B ↔ bday ⁡ A ∈ bday ⁡ B
4 2 3 sylan2 ⊢ A ∈ On s ∧ B ∈ ℕ 0s → A < s B ↔ bday ⁡ A ∈ bday ⁡ B
5 4 biimp3a ⊢ A ∈ On s ∧ B ∈ ℕ 0s ∧ A < s B → bday ⁡ A ∈ bday ⁡ B
6 n0sbday ⊢ B ∈ ℕ 0s → bday ⁡ B ∈ ω
7 6 3ad2ant2 ⊢ A ∈ On s ∧ B ∈ ℕ 0s ∧ A < s B → bday ⁡ B ∈ ω
8 elnn ⊢ bday ⁡ A ∈ bday ⁡ B ∧ bday ⁡ B ∈ ω → bday ⁡ A ∈ ω
9 5 7 8 syl2anc ⊢ A ∈ On s ∧ B ∈ ℕ 0s ∧ A < s B → bday ⁡ A ∈ ω
10 onsfi ⊢ A ∈ On s ∧ bday ⁡ A ∈ ω → A ∈ ℕ 0s
11 1 9 10 syl2anc ⊢ A ∈ On s ∧ B ∈ ℕ 0s ∧ A < s B → A ∈ ℕ 0s