P. 325 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32401-32500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nosgnn0i 32401	If 𝑋 is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011.)
⊢ 𝑋 ∈ {1o, 2o}    ⇒   ⊢ ∅ ≠ 𝑋
Theorem	noreson 32402	The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ↾ 𝐵) ∈ No )
Theorem	sltintdifex 32403*	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	sltres 32404	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 32405	The Cartesian product of an ordinal and {1o} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.)
⊢ (𝐴 ∈ On → (𝐴 × {1o}) ∈ No )
Theorem	noseponlem 32406*	Lemma for nosepon 32407. Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))
Theorem	nosepon 32407*	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 32408	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 32409	Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021.)
⊢ 𝑋 ∈ {1o, 2o}    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No )
Theorem	noextenddif 32410*	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 32411	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 32412	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 32413	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 32414	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 𝑋))
20.8.22  Surreal Numbers: Ordering
Theorem	sltsolem1 32415	Lemma for sltso 32416. The sign expansion relationship totally orders the surreal signs. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} Or ({1o, 2o} ∪ {∅})
Theorem	sltso 32416	Surreal less than totally orders the surreals. Alling's axiom (O). (Contributed by Scott Fenton, 9-Jun-2011.)
⊢ <s Or No
20.8.23  Surreal Numbers: Birthday Function
Theorem	bdayfo 32417	The birthday function maps the surreals onto the ordinals. Alling's axiom (B). (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011.)
⊢ bday : No –onto→On
20.8.24  Surreal Numbers: Density
Theorem	fvnobday 32418	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 32419*	Lemma for nosepne 32420. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))
Theorem	nosepne 32420*	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 32421*	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	nosepdmlem 32422*	Lemma for nosepdm 32423. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ (dom 𝐴 ∪ dom 𝐵))
Theorem	nosepdm 32423*	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 32424*	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 32425*	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 32426*	Lemma for nodense 32431. Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
Theorem	nodenselem5 32427*	Lemma for nodense 32431. If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 32426 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday ‘𝐴))
Theorem	nodenselem6 32428*	The restriction of a surreal to the abstraction from nodenselem4 32426 is still a surreal. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No )
Theorem	nodenselem7 32429*	Lemma for nodense 32431. 𝐴 and 𝐵 are equal at all elements of the abstraction. (Contributed by Scott Fenton, 17-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝐶) = (𝐵‘𝐶)))
Theorem	nodenselem8 32430*	Lemma for nodense 32431. 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 32431*	Given two distinct surreals with the same birthday, there is an older surreal lying between the two of them. Alling's axiom (SD). (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∃𝑥 ∈ No (( bday ‘𝑥) ∈ ( bday ‘𝐴) ∧ 𝐴 <s 𝑥 ∧ 𝑥 <s 𝐵))
20.8.25  Surreal Numbers: Full-Eta Property
Theorem	bdayimaon 32432	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 32433	Lemma for nolt02o 32434. If 𝐴(𝑋) is undefined with 𝐴 surreal and 𝑋 ordinal, then dom 𝐴 ⊆ 𝑋. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋)
Theorem	nolt02o 32434	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	noresle 32435*	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 32436*	A class of surreals has at most one maximum. (Contributed by Scott Fenton, 5-Dec-2021.)
⊢ (𝑆 ⊆ No → ∃*𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ¬ 𝑥 <s 𝑦)
Theorem	noprefixmo 32437*	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	nosupno 32438*	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 32439*	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 32440*	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) → ( bday ‘𝑆) ⊆ suc ∪ ( bday “ 𝐴))
Theorem	nosupfv 32441*	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 32442*	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 32443*	Lemma for nosupbnd1 32449. 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 32444*	Lemma for nosupbnd1 32449. 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 32445*	Lemma for nosupbnd1 32449. 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 32446*	Lemma for nosupbnd1 32449. 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 32447*	Lemma for nosupbnd1 32449. 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 32448*	Lemma for nosupbnd1 32449. 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 32449*	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 32450*	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 32451*	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	noetalem1 32452*	Lemma for noeta 32457. Establish that our final surreal really is a surreal. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    &   ⊢ 𝑍 = (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))    ⇒   ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 ∈ No )
Theorem	noetalem2 32453*	Lemma for noeta 32457. 𝑍 is an upper bound for 𝐴. Part of Theorem 5.1 of [Lipparini] p. 7-8. (Contributed by Scott Fenton, 4-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    &   ⊢ 𝑍 = (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))    ⇒   ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑋 ∈ 𝐴) → 𝑋 <s 𝑍)
Theorem	noetalem3 32454*	Lemma for noeta 32457. When 𝐴 and 𝐵 are separated, then 𝑍 is a lower bound for 𝐵. Part of Theorem 5.1 of [Lipparini] p. 7-8. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    &   ⊢ 𝑍 = (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))    ⇒   ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)
Theorem	noetalem4 32455*	Lemma for noeta 32457. Bound the birthday of 𝑍 above. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    &   ⊢ 𝑍 = (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))    ⇒   ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → ( bday ‘𝑍) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))
Theorem	noetalem5 32456*	Lemma for noeta 32457. The full statement of the theorem with hypotheses. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))    &   ⊢ 𝑍 = (𝑆 ∪ ((suc ∪ ( bday “ 𝐵) ∖ dom 𝑆) × {1o}))    ⇒   ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∃𝑧 ∈ No (∀𝑎 ∈ 𝐴 𝑎 <s 𝑧 ∧ ∀𝑏 ∈ 𝐵 𝑧 <s 𝑏 ∧ ( bday ‘𝑧) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))))
Theorem	noeta 32457*	The full-eta axiom for the surreal numbers. This is the single most important property of the surreals. It says that, given two sets of surreals such that one comes completely before the other, there is a surreal lying strictly between the two. Furthermore, there is an upper bound on the birthday of that surreal. Alling's axiom FE. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → ∃𝑧 ∈ No (∀𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘𝑧) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))))
20.8.26  Surreal numbers - ordering theorems
Syntax	csle 32458	Declare the syntax for surreal less than or equal.
class ≤s
Definition	df-sle 32459	Define the surreal less than or equal predicate. Compare df-le 10417. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ≤s = (( No × No ) ∖ ◡ <s )
Theorem	sltirr 32460	Surreal less than is irreflexive. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → ¬ 𝐴 <s 𝐴)
Theorem	slttr 32461	Surreal less than is transitive. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 <s 𝐵 ∧ 𝐵 <s 𝐶) → 𝐴 <s 𝐶))
Theorem	sltasym 32462	Surreal less than is asymmetric. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ¬ 𝐵 <s 𝐴))
Theorem	sltlin 32463	Surreal less than obeys trichotomy. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <s 𝐴))
Theorem	slttrieq2 32464	Trichotomy law for surreal less than. (Contributed by Scott Fenton, 22-Apr-2012.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 <s 𝐵 ∧ ¬ 𝐵 <s 𝐴)))
Theorem	slttrine 32465	Trichotomy law for surreals. (Contributed by Scott Fenton, 23-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≠ 𝐵 ↔ (𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴)))
Theorem	slenlt 32466	Surreal less than or equal in terms of less than. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
Theorem	sltnle 32467	Surreal less than in terms of less than or equal. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ¬ 𝐵 ≤s 𝐴))
Theorem	sleloe 32468	Surreal less than or equal in terms of less than. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 <s 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	sletri3 32469	Trichotomy law for surreal less than or equal. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 = 𝐵 ↔ (𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐴)))
Theorem	sltletr 32470	Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 <s 𝐵 ∧ 𝐵 ≤s 𝐶) → 𝐴 <s 𝐶))
Theorem	slelttr 32471	Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 ≤s 𝐵 ∧ 𝐵 <s 𝐶) → 𝐴 <s 𝐶))
Theorem	sletr 32472	Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐶) → 𝐴 ≤s 𝐶))
Theorem	slttrd 32473	Surreal less than is transitive. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → 𝐵 <s 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 <s 𝐶)
Theorem	sltletrd 32474	Surreal less than is transitive. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐴 <s 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤s 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 <s 𝐶)
Theorem	slelttrd 32475	Surreal less than is transitive. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≤s 𝐵)    &   ⊢ (𝜑 → 𝐵 <s 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 <s 𝐶)
Theorem	sletrd 32476	Surreal less than or equal is transitive. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ No )    &   ⊢ (𝜑 → 𝐵 ∈ No )    &   ⊢ (𝜑 → 𝐶 ∈ No )    &   ⊢ (𝜑 → 𝐴 ≤s 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤s 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≤s 𝐶)
20.8.27  Surreal numbers - birthday theorems
Theorem	bdayfun 32477	The birthday function is a function. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ Fun bday
Theorem	bdayfn 32478	The birthday function is a function over No . (Contributed by Scott Fenton, 30-Jun-2011.)
⊢ bday Fn No
Theorem	bdaydm 32479	The birthday function's domain is No . (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ dom bday = No
Theorem	bdayrn 32480	The birthday function's range is On. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ ran bday = On
Theorem	bdayelon 32481	The value of the birthday function is always an ordinal. (Contributed by Scott Fenton, 14-Jun-2011.) (Proof shortened by Scott Fenton, 8-Dec-2021.)
⊢ ( bday ‘𝐴) ∈ On
Theorem	nocvxminlem 32482*	Lemma for nocvxmin 32483. Given two birthday-minimal elements of a convex class of surreals, they are not comparable. (Contributed by Scott Fenton, 30-Jun-2011.)
⊢ ((𝐴 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday ‘𝑌) = ∩ ( bday “ 𝐴))) → ¬ 𝑋 <s 𝑌))
Theorem	nocvxmin 32483*	Given a nonempty convex class of surreals, there is a unique birthday-minimal element of that class. (Contributed by Scott Fenton, 30-Jun-2011.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ∃!𝑤 ∈ 𝐴 ( bday ‘𝑤) = ∩ ( bday “ 𝐴))
Theorem	noprc 32484	The surreal numbers are a proper class. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ ¬ No ∈ V
20.8.28  Surreal numbers: Conway cuts
Syntax	csslt 32485	Declare the syntax for surreal set less than.
class <<s
Definition	df-sslt 32486*	Define the relationship that holds iff one set of surreals completely precedes another. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ <<s = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)}
Syntax	cscut 32487	Declare the syntax for the surreal cut operator.
class |s
Definition	df-scut 32488*	Define the cut operator on surreal numbers. This operator, which Conway takes as the primitive operator over surreals, picks the surreal lying between two sets of surreals of minimal birthday. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
Theorem	brsslt 32489*	Binary relation form of the surreal set less-than relation. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)))
Theorem	ssltex1 32490	The first argument of surreal set less than exists. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
Theorem	ssltex2 32491	The second argument of surreal set less than exists. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
Theorem	ssltss1 32492	The first argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
Theorem	ssltss2 32493	The second argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
Theorem	ssltsep 32494*	The separation property of surreal set less than. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
Theorem	sssslt1 32495	Relationship between surreal set less than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴) → 𝐶 <<s 𝐵)
Theorem	sssslt2 32496	Relationship between surreal set less than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐴 <<s 𝐶)
Theorem	nulsslt 32497	The empty set is less than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 ∈ 𝒫 No → ∅ <<s 𝐴)
Theorem	nulssgt 32498	The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅)
Theorem	conway 32499*	Conway's Simplicity Theorem. Given 𝐴 preceeding 𝐵, there is a unique surreal of minimal length separating them. This is a fundamental property of surreals and will be used (via surreal cuts) to prove many properties later on. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → ∃!𝑥 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
Theorem	scutval 32500*	The value of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) = (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})))