| Metamath
Proof Explorer Theorem List (p. 279 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | sltletr 27801 | Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 <s 𝐵 ∧ 𝐵 ≤s 𝐶) → 𝐴 <s 𝐶)) | ||
| Theorem | slelttr 27802 | Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 ≤s 𝐵 ∧ 𝐵 <s 𝐶) → 𝐴 <s 𝐶)) | ||
| Theorem | sletr 27803 | Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐶) → 𝐴 ≤s 𝐶)) | ||
| Theorem | slttrd 27804 | Surreal less-than is transitive. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 𝐵) & ⊢ (𝜑 → 𝐵 <s 𝐶) ⇒ ⊢ (𝜑 → 𝐴 <s 𝐶) | ||
| Theorem | sltletrd 27805 | Surreal less-than is transitive. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 𝐵) & ⊢ (𝜑 → 𝐵 ≤s 𝐶) ⇒ ⊢ (𝜑 → 𝐴 <s 𝐶) | ||
| Theorem | slelttrd 27806 | Surreal less-than is transitive. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐴 ≤s 𝐵) & ⊢ (𝜑 → 𝐵 <s 𝐶) ⇒ ⊢ (𝜑 → 𝐴 <s 𝐶) | ||
| Theorem | sletrd 27807 | Surreal less-than or equal is transitive. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐴 ≤s 𝐵) & ⊢ (𝜑 → 𝐵 ≤s 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤s 𝐶) | ||
| Theorem | slerflex 27808 | Surreal less-than or equal is reflexive. Theorem 0(iii) of [Conway] p. 16. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ (𝐴 ∈ No → 𝐴 ≤s 𝐴) | ||
| Theorem | sletric 27809 | Surreal trichotomy law. (Contributed by Scott Fenton, 14-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ∨ 𝐵 ≤s 𝐴)) | ||
| Theorem | maxs1 27810 | A surreal is less than or equal to the maximum of it and another. (Contributed by Scott Fenton, 14-Feb-2025.) |
| ⊢ (𝐴 ∈ No → 𝐴 ≤s if(𝐴 ≤s 𝐵, 𝐵, 𝐴)) | ||
| Theorem | maxs2 27811 | A surreal is less than or equal to the maximum of it and another. (Contributed by Scott Fenton, 14-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐵 ≤s if(𝐴 ≤s 𝐵, 𝐵, 𝐴)) | ||
| Theorem | mins1 27812 | The minimum of two surreals is less than or equal to the first. (Contributed by Scott Fenton, 14-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → if(𝐴 ≤s 𝐵, 𝐴, 𝐵) ≤s 𝐴) | ||
| Theorem | mins2 27813 | The minimum of two surreals is less than or equal to the second. (Contributed by Scott Fenton, 14-Feb-2025.) |
| ⊢ (𝐵 ∈ No → if(𝐴 ≤s 𝐵, 𝐴, 𝐵) ≤s 𝐵) | ||
| Theorem | sltled 27814 | Surreal less-than implies less-than or equal. (Contributed by Scott Fenton, 16-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤s 𝐵) | ||
| Theorem | sltne 27815 | Surreal less-than implies not equal. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐴 <s 𝐵) → 𝐵 ≠ 𝐴) | ||
| Theorem | sltlend 27816 | Surreal less-than in terms of less-than or equal. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 ≤s 𝐵 ∧ 𝐵 ≠ 𝐴))) | ||
| Theorem | bdayfun 27817 | The birthday function is a function. (Contributed by Scott Fenton, 14-Jun-2011.) |
| ⊢ Fun bday | ||
| Theorem | bdayfn 27818 | The birthday function is a function over No . (Contributed by Scott Fenton, 30-Jun-2011.) |
| ⊢ bday Fn No | ||
| Theorem | bdaydm 27819 | The birthday function's domain is No . (Contributed by Scott Fenton, 14-Jun-2011.) |
| ⊢ dom bday = No | ||
| Theorem | bdayrn 27820 | The birthday function's range is On. (Contributed by Scott Fenton, 14-Jun-2011.) |
| ⊢ ran bday = On | ||
| Theorem | bdayelon 27821 | 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 27822* | Lemma for nocvxmin 27823. 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 27823* | Given a nonempty convex class of surreals, there is a unique birthday-minimal element of that class. Lemma 0 of [Alling] p. 185. (Contributed by Scott Fenton, 30-Jun-2011.) |
| ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ∃!𝑤 ∈ 𝐴 ( bday ‘𝑤) = ∩ ( bday “ 𝐴)) | ||
| Theorem | noprc 27824 | The surreal numbers are a proper class. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ ¬ No ∈ V | ||
In [Conway] surreal numbers are represented as equivalence classes of cuts of previously defined surreal numbers. This is complicated to handle in ZFC without classes so we do not make it our definition. However, we can define a cut operator on surreals that behaves similarly. We introduce such an operator in this section and use it to define all surreals hearafter. | ||
| Syntax | csslt 27825 | Declare the syntax for surreal set less-than. |
| class <<s | ||
| Definition | df-sslt 27826* | Define the relation that holds iff one set of surreals completely precedes another. (Contributed by Scott Fenton, 7-Dec-2021.) |
| ⊢ <<s = {〈𝑎, 𝑏〉 ∣ (𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)} | ||
| Syntax | cscut 27827 | Declare the syntax for the surreal cut operator. |
| class |s | ||
| Definition | df-scut 27828* | 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. Definition from [Gonshor] p. 7. (Contributed by Scott Fenton, 7-Dec-2021.) |
| ⊢ |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) | ||
| Theorem | noeta2 27829* | A version of noeta 27788 with fewer hypotheses but a weaker upper bound (Contributed by Scott Fenton, 7-Dec-2021.) |
| ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → ∃𝑧 ∈ No (∀𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday ‘𝑧) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) | ||
| Theorem | brsslt 27830* | 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 27831 | The first argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) | ||
| Theorem | ssltex2 27832 | The second argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) | ||
| Theorem | ssltss1 27833 | The first argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No ) | ||
| Theorem | ssltss2 27834 | The second argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No ) | ||
| Theorem | ssltsep 27835* | The separation property of surreal set less-than. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) | ||
| Theorem | ssltd 27836* | Deduce surreal set less-than. (Contributed by Scott Fenton, 24-Sep-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ No ) & ⊢ (𝜑 → 𝐵 ⊆ No ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦) ⇒ ⊢ (𝜑 → 𝐴 <<s 𝐵) | ||
| Theorem | ssltsn 27837 | Surreal set less-than of two singletons. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 𝐵) ⇒ ⊢ (𝜑 → {𝐴} <<s {𝐵}) | ||
| Theorem | ssltsepc 27838 | Two elements of separated sets obey less-than. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 <s 𝑌) | ||
| Theorem | ssltsepcd 27839 | Two elements of separated sets obey less-than. Deduction form of ssltsepc 27838. (Contributed by Scott Fenton, 25-Sep-2024.) |
| ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 <s 𝑌) | ||
| Theorem | sssslt1 27840 | Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴) → 𝐶 <<s 𝐵) | ||
| Theorem | sssslt2 27841 | Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐴 <<s 𝐶) | ||
| Theorem | nulsslt 27842 | The empty set is less-than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 ∈ 𝒫 No → ∅ <<s 𝐴) | ||
| Theorem | nulssgt 27843 | The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅) | ||
| Theorem | conway 27844* | 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. Theorem from [Alling] p. 185. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → ∃!𝑥 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) | ||
| Theorem | scutval 27845* | The value of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) = (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))) | ||
| Theorem | scutcut 27846 | Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) | ||
| Theorem | scutcl 27847 | Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.) |
| ⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) ∈ No ) | ||
| Theorem | scutcld 27848 | Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 <<s 𝐵) ⇒ ⊢ (𝜑 → (𝐴 |s 𝐵) ∈ No ) | ||
| Theorem | scutbday 27849* | The birthday of the surreal cut is equal to the minimum birthday in the gap. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑥 ∈ No ∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)})) | ||
| Theorem | eqscut 27850* | Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024.) |
| ⊢ ((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday ‘𝑋) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})))) | ||
| Theorem | eqscut2 27851* | Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024.) |
| ⊢ ((𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ∀𝑦 ∈ No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday ‘𝑋) ⊆ ( bday ‘𝑦))))) | ||
| Theorem | sslttr 27852 | Transitive law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅) → 𝐴 <<s 𝐶) | ||
| Theorem | ssltun1 27853 | Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
| ⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → (𝐴 ∪ 𝐵) <<s 𝐶) | ||
| Theorem | ssltun2 27854 | Union law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s (𝐵 ∪ 𝐶)) | ||
| Theorem | scutun12 27855 | Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 ∪ 𝐶) |s (𝐵 ∪ 𝐷)) = (𝐴 |s 𝐵)) | ||
| Theorem | dmscut 27856 | The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ dom |s = <<s | ||
| Theorem | scutf 27857 | Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.) |
| ⊢ |s : <<s ⟶ No | ||
| Theorem | etasslt 27858* | A restatement of noeta 27788 using set less-than. (Contributed by Scott Fenton, 10-Aug-2024.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ 𝑂)) | ||
| Theorem | etasslt2 27859* | A version of etasslt 27858 with fewer hypotheses but a weaker upper bound. (Contributed by Scott Fenton, 10-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) | ||
| Theorem | scutbdaybnd 27860 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Aug-2024.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ( bday ‘(𝐴 |s 𝐵)) ⊆ 𝑂) | ||
| Theorem | scutbdaybnd2 27861 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.) |
| ⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) | ||
| Theorem | scutbdaybnd2lim 27862 | An upper bound on the birthday of a surreal cut when it is a limit birthday. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday ‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ∪ ( bday “ (𝐴 ∪ 𝐵))) | ||
| Theorem | scutbdaylt 27863 | If a surreal lies in a gap and is not equal to the cut, its birthday is greater than the cut's. (Contributed by Scott Fenton, 11-Dec-2021.) |
| ⊢ ((𝑋 ∈ No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday ‘𝑋)) | ||
| Theorem | slerec 27864* | A comparison law for surreals considered as cuts of sets of surreals. Definition from [Conway] p. 4. Theorem 4 of [Alling] p. 186. Theorem 2.5 of [Gonshor] p. 9. (Contributed by Scott Fenton, 11-Dec-2021.) |
| ⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷) ∧ (𝑋 = (𝐴 |s 𝐵) ∧ 𝑌 = (𝐶 |s 𝐷))) → (𝑋 ≤s 𝑌 ↔ (∀𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑌))) | ||
| Theorem | sltrec 27865* | A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 11-Dec-2021.) |
| ⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷) ∧ (𝑋 = (𝐴 |s 𝐵) ∧ 𝑌 = (𝐶 |s 𝐷))) → (𝑋 <s 𝑌 ↔ (∃𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃𝑏 ∈ 𝐵 𝑏 ≤s 𝑌))) | ||
| Theorem | ssltdisj 27866 | If 𝐴 preceeds 𝐵, then 𝐴 and 𝐵 are disjoint. (Contributed by Scott Fenton, 18-Sep-2024.) |
| ⊢ (𝐴 <<s 𝐵 → (𝐴 ∩ 𝐵) = ∅) | ||
| Syntax | c0s 27867 | Declare the class syntax for surreal zero. |
| class 0s | ||
| Syntax | c1s 27868 | Declare the class syntax for surreal one. |
| class 1s | ||
| Definition | df-0s 27869 | Define surreal zero. This is the simplest cut of surreal number sets. Definition from [Conway] p. 17. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ 0s = (∅ |s ∅) | ||
| Definition | df-1s 27870 | Define surreal one. This is the simplest number greater than surreal zero. Definition from [Conway] p. 18. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ 1s = ({ 0s } |s ∅) | ||
| Theorem | 0sno 27871 | Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ 0s ∈ No | ||
| Theorem | 1sno 27872 | Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ 1s ∈ No | ||
| Theorem | bday0s 27873 | Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ ( bday ‘ 0s ) = ∅ | ||
| Theorem | 0slt1s 27874 | Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ 0s <s 1s | ||
| Theorem | bday0b 27875 | The only surreal with birthday ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.) |
| ⊢ (𝑋 ∈ No → (( bday ‘𝑋) = ∅ ↔ 𝑋 = 0s )) | ||
| Theorem | bday1s 27876 | The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.) |
| ⊢ ( bday ‘ 1s ) = 1o | ||
| Theorem | cuteq0 27877 | Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 <<s { 0s }) & ⊢ (𝜑 → { 0s } <<s 𝐵) ⇒ ⊢ (𝜑 → (𝐴 |s 𝐵) = 0s ) | ||
| Theorem | cuteq1 27878 | Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ (𝜑 → 0s ∈ 𝐴) & ⊢ (𝜑 → 𝐴 <<s { 1s }) & ⊢ (𝜑 → { 1s } <<s 𝐵) ⇒ ⊢ (𝜑 → (𝐴 |s 𝐵) = 1s ) | ||
| Theorem | sgt0ne0 27879 | A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ ( 0s <s 𝐴 → 𝐴 ≠ 0s ) | ||
| Theorem | sgt0ne0d 27880 | A positive surreal is not equal to zero. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ (𝜑 → 0s <s 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0s ) | ||
| Syntax | cmade 27881 | Declare the symbol for the made by function. |
| class M | ||
| Syntax | cold 27882 | Declare the symbol for the older than function. |
| class O | ||
| Syntax | cnew 27883 | Declare the symbol for the new on function. |
| class N | ||
| Syntax | cleft 27884 | Declare the symbol for the left option function. |
| class L | ||
| Syntax | cright 27885 | Declare the symbol for the right option function. |
| class R | ||
| Definition | df-made 27886 | Define the made by function. This function carries an ordinal to all surreals made by sections of surreals older than it. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.) |
| ⊢ M = recs((𝑓 ∈ V ↦ ( |s “ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓)))) | ||
| Definition | df-old 27887 | Define the older than function. This function carries an ordinal to all surreals made by a previous ordinal. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.) |
| ⊢ O = (𝑥 ∈ On ↦ ∪ ( M “ 𝑥)) | ||
| Definition | df-new 27888 | Define the newer than function. This function carries an ordinal to all surreals made on that day. Definition from [Conway] p. 29. (Contributed by Scott Fenton, 17-Dec-2021.) |
| ⊢ N = (𝑥 ∈ On ↦ (( M ‘𝑥) ∖ ( O ‘𝑥))) | ||
| Definition | df-left 27889* | Define the left options of a surreal. This is the set of surreals that are simpler and less than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024.) |
| ⊢ L = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑦 <s 𝑥}) | ||
| Definition | df-right 27890* | Define the right options of a surreal. This is the set of surreals that are simpler and greater than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024.) |
| ⊢ R = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑥 <s 𝑦}) | ||
| Theorem | madeval 27891 | The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
| ⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)))) | ||
| Theorem | madeval2 27892* | Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
| ⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)}) | ||
| Theorem | oldval 27893 | The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
| ⊢ (𝐴 ∈ On → ( O ‘𝐴) = ∪ ( M “ 𝐴)) | ||
| Theorem | newval 27894 | The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( N ‘𝐴) = (( M ‘𝐴) ∖ ( O ‘𝐴)) | ||
| Theorem | madef 27895 | The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
| ⊢ M :On⟶𝒫 No | ||
| Theorem | oldf 27896 | The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
| ⊢ O :On⟶𝒫 No | ||
| Theorem | newf 27897 | The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
| ⊢ N :On⟶𝒫 No | ||
| Theorem | old0 27898 | No surreal is older than ∅. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ ( O ‘∅) = ∅ | ||
| Theorem | madessno 27899 | Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( M ‘𝐴) ⊆ No | ||
| Theorem | oldssno 27900 | Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( O ‘𝐴) ⊆ No | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |