P. 277 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27601-27700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elmade2 27601*	Membership in the made function in terms of the old function. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ( O ‘𝐴)∃𝑟 ∈ 𝒫 ( O ‘𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋)))
Theorem	elold 27602*	Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ On → (𝑋 ∈ ( O ‘𝐴) ↔ ∃𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘𝑏)))
Theorem	ssltleft 27603	A surreal is greater than its left options. Theorem 0(ii) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ No → ( L ‘𝐴) <<s {𝐴})
Theorem	ssltright 27604	A surreal is less than its right options. Theorem 0(i) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (𝐴 ∈ No → {𝐴} <<s ( R ‘𝐴))
Theorem	lltropt 27605	The left options of a surreal are strictly less than the right options of the same surreal. (Contributed by Scott Fenton, 6-Aug-2024.) (Revised by Scott Fenton, 21-Feb-2025.)
⊢ ( L ‘𝐴) <<s ( R ‘𝐴)
Theorem	made0 27606	The only surreal made on day ∅ is 0s. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ ( M ‘∅) = { 0s }
Theorem	new0 27607	The only surreal new on day ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ( N ‘∅) = { 0s }
Theorem	old1 27608	The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( O ‘1o) = { 0s }
Theorem	madess 27609	If 𝐴 is less than or equal to ordinal 𝐵, then the made set of 𝐴 is included in the made set of 𝐵. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ((𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵) → ( M ‘𝐴) ⊆ ( M ‘𝐵))
Theorem	oldssmade 27610	The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( O ‘𝐴) ⊆ ( M ‘𝐴)
Theorem	leftssold 27611	The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
Theorem	rightssold 27612	The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
Theorem	leftssno 27613	The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( L ‘𝐴) ⊆ No
Theorem	rightssno 27614	The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( R ‘𝐴) ⊆ No
Theorem	madecut 27615	Given a section that is a subset of an old set, the cut is a member of the made set. (Contributed by Scott Fenton, 7-Aug-2024.)
⊢ (((𝐴 ∈ On ∧ 𝐿 <<s 𝑅) ∧ (𝐿 ⊆ ( O ‘𝐴) ∧ 𝑅 ⊆ ( O ‘𝐴))) → (𝐿 |s 𝑅) ∈ ( M ‘𝐴))
Theorem	madeun 27616	The made set is the union of the old set and the new set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ( M ‘𝐴) = (( O ‘𝐴) ∪ ( N ‘𝐴))
Theorem	madeoldsuc 27617	The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( O ‘suc 𝐴))
Theorem	oldsuc 27618	The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ∈ On → ( O ‘suc 𝐴) = (( O ‘𝐴) ∪ ( N ‘𝐴)))
Theorem	oldlim 27619	The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → ( O ‘𝐴) = ∪ ( O “ 𝐴))
Theorem	madebdayim 27620	If a surreal is a member of a made set, its birthday is less than or equal to the level. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ (𝑋 ∈ ( M ‘𝐴) → ( bday ‘𝑋) ⊆ 𝐴)
Theorem	oldbdayim 27621	If 𝑋 is in the old set for 𝐴, then the birthday of 𝑋 is less than 𝐴. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ (𝑋 ∈ ( O ‘𝐴) → ( bday ‘𝑋) ∈ 𝐴)
Theorem	oldirr 27622	No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.)
⊢ ¬ 𝑋 ∈ ( O ‘( bday ‘𝑋))
Theorem	leftirr 27623	No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ¬ 𝑋 ∈ ( L ‘𝑋)
Theorem	rightirr 27624	No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ ¬ 𝑋 ∈ ( R ‘𝑋)
Theorem	left0s 27625	The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( L ‘ 0s ) = ∅
Theorem	right0s 27626	The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ( R ‘ 0s ) = ∅
Theorem	left1s 27627	The left set of 1s is the singleton of 0s. (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( L ‘ 1s ) = { 0s }
Theorem	right1s 27628	The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025.)
⊢ ( R ‘ 1s ) = ∅
Theorem	lrold 27629	The union of the left and right options of a surreal make its old set. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday ‘𝐴))
Theorem	madebdaylemold 27630*	Lemma for madebday 27632. If the inductive hypothesis of madebday 27632 is satisfied, the converse of oldbdayim 27621 holds. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ ∀𝑏 ∈ 𝐴 ∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( bday ‘𝑋) ∈ 𝐴 → 𝑋 ∈ ( O ‘𝐴)))
Theorem	madebdaylemlrcut 27631*	Lemma for madebday 27632. If the inductive hypothesis of madebday 27632 is satisfied up to the birthday of 𝑋, then the conclusion of lrcut 27635 holds. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((∀𝑏 ∈ ( bday ‘𝑋)∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋)
Theorem	madebday 27632	A surreal is part of the set made by ordinal 𝐴 iff its birthday is less than or equal to 𝐴. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No ) → (𝑋 ∈ ( M ‘𝐴) ↔ ( bday ‘𝑋) ⊆ 𝐴))
Theorem	oldbday 27633	A surreal is part of the set older than ordinal 𝐴 iff its birthday is less than 𝐴. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No ) → (𝑋 ∈ ( O ‘𝐴) ↔ ( bday ‘𝑋) ∈ 𝐴))
Theorem	newbday 27634	A surreal is an element of a new set iff its birthday is equal to that ordinal. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No ) → (𝑋 ∈ ( N ‘𝐴) ↔ ( bday ‘𝑋) = 𝐴))
Theorem	lrcut 27635	A surreal is equal to the cut of its left and right sets. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ (𝑋 ∈ No → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋)
Theorem	scutfo 27636	The surreal cut function is onto. (Contributed by Scott Fenton, 23-Aug-2024.)
⊢ |s : <<s –onto→ No
Theorem	sltn0 27637	If 𝑋 is less than 𝑌, then either ( L ‘𝑌) or ( R ‘𝑋) is non-empty. (Contributed by Scott Fenton, 10-Dec-2024.)
⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑋 <s 𝑌) → (( L ‘𝑌) ≠ ∅ ∨ ( R ‘𝑋) ≠ ∅))
Theorem	lruneq 27638	If two surreals share a birthday, then the union of their left and right sets are equal. (Contributed by Scott Fenton, 17-Sep-2024.)
⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (( L ‘𝑋) ∪ ( R ‘𝑋)) = (( L ‘𝑌) ∪ ( R ‘𝑌)))
Theorem	sltlpss 27639	If two surreals share a birthday, then 𝑋 <s 𝑌 iff the left set of 𝑋 is a proper subset of the left set of 𝑌. (Contributed by Scott Fenton, 17-Sep-2024.)
⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 ↔ ( L ‘𝑋) ⊊ ( L ‘𝑌)))
Theorem	slelss 27640	If two surreals 𝐴 and 𝐵 share a birthday, then 𝐴 ≤s 𝐵 if and only if the left set of 𝐴 is a non-strict subset of the left set of 𝐵. (Contributed by Scott Fenton, 21-Mar-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( bday ‘𝐴) = ( bday ‘𝐵)) → (𝐴 ≤s 𝐵 ↔ ( L ‘𝐴) ⊆ ( L ‘𝐵)))
Theorem	0elold 27641	Zero is in the old set of any non-zero number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≠ 0s )    ⇒   ⊢ (𝜑 → 0s ∈ ( O ‘( bday ‘𝐴)))
Theorem	0elleft 27642	Zero is in the left set of any positive number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 0s ∈ ( L ‘𝐴))
Theorem	0elright 27643	Zero is in the right set of any negative number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 0s )    ⇒   ⊢ (𝜑 → 0s ∈ ( R ‘𝐴))
15.3.4  Cofinality and coinitiality
Theorem	cofsslt 27644*	If every element of 𝐴 is bounded above by some element of 𝐵 and 𝐵 precedes 𝐶, then 𝐴 precedes 𝐶. Note - we will often use the term "cofinal" to denote that every element of 𝐴 is bounded above by some element of 𝐵. Similarly, we will use the term "coinitial" to denote that every element of 𝐴 is bounded below by some element of 𝐵. (Contributed by Scott Fenton, 24-Sep-2024.)
⊢ ((𝐴 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶) → 𝐴 <<s 𝐶)
Theorem	coinitsslt 27645*	If 𝐵 is coinitial with 𝐶 and 𝐴 precedes 𝐶, then 𝐴 precedes 𝐵. (Contributed by Scott Fenton, 24-Sep-2024.)
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s 𝐵)
Theorem	cofcut1 27646*	If 𝐶 is cofinal with 𝐴 and 𝐷 is coinitial with 𝐵 and the cut of 𝐴 and 𝐵 lies between 𝐶 and 𝐷, then the cut of 𝐶 and 𝐷 is equal to the cut of 𝐴 and 𝐵. Theorem 2.6 of [Gonshor] p. 10. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))
Theorem	cofcut1d 27647*	If 𝐶 is cofinal with 𝐴 and 𝐷 is coinitial with 𝐵 and the cut of 𝐴 and 𝐵 lies between 𝐶 and 𝐷, then the cut of 𝐶 and 𝐷 is equal to the cut of 𝐴 and 𝐵. Theorem 2.6 of [Gonshor] p. 10. (Contributed by Scott Fenton, 23-Jan-2025.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧)    &   ⊢ (𝜑 → 𝐶 <<s {(𝐴 |s 𝐵)})    &   ⊢ (𝜑 → {(𝐴 |s 𝐵)} <<s 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))
Theorem	cofcut2 27648*	If 𝐴 and 𝐶 are mutually cofinal and 𝐵 and 𝐷 are mutually coinitial, then the cut of 𝐴 and 𝐵 is equal to the cut of 𝐶 and 𝐷. Theorem 2.7 of [Gonshor] p. 10. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (∀𝑡 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀𝑟 ∈ 𝐷 ∃𝑠 ∈ 𝐵 𝑠 ≤s 𝑟)) → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))
Theorem	cofcut2d 27649*	If 𝐴 and 𝐶 are mutually cofinal and 𝐵 and 𝐷 are mutually coinitial, then the cut of 𝐴 and 𝐵 is equal to the cut of 𝐶 and 𝐷. Theorem 2.7 of [Gonshor] p. 10. (Contributed by Scott Fenton, 23-Jan-2025.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝒫 No )    &   ⊢ (𝜑 → 𝐷 ∈ 𝒫 No )    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧)    &   ⊢ (𝜑 → ∀𝑡 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑡 ≤s 𝑢)    &   ⊢ (𝜑 → ∀𝑟 ∈ 𝐷 ∃𝑠 ∈ 𝐵 𝑠 ≤s 𝑟)    ⇒   ⊢ (𝜑 → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))
Theorem	cofcutr 27650*	If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐴 is cofinal with ( L ‘𝑋) and 𝐵 is coinitial with ( R ‘𝑋). Theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧))
Theorem	cofcutr1d 27651*	If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐴 is cofinal with ( L ‘𝑋). First half of theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 23-Jan-2025.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
Theorem	cofcutr2d 27652*	If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐵 is coinitial with ( R ‘𝑋). Second half of theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
Theorem	cofcutrtime 27653*	If 𝑋 is the cut of 𝐴 and 𝐵 and all of 𝐴 and 𝐵 are older than 𝑋, then ( L ‘𝑋) is cofinal with 𝐴 and ( R ‘𝑋) is coinitial with 𝐵. Note: we will call a cut where all of the elements of the cut are older than the cut itself a "timely" cut. Part of Theorem 4.02(12) of [Alling] p. 125. (Contributed by Scott Fenton, 27-Sep-2024.)
⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧))
Theorem	cofcutrtime1d 27654*	If 𝑋 is a timely cut of 𝐴 and 𝐵, then ( L ‘𝑋) is cofinal with 𝐴. (Contributed by Scott Fenton, 23-Jan-2025.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)))    &   ⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦)
Theorem	cofcutrtime2d 27655*	If 𝑋 is a timely cut of 𝐴 and 𝐵, then ( R ‘𝑋) is coinitial with 𝐵. (Contributed by Scott Fenton, 23-Jan-2025.)
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)))    &   ⊢ (𝜑 → 𝐴 <<s 𝐵)    &   ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧)
Theorem	cofss 27656*	Cofinality for a subset. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ⊆ No )    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
Theorem	coiniss 27657*	Coinitiality for a subset. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ⊆ No )    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑦 ≤s 𝑥)
Theorem	cutlt 27658*	Eliminating all elements below a given element of a cut does not affect the cut. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐿 <<s 𝑅)    &   ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐿)    ⇒   ⊢ (𝜑 → 𝐴 = (({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) |s 𝑅))
Theorem	cutpos 27659*	Reduce the elements of a cut for a positive number. (Contributed by Scott Fenton, 13-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 0s <s 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = (({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) |s ( R ‘𝐴)))
15.4  Induction and recursion
15.4.1  Induction and recursion on one variable
Syntax	cnorec 27660	Declare the syntax for surreal recursion of one variable.
class norec (𝐹)
Definition	df-norec 27661*	Define the recursion generator for surreal functions of one variable. This generator creates a recursive function of surreals from their value on their left and right sets. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ norec (𝐹) = frecs({⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝐹)
Theorem	lrrecval 27662*	The next step in the development of the surreals is to establish induction and recursion across left and right sets. To that end, we are going to develop a relationship 𝑅 that is founded, partial, and set-like across the surreals. This first theorem just establishes the value of 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝑅𝐵 ↔ 𝐴 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))))
Theorem	lrrecval2 27663*	Next, we establish an alternate expression for 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝑅𝐵 ↔ ( bday ‘𝐴) ∈ ( bday ‘𝐵)))
Theorem	lrrecpo 27664*	Now, we establish that 𝑅 is a partial ordering on No . (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ 𝑅 Po No
Theorem	lrrecse 27665*	Next, we show that 𝑅 is set-like over No . (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ 𝑅 Se No
Theorem	lrrecfr 27666*	Now we show that 𝑅 is founded over No . (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ 𝑅 Fr No
Theorem	lrrecpred 27667*	Finally, we calculate the value of the predecessor class over 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}    ⇒   ⊢ (𝐴 ∈ No → Pred(𝑅, No , 𝐴) = (( L ‘𝐴) ∪ ( R ‘𝐴)))
Theorem	noinds 27668*	Induction principle for a single surreal. If a property passes from a surreal's left and right sets to the surreal itself, then it holds for all surreals. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ No → (∀𝑦 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 → 𝜑))    ⇒   ⊢ (𝐴 ∈ No → 𝜒)
Theorem	norecfn 27669	Surreal recursion over one variable is a function over the surreals. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝐹 = norec (𝐺)    ⇒   ⊢ 𝐹 Fn No
Theorem	norecov 27670	Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝐹 = norec (𝐺)    ⇒   ⊢ (𝐴 ∈ No → (𝐹‘𝐴) = (𝐴𝐺(𝐹 ↾ (( L ‘𝐴) ∪ ( R ‘𝐴)))))
15.4.2  Induction and recursion on two variables
Syntax	cnorec2 27671	Declare the syntax for surreal recursion on two arguments.
class norec2 (𝐹)
Definition	df-norec2 27672*	Define surreal recursion on two variables. This function is key to the development of most of surreal numbers. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ norec2 (𝐹) = frecs({⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1st ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){⟨𝑐, 𝑑⟩ ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No × No ), 𝐹)
Theorem	noxpordpo 27673*	To get through most of the textbook defintions in surreal numbers we will need recursion on two variables. This set of theorems sets up the preconditions for double recursion. This theorem establishes the partial ordering. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑅(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    ⇒   ⊢ 𝑆 Po ( No × No )
Theorem	noxpordfr 27674*	Next we establish the foundedness of the relationship. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑅(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    ⇒   ⊢ 𝑆 Fr ( No × No )
Theorem	noxpordse 27675*	Next we establish the set-like nature of the relationship. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑅(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    ⇒   ⊢ 𝑆 Se ( No × No )
Theorem	noxpordpred 27676*	Next we calculate the predecessor class of the relationship. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑅 = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑅(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → Pred(𝑆, ( No × No ), ⟨𝐴, 𝐵⟩) = ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩}))
Theorem	no2indslem 27677*	Double induction on surreals with explicit notation for the relationships. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ 𝑅 = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑧 → (𝜃 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑦 = 𝐵 → (𝜏 ↔ 𝜂))    &   ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → ((∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜒 ∧ ∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 ∧ ∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜃) → 𝜑))    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂)
Theorem	no2inds 27678*	Double induction on surreals. The many substitution instances are to cover all possible cases. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑧 → (𝜃 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑦 = 𝐵 → (𝜏 ↔ 𝜂))    &   ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → ((∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜒 ∧ ∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 ∧ ∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜃) → 𝜑))    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂)
Theorem	norec2fn 27679	The double-recursion operator on surreals yields a function on pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ 𝐹 = norec2 (𝐺)    ⇒   ⊢ 𝐹 Fn ( No × No )
Theorem	norec2ov 27680	The value of the double-recursion surreal function. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ 𝐹 = norec2 (𝐺)    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝐹𝐵) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {⟨𝐴, 𝐵⟩}))))
Theorem	no3inds 27681*	Triple induction over surreal numbers. (Contributed by Scott Fenton, 9-Oct-2024.)
⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃))    &   ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃))    &   ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏))    &   ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌))    &   ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇))    &   ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆))    &   ⊢ ((𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → (((∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃 ∧ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜒 ∧ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜁) ∧ (∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))𝜓 ∧ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜏 ∧ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜎) ∧ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜂) → 𝜑))    ⇒   ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑍 ∈ No ) → 𝜆)
15.5  Surreal arithmetic
15.5.1  Addition
Syntax	cadds 27682	Declare the syntax for surreal addition.
class +s
Definition	df-adds 27683*	Define surreal addition. This is the first of the field operations on the surreals. Definition from [Conway] p. 5. Definition from [Gonshor] p. 13. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ +s = norec2 ((𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st ‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)}))))
Theorem	addsfn 27684	Surreal addition is a function over pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ +s Fn ( No × No )
Theorem	addsval 27685*	The value of surreal addition. Definition from [Conway] p. 5. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s 𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑦 = (𝑟 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑧 = (𝐴 +s 𝑟)})))
Theorem	addsval2 27686*	The value of surreal addition with different choices for each bound variable. Definition from [Conway] p. 5. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝐵)𝑡 = (𝐴 +s 𝑠)})))
Theorem	addsrid 27687	Surreal addition to zero is identity. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ (𝐴 ∈ No → (𝐴 +s 0s ) = 𝐴)
Theorem	addsridd 27688	Surreal addition to zero is identity. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 +s 0s ) = 𝐴)
Theorem	addscom 27689	Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (𝐵 +s 𝐴))
Theorem	addscomd 27690	Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    ⇒   ⊢ (𝜑 → (𝐴 +s 𝐵) = (𝐵 +s 𝐴))
Theorem	addslid 27691	Surreal addition to zero is identity. (Contributed by Scott Fenton, 3-Feb-2025.)
⊢ (𝐴 ∈ No → ( 0s +s 𝐴) = 𝐴)
Theorem	addsproplem1 27692*	Lemma for surreal addition properties. To prove closure on surreal addition we need to prove that addition is compatible with order at the same time. We do this by inducting over the maximum of two natural sums of the birthdays of surreals numbers. In the final step we will loop around and use tfr3 8403 to prove this of all surreals. This first lemma just instantiates the inductive hypothesis so we do not need to do it continuously throughout the proof. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (( bday ‘𝐴) +no ( bday ‘𝐶))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))    ⇒   ⊢ (𝜑 → ((𝐴 +s 𝐵) ∈ No ∧ (𝐵 <s 𝐶 → (𝐵 +s 𝐴) <s (𝐶 +s 𝐴))))
Theorem	addsproplem2 27693*	Lemma for surreal addition properties. When proving closure for operations defined using norec and norec2, it is a strictly stronger statement to say that the cut defined is actually a cut than it is to say that the operation is closed. We will often prove this stronger statement. Here, we do so for the cut involved in surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))    &   ⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    ⇒   ⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
Theorem	addsproplem3 27694*	Lemma for surreal addition properties. Show the cut properties of surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))    &   ⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    ⇒   ⊢ (𝜑 → ((𝑋 +s 𝑌) ∈ No ∧ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s {(𝑋 +s 𝑌)} ∧ {(𝑋 +s 𝑌)} <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})))
Theorem	addsproplem4 27695*	Lemma for surreal addition properties. Show the second half of the inductive hypothesis when 𝑌 is older than 𝑍. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))    &   ⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    &   ⊢ (𝜑 → 𝑍 ∈ No )    &   ⊢ (𝜑 → 𝑌 <s 𝑍)    &   ⊢ (𝜑 → ( bday ‘𝑌) ∈ ( bday ‘𝑍))    ⇒   ⊢ (𝜑 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))
Theorem	addsproplem5 27696*	Lemma for surreal addition properties. Show the second half of the inductive hypothesis when 𝑍 is older than 𝑌. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))    &   ⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    &   ⊢ (𝜑 → 𝑍 ∈ No )    &   ⊢ (𝜑 → 𝑌 <s 𝑍)    &   ⊢ (𝜑 → ( bday ‘𝑍) ∈ ( bday ‘𝑌))    ⇒   ⊢ (𝜑 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))
Theorem	addsproplem6 27697*	Lemma for surreal addition properties. Finally, we show the second half of the induction hypothesis when 𝑌 and 𝑍 are the same age. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))    &   ⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    &   ⊢ (𝜑 → 𝑍 ∈ No )    &   ⊢ (𝜑 → 𝑌 <s 𝑍)    &   ⊢ (𝜑 → ( bday ‘𝑌) = ( bday ‘𝑍))    ⇒   ⊢ (𝜑 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))
Theorem	addsproplem7 27698*	Lemma for surreal addition properties. Putting together the three previous lemmas, we now show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))    &   ⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    &   ⊢ (𝜑 → 𝑍 ∈ No )    &   ⊢ (𝜑 → 𝑌 <s 𝑍)    ⇒   ⊢ (𝜑 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))
Theorem	addsprop 27699	Inductively show that surreal addition is closed and compatible with less-than. This proof follows from induction on the birthdays of the surreal numbers involved. This pattern occurs throughout surreal development. Theorem 3.1 of [Gonshor] p. 14. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑍 ∈ No ) → ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))))
Theorem	addscutlem 27700*	Lemma for addscut 27701. Show the statement with some additional distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025.)
⊢ (𝜑 → 𝑋 ∈ No )    &   ⊢ (𝜑 → 𝑌 ∈ No )    ⇒   ⊢ (𝜑 → ((𝑋 +s 𝑌) ∈ No ∧ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s {(𝑋 +s 𝑌)} ∧ {(𝑋 +s 𝑌)} <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})))