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	qrngbas 27601	The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ ℚ = (Base‘𝑄)
Theorem	qdrng 27602	The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 𝑄 ∈ DivRing
Theorem	qrng0 27603	The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 0 = (0g‘𝑄)
Theorem	qrng1 27604	The unity element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 1 = (1r‘𝑄)
Theorem	qrngneg 27605	The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ (𝑋 ∈ ℚ → ((invg‘𝑄)‘𝑋) = -𝑋)
Theorem	qrngdiv 27606	The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ ((𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0) → (𝑋(/r‘𝑄)𝑌) = (𝑋 / 𝑌))
Theorem	qabvle 27607	By using induction on 𝑁, we show a long-range inequality coming from the triangle inequality. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0) → (𝐹‘𝑁) ≤ 𝑁)
Theorem	qabvexp 27608	Induct the product rule abvmul 20787 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁))
Theorem	ostthlem1 27609*	Lemma for ostth 27621. If two absolute values agree on the positive integers greater than one, then they agree for all rational numbers and thus are equal as functions. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘2)) → (𝐹‘𝑛) = (𝐺‘𝑛))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	ostthlem2 27610*	Lemma for ostth 27621. Refine ostthlem1 27609 so that it is sufficient to only show equality on the primes. (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐹‘𝑝) = (𝐺‘𝑝))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	qabsabv 27611	The regular absolute value function on the rationals is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    ⇒   ⊢ (abs ↾ ℚ) ∈ 𝐴
Theorem	padicabv 27612*	The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐹 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹 ∈ 𝐴)
Theorem	padicabvf 27613*	The p-adic absolute value is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    ⇒   ⊢ 𝐽:ℙ⟶𝐴
Theorem	padicabvcxp 27614*	All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+) → (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴)
Theorem	ostth1 27615*	- Lemma for ostth 27621: trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If 𝐹 is equal to 1 on the primes, then by complete induction and the multiplicative property abvmul 20787 of the absolute value, 𝐹 is equal to 1 on all the integers, and ostthlem1 27609 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ ¬ (𝐹‘𝑛) < 1)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐾)
Theorem	ostth2lem2 27616*	Lemma for ostth2 27619. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 1 < (𝐹‘𝑁))    &   ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀))    &   ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ (0...((𝑀↑𝑋) − 1))) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))
Theorem	ostth2lem3 27617*	Lemma for ostth2 27619. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 1 < (𝐹‘𝑁))    &   ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀))    &   ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))    &   ⊢ 𝑈 = ((log‘𝑁) / (log‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝐹‘𝑁) / (𝑇↑𝑐𝑈))↑𝑋) ≤ (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))))
Theorem	ostth2lem4 27618*	Lemma for ostth2 27619. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 1 < (𝐹‘𝑁))    &   ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀))    &   ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))    &   ⊢ 𝑈 = ((log‘𝑁) / (log‘𝑀))    ⇒   ⊢ (𝜑 → (1 < (𝐹‘𝑀) ∧ 𝑅 ≤ 𝑆))
Theorem	ostth2 27619*	- Lemma for ostth 27621: regular case. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 1 < (𝐹‘𝑁))    &   ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (0(,]1)𝐹 = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑎)))
Theorem	ostth3 27620*	- Lemma for ostth 27621: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (𝐹‘𝑃) < 1)    &   ⊢ 𝑅 = -((log‘(𝐹‘𝑃)) / (log‘𝑃))    &   ⊢ 𝑆 = if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎)))
Theorem	ostth 27621*	Ostrowski's theorem, which classifies all absolute values on ℚ. Any such absolute value must either be the trivial absolute value 𝐾, a constant exponent 0 < 𝑎 ≤ 1 times the regular absolute value, or a positive exponent times the p-adic absolute value. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    ⇒   ⊢ (𝐹 ∈ 𝐴 ↔ (𝐹 = 𝐾 ∨ ∃𝑎 ∈ (0(,]1)𝐹 = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑎)) ∨ ∃𝑎 ∈ ℝ+ ∃𝑔 ∈ ran 𝐽 𝐹 = (𝑦 ∈ ℚ ↦ ((𝑔‘𝑦)↑𝑐𝑎))))
PART 15  SURREAL NUMBERS
15.1  Sign sequence representation and Alling's axioms The surreal numbers can be represented in several equivalent ways. In [Alling], Norman Alling made this notion explicit by giving a set of axioms that all representations admit, then proving that there is an order and birthday preserving bijection between any systems that satisfy these axioms. In this section, we start with the definition of surreal numbers given in [Gonshor] and derive Alling's axioms. After deriving them we no longer refer to the explicit definition of surreals. In particular, we never take advantage of the fact that the empty set is a surreal number under our definition.
15.1.1  Definitions and initial properties
Syntax	csur 27622	Declare the class of all surreal numbers (see df-no 27625).
class No
Syntax	clts 27623	Declare the less-than relation over surreal numbers (see df-lts 27626).
class <s
Syntax	cbday 27624	Declare the birthday function for surreal numbers (see df-bday 27627).
class bday
Definition	df-no 27625*	Define the class of surreal numbers. The surreal numbers are a proper class of numbers developed by John H. Conway and introduced by Donald Knuth in 1975. They form a proper class into which all ordered fields can be embedded. The approach we take to defining them was first introduced by Hary Gonshor, and is based on the conception of a "sign expansion" of a surreal number. We define the surreals as ordinal-indexed sequences of 1o and 2o, analogous to Gonshor's ( − ) and ( + ). After introducing this definition, we will abstract away from it using axioms that Norman Alling developed in "Foundations of Analysis over Surreal Number Fields." This is done in an effort to be agnostic towards the exact implementation of surreals. (Contributed by Scott Fenton, 9-Jun-2011.)
⊢ No = {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1o, 2o}}
Definition	df-lts 27626*	Next, we introduce surreal less-than, a comparison relation over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011.)
⊢ <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))}
Definition	df-bday 27627	Finally, we introduce the birthday function. This function maps each surreal to an ordinal. In our implementation, this is the domain of the sign function. The important properties of this function are established later. (Contributed by Scott Fenton, 11-Jun-2011.)
⊢ bday = (𝑥 ∈ No ↦ dom 𝑥)
Theorem	elno 27628*	Membership in the surreals. (Contributed by Scott Fenton, 11-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.) Avoid ax-rep 5212. (Revised by SN, 5-Jun-2025.)
⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
Theorem	elnoOLD 27629*	Obsolete version of elno 27628 as of 5-Jun-2025. (Contributed by Scott Fenton, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
Theorem	ltsval 27630*	The value of the surreal less-than relation. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
Theorem	bdayval 27631	The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ (𝐴 ∈ No → ( bday ‘𝐴) = dom 𝐴)
Theorem	nofun 27632	A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → Fun 𝐴)
Theorem	nodmon 27633	The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)
Theorem	norn 27634	The range of a surreal is a subset of the surreal signs. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → ran 𝐴 ⊆ {1o, 2o})
Theorem	nofnbday 27635	A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → 𝐴 Fn ( bday ‘𝐴))
Theorem	nodmord 27636	The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → Ord dom 𝐴)
Theorem	elno2 27637	An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ (𝐴 ∈ No ↔ (Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ {1o, 2o}))
Theorem	elno3 27638	Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ (𝐴 ∈ No ↔ (𝐴:dom 𝐴⟶{1o, 2o} ∧ dom 𝐴 ∈ On))
Theorem	ltsval2 27639*	Alternate expression for surreal less-than. Two surreals obey surreal less-than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
Theorem	nofv 27640	The function value of a surreal is either a sign or the empty set. (Contributed by Scott Fenton, 22-Jun-2011.)
⊢ (𝐴 ∈ No → ((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = 2o))
Theorem	nosgnn0 27641	∅ is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ ¬ ∅ ∈ {1o, 2o}
Theorem	nosgnn0i 27642	If 𝑋 is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011.)
⊢ 𝑋 ∈ {1o, 2o}    ⇒   ⊢ ∅ ≠ 𝑋
Theorem	noreson 27643	The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ↾ 𝐵) ∈ No )
Theorem	ltsintdifex 27644*	If 𝐴 <s 𝐵, then the intersection of all the ordinals that have differing signs in 𝐴 and 𝐵 exists. (Contributed by Scott Fenton, 22-Feb-2012.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V))
Theorem	ltsres 27645	If the restrictions of two surreals to a given ordinal obey surreal less-than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → 𝐴 <s 𝐵))
Theorem	noxp1o 27646	The Cartesian product of an ordinal and {1o} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.)
⊢ (𝐴 ∈ On → (𝐴 × {1o}) ∈ No )
Theorem	noseponlem 27647*	Lemma for nosepon 27648. Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))
Theorem	nosepon 27648*	Given two unequal surreals, the minimal ordinal at which they differ is an ordinal. (Contributed by Scott Fenton, 21-Sep-2020.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ On)
Theorem	noextend 27649	Extending a surreal by one sign value results in a new surreal. (Contributed by Scott Fenton, 22-Nov-2021.)
⊢ 𝑋 ∈ {1o, 2o}    ⇒   ⊢ (𝐴 ∈ No → (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ No )
Theorem	noextendseq 27650	Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021.)
⊢ 𝑋 ∈ {1o, 2o}    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No )
Theorem	noextenddif 27651*	Calculate the place where a surreal and its extension differ. (Contributed by Scott Fenton, 22-Nov-2021.)
⊢ 𝑋 ∈ {1o, 2o}    ⇒   ⊢ (𝐴 ∈ No → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {⟨dom 𝐴, 𝑋⟩})‘𝑥)} = dom 𝐴)
Theorem	noextendlt 27652	Extending a surreal with a negative sign results in a smaller surreal. (Contributed by Scott Fenton, 22-Nov-2021.)
⊢ (𝐴 ∈ No → (𝐴 ∪ {⟨dom 𝐴, 1o⟩}) <s 𝐴)
Theorem	noextendgt 27653	Extending a surreal with a positive sign results in a bigger surreal. (Contributed by Scott Fenton, 22-Nov-2021.)
⊢ (𝐴 ∈ No → 𝐴 <s (𝐴 ∪ {⟨dom 𝐴, 2o⟩}))
Theorem	nolesgn2o 27654	Given 𝐴 less-than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 2o, then 𝐵(𝑋) = 2o. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐵‘𝑋) = 2o)
Theorem	nolesgn2ores 27655	Given 𝐴 less-than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 2o, then (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋). (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋))
Theorem	nogesgn1o 27656	Given 𝐴 greater than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 1o, then 𝐵(𝑋) = 1o. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ¬ 𝐴 <s 𝐵) → (𝐵‘𝑋) = 1o)
Theorem	nogesgn1ores 27657	Given 𝐴 greater than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 1o, then (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋). (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ¬ 𝐴 <s 𝐵) → (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋))
15.1.2  Ordering
Theorem	ltssolem1 27658	Lemma for ltsso 27659. The "sign expansion" binary relation totally orders the surreal signs. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} Or ({1o, 2o} ∪ {∅})
Theorem	ltsso 27659	Less-than totally orders the surreals. Axiom O of [Alling] p. 184. (Contributed by Scott Fenton, 9-Jun-2011.)
⊢ <s Or No
15.1.3  Birthday Function
Theorem	bdayfo 27660	The birthday function maps the surreals onto the ordinals. Axiom B of [Alling] p. 184. (Proof shortened on 14-Apr-2012 by SF). (Contributed by Scott Fenton, 11-Jun-2011.)
⊢ bday : No –onto→On
15.1.4  Density
Theorem	fvnobday 27661	The value of a surreal at its birthday is ∅. (Contributed by Scott Fenton, 14-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.)
⊢ (𝐴 ∈ No → (𝐴‘( bday ‘𝐴)) = ∅)
Theorem	nosepnelem 27662*	Lemma for nosepne 27663. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))
Theorem	nosepne 27663*	The value of two non-equal surreals at the first place they differ is different. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))
Theorem	nosep1o 27664*	If the value of a surreal at a separator is 1o then the surreal is lesser. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) ∧ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o) → 𝐴 <s 𝐵)
Theorem	nosep2o 27665*	If the value of a surreal at a separator is 2o then the surreal is greater. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) ∧ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) = 2o) → 𝐵 <s 𝐴)
Theorem	nosepdmlem 27666*	Lemma for nosepdm 27667. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ (dom 𝐴 ∪ dom 𝐵))
Theorem	nosepdm 27667*	The first place two surreals differ is an element of the larger of their domains. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ (dom 𝐴 ∪ dom 𝐵))
Theorem	nosepeq 27668*	The values of two surreals at a point less than their separators are equal. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) → (𝐴‘𝑋) = (𝐵‘𝑋))
Theorem	nosepssdm 27669*	Given two non-equal surreals, their separator is less-than or equal to the domain of one of them. Part of Lemma 2.1.1 of [Lipparini] p. 3. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ⊆ dom 𝐴)
Theorem	nodenselem4 27670*	Lemma for nodense 27675. Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
Theorem	nodenselem5 27671*	Lemma for nodense 27675. If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 27670 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday ‘𝐴))
Theorem	nodenselem6 27672*	The restriction of a surreal to the abstraction from nodenselem4 27670 is still a surreal. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No )
Theorem	nodenselem7 27673*	Lemma for nodense 27675. 𝐴 and 𝐵 are equal at all elements of the abstraction. (Contributed by Scott Fenton, 17-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝐶) = (𝐵‘𝐶)))
Theorem	nodenselem8 27674*	Lemma for nodense 27675. Give a condition for surreal less-than when two surreals have the same birthday. (Contributed by Scott Fenton, 19-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( bday ‘𝐴) = ( bday ‘𝐵)) → (𝐴 <s 𝐵 ↔ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o)))
Theorem	nodense 27675*	Given two distinct surreals with the same birthday, there is an older surreal lying between the two of them. Axiom SD of [Alling] p. 184. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∃𝑥 ∈ No (( bday ‘𝑥) ∈ ( bday ‘𝐴) ∧ 𝐴 <s 𝑥 ∧ 𝑥 <s 𝐵))
15.1.5  Full-Eta Property The theorems in this section are derived from "A clean way to separate sets of surreals" by Paolo Lipparini, https://doi.org/10.48550/arXiv.1712.03500.
Theorem	bdayimaon 27676	Lemma for full-eta properties. The successor of the union of the image of the birthday function under a set is an ordinal. (Contributed by Scott Fenton, 20-Aug-2011.)
⊢ (𝐴 ∈ 𝑉 → suc ∪ ( bday “ 𝐴) ∈ On)
Theorem	nolt02olem 27677	Lemma for nolt02o 27678. If 𝐴(𝑋) is undefined with 𝐴 surreal and 𝑋 ordinal, then dom 𝐴 ⊆ 𝑋. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋)
Theorem	nolt02o 27678	Given 𝐴 less-than 𝐵, equal to 𝐵 up to 𝑋, and undefined at 𝑋, then 𝐵(𝑋) = 2o. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴‘𝑋) = ∅) → (𝐵‘𝑋) = 2o)
Theorem	nogt01o 27679	Given 𝐴 greater than 𝐵, equal to 𝐵 up to 𝑋, and 𝐵(𝑋) undefined, then 𝐴(𝑋) = 1o. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵‘𝑋) = ∅) → (𝐴‘𝑋) = 1o)
Theorem	noresle 27680*	Restriction law for surreals. Lemma 2.1.4 of [Lipparini] p. 3. (Contributed by Scott Fenton, 5-Dec-2021.)
⊢ (((𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ (dom 𝑈 ⊆ 𝐴 ∧ dom 𝑆 ⊆ 𝐴 ∧ ∀𝑔 ∈ 𝐴 ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ 𝑆 <s 𝑈)
Theorem	nomaxmo 27681*	A class of surreals has at most one maximum. (Contributed by Scott Fenton, 5-Dec-2021.)
⊢ (𝑆 ⊆ No → ∃*𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ¬ 𝑥 <s 𝑦)
Theorem	nominmo 27682*	A class of surreals has at most one minimum. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑆 ⊆ No → ∃*𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ¬ 𝑦 <s 𝑥)
Theorem	nosupprefixmo 27683*	In any class of surreals, there is at most one value of the prefix property. (Contributed by Scott Fenton, 26-Nov-2021.)
⊢ (𝐴 ⊆ No → ∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
Theorem	noinfprefixmo 27684*	In any class of surreals, there is at most one value of the prefix property. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝐴 ⊆ No → ∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))
Theorem	nosupcbv 27685*	Lemma to change bound variables in a surreal supremum. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ 𝑆 = if(∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏, ((℩𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏) ∪ {⟨dom (℩𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎 <s 𝑏), 2o⟩}), (𝑐 ∈ {𝑑 ∣ ∃𝑒 ∈ 𝐴 (𝑑 ∈ dom 𝑒 ∧ ∀𝑓 ∈ 𝐴 (¬ 𝑓 <s 𝑒 → (𝑒 ↾ suc 𝑑) = (𝑓 ↾ suc 𝑑)))} ↦ (℩𝑎∃𝑒 ∈ 𝐴 (𝑐 ∈ dom 𝑒 ∧ ∀𝑓 ∈ 𝐴 (¬ 𝑓 <s 𝑒 → (𝑒 ↾ suc 𝑐) = (𝑓 ↾ suc 𝑐)) ∧ (𝑒‘𝑐) = 𝑎))))
Theorem	nosupno 27686*	The next several theorems deal with a surreal "supremum". This surreal will ultimately be shown to bound 𝐴 below and bound the restriction of any surreal above. We begin by showing that the given expression actually defines a surreal number. (Contributed by Scott Fenton, 5-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) → 𝑆 ∈ No )
Theorem	nosupdm 27687*	The domain of the surreal supremum when there is no maximum. The primary point of this theorem is to change bound variable. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑧 ∣ ∃𝑝 ∈ 𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
Theorem	nosupbday 27688*	Birthday bounding law for surreal supremum. (Contributed by Scott Fenton, 5-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → ( bday ‘𝑆) ⊆ 𝑂)
Theorem	nosupfv 27689*	The value of surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑆‘𝐺) = (𝑈‘𝐺))
Theorem	nosupres 27690*	A restriction law for surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑆 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
Theorem	nosupbnd1lem1 27691*	Lemma for nosupbnd1 27697. Establish a soft upper bound. (Contributed by Scott Fenton, 5-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))
Theorem	nosupbnd1lem2 27692*	Lemma for nosupbnd1 27697. When there is no maximum, if any member of 𝐴 is a prolongment of 𝑆, then so are all elements of 𝐴 above it. (Contributed by Scott Fenton, 5-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ ((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → (𝑊 ↾ dom 𝑆) = 𝑆)
Theorem	nosupbnd1lem3 27693*	Lemma for nosupbnd1 27697. If 𝑈 is a prolongment of 𝑆 and in 𝐴, then (𝑈‘dom 𝑆) is not 2o. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ 2o)
Theorem	nosupbnd1lem4 27694*	Lemma for nosupbnd1 27697. If 𝑈 is a prolongment of 𝑆 and in 𝐴, then (𝑈‘dom 𝑆) is not undefined. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ ∅)
Theorem	nosupbnd1lem5 27695*	Lemma for nosupbnd1 27697. If 𝑈 is a prolongment of 𝑆 and in 𝐴, then (𝑈‘dom 𝑆) is not 1o. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ 1o)
Theorem	nosupbnd1lem6 27696*	Lemma for nosupbnd1 27697. Establish a hard upper bound when there is no maximum. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
Theorem	nosupbnd1 27697*	Bounding law from below for the surreal supremum. Proposition 4.2 of [Lipparini] p. 6. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
Theorem	nosupbnd2lem1 27698*	Bounding law from above when a set of surreals has a maximum. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {⟨dom 𝑈, 2o⟩}))
Theorem	nosupbnd2 27699*	Bounding law from above for the surreal supremum. Proposition 4.3 of [Lipparini] p. 6. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑍 ∈ No ) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 ↔ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆))
Theorem	noinfcbv 27700*	Change bound variables for surreal infimum. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    ⇒   ⊢ 𝑇 = if(∃𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎, ((℩𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎) ∪ {⟨dom (℩𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ¬ 𝑏 <s 𝑎), 1o⟩}), (𝑐 ∈ {𝑏 ∣ ∃𝑑 ∈ 𝐵 (𝑏 ∈ dom 𝑑 ∧ ∀𝑒 ∈ 𝐵 (¬ 𝑑 <s 𝑒 → (𝑑 ↾ suc 𝑏) = (𝑒 ↾ suc 𝑏)))} ↦ (℩𝑎∃𝑑 ∈ 𝐵 (𝑐 ∈ dom 𝑑 ∧ ∀𝑒 ∈ 𝐵 (¬ 𝑑 <s 𝑒 → (𝑑 ↾ suc 𝑐) = (𝑒 ↾ suc 𝑐)) ∧ (𝑑‘𝑐) = 𝑎))))