P. 283 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28201-28300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	divs1d 28201	A surreal divided by one is itself. Deduction version. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 /su 1s ) = 𝐴)
Theorem	precsexlemcbv 28202*	Lemma for surreal reciprocals. Change some bound variables. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    ⇒   ⊢ 𝐹 = rec((𝑞 ∈ V ↦ ⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑡)) /su 𝑧𝑅)}))⟩), ⟨{ 0s }, ∅⟩)
Theorem	precsexlem1 28203	Lemma for surreal reciprocals. Calculate the value of the recursive left function at zero. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ (𝐿‘∅) = { 0s }
Theorem	precsexlem2 28204	Lemma for surreal reciprocals. Calculate the value of the recursive right function at zero. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ (𝑅‘∅) = ∅
Theorem	precsexlem3 28205*	Lemma for surreal reciprocals. Calculate the value of the recursive function at a successor. (Contributed by Scott Fenton, 12-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ (𝐼 ∈ ω → (𝐹‘suc 𝐼) = ⟨((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), ((𝑅‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩)
Theorem	precsexlem4 28206*	Lemma for surreal reciprocals. Calculate the value of the recursive left function at a successor. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ (𝐼 ∈ ω → (𝐿‘suc 𝐼) = ((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
Theorem	precsexlem5 28207*	Lemma for surreal reciprocals. Calculate the value of the recursive right function at a successor. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ (𝐼 ∈ ω → (𝑅‘suc 𝐼) = ((𝑅‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
Theorem	precsexlem6 28208*	Lemma for surreal reciprocal. Show that 𝐿 is non-strictly increasing in its argument. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐼 ⊆ 𝐽) → (𝐿‘𝐼) ⊆ (𝐿‘𝐽))
Theorem	precsexlem7 28209*	Lemma for surreal reciprocal. Show that 𝑅 is non-strictly increasing in its argument. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    ⇒   ⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐼 ⊆ 𝐽) → (𝑅‘𝐼) ⊆ (𝑅‘𝐽))
Theorem	precsexlem8 28210*	Lemma for surreal reciprocal. Show that the left and right functions give sets of surreals. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No ))
Theorem	precsexlem9 28211*	Lemma for surreal reciprocal. Show that the product of 𝐴 and a left element is less than one and the product of 𝐴 and a right element is greater than one. (Contributed by Scott Fenton, 14-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))
Theorem	precsexlem10 28212*	Lemma for surreal reciprocal. Show that the union of the left sets is less than the union of the right sets. Note that this is the first theorem in the surreal numbers to require the axiom of infinity. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    ⇒   ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω))
Theorem	precsexlem11 28213*	Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for 𝐴. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)    &   ⊢ 𝐿 = (1st ∘ 𝐹)    &   ⊢ 𝑅 = (2nd ∘ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    &   ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))    &   ⊢ 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝑌) = 1s )
Theorem	precsex 28214*	Every positive surreal has a reciprocal. Theorem 10(iv) of [Conway] p. 21. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 0s <s 𝐴) → ∃𝑦 ∈ No (𝐴 ·s 𝑦) = 1s )
Theorem	recsex 28215*	A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s )
Theorem	recsexd 28216*	A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≠ 0s )    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s )
Theorem	divmuls 28217	Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ (𝐶 ∈ No ∧ 𝐶 ≠ 0s )) → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴))
Theorem	divmulsd 28218	Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴))
Theorem	divscl 28219	Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) → (𝐴 /su 𝐵) ∈ No )
Theorem	divscld 28220	Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → (𝐴 /su 𝐵) ∈ No )
Theorem	divscan2d 28221	A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → (𝐵 ·s (𝐴 /su 𝐵)) = 𝐴)
Theorem	divscan1d 28222	A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s 𝐵) = 𝐴)
Theorem	ltdivmulsd 28223	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐶 ·s 𝐵)))
Theorem	ltdivmuls2d 28224	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 ·s 𝐶)))
Theorem	ltmuldivsd 28225	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶)))
Theorem	ltmuldivs2d 28226	Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐶)    ⇒   ⊢ (𝜑 → ((𝐶 ·s 𝐴) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶)))
Theorem	divsassd 28227	An associative law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 ·s 𝐵) /su 𝐶) = (𝐴 ·s (𝐵 /su 𝐶)))
Theorem	divmuldivsd 28228	Multiplication of two surreal ratios. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐷 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → 𝐷 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s (𝐶 /su 𝐷)) = ((𝐴 ·s 𝐶) /su (𝐵 ·s 𝐷)))
Theorem	divdivs1d 28229	Surreal division into a fraction. (Contributed by Scott Fenton, 7-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 /su 𝐵) /su 𝐶) = (𝐴 /su (𝐵 ·s 𝐶)))
Theorem	divsrecd 28230	Relationship between surreal division and reciprocal. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → (𝐴 /su 𝐵) = (𝐴 ·s ( 1s /su 𝐵)))
Theorem	divsdird 28231	Distribution of surreal division over addition. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐶 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) /su 𝐶) = ((𝐴 /su 𝐶) +s (𝐵 /su 𝐶)))
Theorem	divscan3d 28232	A cancellation law for surreal division. (Contributed by Scott Fenton, 13-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐵 ≠ 0s )    ⇒   ⊢ (𝜑 → ((𝐵 ·s 𝐴) /su 𝐵) = 𝐴)
15.5.5  Absolute value
Syntax	cabss 28233	Declare the syntax for surreal absolute value.
class abss
Definition	df-abss 28234	Define the surreal absolute value function. See abssval 28235 for its value and absscl 28236 for its closure. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ abss = (𝑥 ∈ No ↦ if( 0s ≤s 𝑥, 𝑥, ( -us ‘𝑥)))
Theorem	abssval 28235	The value of surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘𝐴) = if( 0s ≤s 𝐴, 𝐴, ( -us ‘𝐴)))
Theorem	absscl 28236	Closure law for surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘𝐴) ∈ No )
Theorem	abssid 28237	The absolute value of a non-negative surreal is itself. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 0s ≤s 𝐴) → (abss‘𝐴) = 𝐴)
Theorem	abs0s 28238	The absolute value of surreal zero. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (abss‘ 0s ) = 0s
Theorem	abssnid 28239	For a negative surreal, its absolute value is its negation. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → (abss‘𝐴) = ( -us ‘𝐴))
Theorem	absmuls 28240	Surreal absolute value distributes over multiplication. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (abss‘(𝐴 ·s 𝐵)) = ((abss‘𝐴) ·s (abss‘𝐵)))
Theorem	abssge0 28241	The absolute value of a surreal number is non-negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → 0s ≤s (abss‘𝐴))
Theorem	abssor 28242	The absolute value of a surreal is either that surreal or its negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → ((abss‘𝐴) = 𝐴 ∨ (abss‘𝐴) = ( -us ‘𝐴)))
Theorem	absnegs 28243	Surreal absolute value of the negative. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → (abss‘( -us ‘𝐴)) = (abss‘𝐴))
Theorem	leabss 28244	A surreal is less than or equal to its absolute value. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ (𝐴 ∈ No → 𝐴 ≤s (abss‘𝐴))
Theorem	abslts 28245	Surreal absolute value and less-than relation. (Contributed by Scott Fenton, 16-Apr-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((abss‘𝐴) <s 𝐵 ↔ (( -us ‘𝐵) <s 𝐴 ∧ 𝐴 <s 𝐵)))
Theorem	abssubs 28246	Swapping order of surreal subtraction doesn't change the absolute value. (Contributed by Scott Fenton, 29-Jan-2026.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (abss‘(𝐴 -s 𝐵)) = (abss‘(𝐵 -s 𝐴)))
15.6  Subsystems of surreals
15.6.1  Ordinal numbers
Syntax	cons 28247	Declare the syntax for surreal ordinals.
class Ons
Definition	df-ons 28248	Define the surreal ordinals. These are the maximum members of each generation of surreals. Variant of definition from [Conway] p. 27. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ Ons = {𝑥 ∈ No ∣ ( R ‘𝑥) = ∅}
Theorem	elons 28249	Membership in the class of surreal ordinals. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ (𝐴 ∈ Ons ↔ (𝐴 ∈ No ∧ ( R ‘𝐴) = ∅))
Theorem	onssno 28250	The surreal ordinals are a subclass of the surreals. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ Ons ⊆ No
Theorem	onno 28251	A surreal ordinal is a surreal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ (𝐴 ∈ Ons → 𝐴 ∈ No )
Theorem	0ons 28252	Surreal zero is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ 0s ∈ Ons
Theorem	1ons 28253	Surreal one is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.)
⊢ 1s ∈ Ons
Theorem	elons2 28254*	A surreal is ordinal iff it is the cut of some set of surreals and the empty set. Definition from [Conway] p. 27. (Contributed by Scott Fenton, 19-Mar-2025.)
⊢ (𝐴 ∈ Ons ↔ ∃𝑎 ∈ 𝒫 No 𝐴 = (𝑎 |s ∅))
Theorem	elons2d 28255	The cut of any set of surreals and the empty set is a surreal ordinal. (Contributed by Scott Fenton, 19-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ No )    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s ∅))    ⇒   ⊢ (𝜑 → 𝑋 ∈ Ons)
Theorem	onleft 28256	The left set of a surreal ordinal is the same as its old set. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ (𝐴 ∈ Ons → ( O ‘( bday ‘𝐴)) = ( L ‘𝐴))
Theorem	ltonold 28257*	The class of ordinals less than any surreal is a subset of that surreal's old set. (Contributed by Scott Fenton, 22-Mar-2025.)
⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ⊆ ( O ‘( bday ‘𝐴)))
Theorem	ltonsex 28258*	The class of ordinals less than any particular surreal is a set. Theorem 14 of [Conway] p. 27. (Contributed by Scott Fenton, 22-Mar-2025.)
⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ∈ V)
Theorem	oncutleft 28259	A surreal ordinal is equal to the cut of its left set and the empty set. (Contributed by Scott Fenton, 29-Mar-2025.)
⊢ (𝐴 ∈ Ons → 𝐴 = (( L ‘𝐴) |s ∅))
Theorem	oncutlt 28260*	A surreal ordinal is the simplest number greater than all previous surreal ordinals. Theorem 15 of [Conway] p. 28. (Contributed by Scott Fenton, 4-Nov-2025.)
⊢ (𝐴 ∈ Ons → 𝐴 = ({𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} |s ∅))
Theorem	bday11on 28261	The birthday function is one-to-one over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘𝐴) = ( bday ‘𝐵)) → 𝐴 = 𝐵)
Theorem	onnolt 28262	If a surreal ordinal is less than a given surreal, then it is simpler. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → ( bday ‘𝐴) ∈ ( bday ‘𝐵))
Theorem	onlts 28263	Less-than is the same as birthday comparison over surreal ordinals. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 <s 𝐵 ↔ ( bday ‘𝐴) ∈ ( bday ‘𝐵)))
Theorem	onles 28264	Less-than or equal is the same as non-strict birthday comparison over surreal ordinals. (Contributed by Scott Fenton, 25-Feb-2026.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 ≤s 𝐵 ↔ ( bday ‘𝐴) ⊆ ( bday ‘𝐵)))
Theorem	onltsd 28265	Less-than is the same as birthday comparison over surreal ordinals. Deduction version. (Contributed by Scott Fenton, 25-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ Ons)    &   ⊢ (𝜑 → 𝐵 ∈ Ons)    ⇒   ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ( bday ‘𝐴) ∈ ( bday ‘𝐵)))
Theorem	onlesd 28266	Less-than or equal is the same as non-strict birthday comparison over surreal ordinals. Deduction version. (Contributed by Scott Fenton, 25-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ Ons)    &   ⊢ (𝜑 → 𝐵 ∈ Ons)    ⇒   ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ ( bday ‘𝐴) ⊆ ( bday ‘𝐵)))
Theorem	oniso 28267	The birthday function restricted to the surreal ordinals forms an order-preserving isomorphism with the regular ordinals. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ( bday ↾ Ons) Isom <s , E (Ons, On)
Theorem	onswe 28268	Surreal less-than well-orders the surreal ordinals. Part of Theorem 15 of [Conway] p. 28. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ <s We Ons
Theorem	onsse 28269	Surreal less-than is set-like over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ <s Se Ons
Theorem	onsis 28270*	Transfinite induction schema for surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ Ons → (∀𝑦 ∈ Ons (𝑦 <s 𝑥 → 𝜓) → 𝜑))    ⇒   ⊢ (𝐴 ∈ Ons → 𝜒)
Theorem	ons2ind 28271*	Double induction schema for surreal ordinals. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ (𝑥 = 𝑥𝑂 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑦𝑂 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑥𝑂 → (𝜃 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑦 = 𝐵 → (𝜏 ↔ 𝜂))    &   ⊢ ((𝑥 ∈ Ons ∧ 𝑦 ∈ Ons) → ((∀𝑥𝑂 ∈ Ons ∀𝑦𝑂 ∈ Ons ((𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦) → 𝜒) ∧ ∀𝑥𝑂 ∈ Ons (𝑥𝑂 <s 𝑥 → 𝜓) ∧ ∀𝑦𝑂 ∈ Ons (𝑦𝑂 <s 𝑦 → 𝜃)) → 𝜑))    ⇒   ⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → 𝜂)
Theorem	bdayons 28272*	The birthday of a surreal ordinal is the set of all previous ordinal birthdays. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ Ons → ( bday ‘𝐴) = ( bday “ {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴}))
Theorem	onaddscl 28273	The surreal ordinals are closed under addition. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 +s 𝐵) ∈ Ons)
Theorem	onmulscl 28274	The surreal ordinals are closed under multiplication. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 ·s 𝐵) ∈ Ons)
Theorem	addonbday 28275	The birthday of the sum of two ordinals is the natural sum of their birthdays. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → ( bday ‘(𝐴 +s 𝐵)) = (( bday ‘𝐴) +no ( bday ‘𝐵)))
Theorem	peano2ons 28276	The successor of a surreal ordinal is a surreal ordinal. (Contributed by Scott Fenton, 22-Aug-2025.)
⊢ (𝐴 ∈ Ons → (𝐴 +s 1s ) ∈ Ons)
Theorem	onsbnd 28277	The surreals of a given birthday are bounded above by that ordinal. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘( bday ‘𝐴))) → 𝐵 ≤s 𝐴)
Theorem	onsbnd2 28278	The surreals of a given birthday are bounded below by the negative of that ordinal. (Contributed by Scott Fenton, 22-Feb-2026.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘( bday ‘𝐴))) → ( -us ‘𝐴) ≤s 𝐵)
15.6.2  Surreal recursive sequences
Syntax	cseqs 28279	Extend class notation with the surreal recursive sequence builder.
class seqs𝑀( + , 𝐹)
Definition	df-seqs 28280*	Define a general-purpose sequence builder for surreal numbers. Compare df-seq 13925. Note that in the theorems we develop here, we do not require 𝑀 to be an integer. This is because there are infinite surreal numbers and we may want to start our sequence there. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ seqs𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
Theorem	seqsex 28281	Existence of the surreal sequence builder operation. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ seqs𝑀( + , 𝐹) ∈ V
Theorem	seqseq123d 28282	Equality deduction for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑀 = 𝑁)    &   ⊢ (𝜑 → + = 𝑄)    &   ⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) = seqs𝑁(𝑄, 𝐺))
Theorem	nfseqs 28283	Hypothesis builder for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ Ⅎ𝑥𝑀    &   ⊢ Ⅎ𝑥 +    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥seqs𝑀( + , 𝐹)
Theorem	seqsval 28284*	The value of the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 +s 1s ))))𝑦)⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ↾ ω))    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) = ran 𝑅)
Theorem	noseqex 28285	The next several theorems develop the concept of a countable sequence of surreals. This set is denoted by 𝑍 here and is the analogue of the upper integer sets for surreal numbers. However, we do not require the starting point to be an integer so we can accommodate infinite numbers. This first theorem establishes that 𝑍 is a set. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    ⇒   ⊢ (𝜑 → 𝑍 ∈ V)
Theorem	noseq0 28286	The surreal 𝐴 is a member of the sequence starting at 𝐴. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑍)
Theorem	noseqp1 28287*	One plus an element of 𝑍 is an element of 𝑍. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (𝐵 +s 1s ) ∈ 𝑍)
Theorem	noseqind 28288*	Peano's inductive postulate for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 +s 1s ) ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑍 ⊆ 𝐵)
Theorem	noseqinds 28289*	Induction schema for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑦 = (𝑧 +s 1s ) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → (𝜃 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝜂)
Theorem	noseqssno 28290	A surreal sequence is a subset of the surreals. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → 𝑍 ⊆ No )
Theorem	noseqno 28291	An element of a surreal sequence is a surreal. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 ∈ No )
Theorem	om2noseq0 28292	The mapping 𝐺 is a one-to-one mapping from ω onto a countable sequence of surreals that will be used to show the properties of seqs. This theorem shows the value of 𝐺 at ordinal zero. Compare the series of theorems starting at om2uz0i 13870. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    ⇒   ⊢ (𝜑 → (𝐺‘∅) = 𝐶)
Theorem	om2noseqsuc 28293*	The value of 𝐺 at a successor. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝐴 ∈ ω)    ⇒   ⊢ (𝜑 → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) +s 1s ))
Theorem	om2noseqfo 28294	Function statement for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω–onto→𝑍)
Theorem	om2noseqlt 28295*	Surreal less-than relation for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 → (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqlt2 28296*	The mapping 𝐺 preserves order. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 ↔ (𝐺‘𝐴) <s (𝐺‘𝐵)))
Theorem	om2noseqf1o 28297*	𝐺 is a bijection. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺:ω–1-1-onto→𝑍)
Theorem	om2noseqiso 28298*	𝐺 is an isomorphism from the finite ordinals to a surreal sequence. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺 Isom E , <s (ω, 𝑍))
Theorem	om2noseqoi 28299*	An alternative definition of 𝐺 in terms of df-oi 9415. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    ⇒   ⊢ (𝜑 → 𝐺 = OrdIso( <s , 𝑍))
Theorem	om2noseqrdg 28300*	A helper lemma for the value of a recursive definition generator on a surreal sequence with characteristic function 𝐹(𝑥, 𝑦) and initial value 𝐴. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω))    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω))    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ ω) → (𝑅‘𝐵) = ⟨(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))⟩)