Home | Metamath
Proof Explorer Theorem List (p. 340 of 464) | < 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: | Metamath Proof Explorer
(1-29181) |
Hilbert Space Explorer
(29182-30704) |
Users' Mathboxes
(30705-46395) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | noprc 33901 | The surreal numbers are a proper class. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ ¬ No ∈ V | ||
Syntax | csslt 33902 | Declare the syntax for surreal set less than. |
class <<s | ||
Definition | df-sslt 33903* | 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 33904 | Declare the syntax for the surreal cut operator. |
class |s | ||
Definition | df-scut 33905* | 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 33906* | A version of noeta 33873 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 33907* | 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 33908 | The first argument of surreal set less than exists. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) | ||
Theorem | ssltex2 33909 | The second argument of surreal set less than exists. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) | ||
Theorem | ssltss1 33910 | The first argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No ) | ||
Theorem | ssltss2 33911 | The second argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No ) | ||
Theorem | ssltsep 33912* | The separation property of surreal set less than. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) | ||
Theorem | ssltd 33913* | Deduce surreal set less than. (Contributed by Scott Fenton, 24-Sep-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ No ) & ⊢ (𝜑 → 𝐵 ⊆ No ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦) ⇒ ⊢ (𝜑 → 𝐴 <<s 𝐵) | ||
Theorem | ssltsepc 33914 | Two elements of separated sets obey less than. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 <s 𝑌) | ||
Theorem | ssltsepcd 33915 | Two elements of separated sets obey less than. Deduction form of ssltsepc 33914. (Contributed by Scott Fenton, 25-Sep-2024.) |
⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 <s 𝑌) | ||
Theorem | sssslt1 33916 | Relationship between surreal set less than and subset. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴) → 𝐶 <<s 𝐵) | ||
Theorem | sssslt2 33917 | Relationship between surreal set less than and subset. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐴 <<s 𝐶) | ||
Theorem | nulsslt 33918 | The empty set is less than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ (𝐴 ∈ 𝒫 No → ∅ <<s 𝐴) | ||
Theorem | nulssgt 33919 | The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ (𝐴 ∈ 𝒫 No → 𝐴 <<s ∅) | ||
Theorem | conway 33920* | 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 33921* | 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 33922 | Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) | ||
Theorem | scutcl 33923 | Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.) |
⊢ (𝐴 <<s 𝐵 → (𝐴 |s 𝐵) ∈ No ) | ||
Theorem | scutcld 33924 | Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024.) |
⊢ (𝜑 → 𝐴 <<s 𝐵) ⇒ ⊢ (𝜑 → (𝐴 |s 𝐵) ∈ No ) | ||
Theorem | scutbday 33925* | 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 33926* | 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 33927* | 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 33928 | Transitive law for surreal set less than. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅) → 𝐴 <<s 𝐶) | ||
Theorem | ssltun1 33929 | Union law for surreal set less than. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → (𝐴 ∪ 𝐵) <<s 𝐶) | ||
Theorem | ssltun2 33930 | Union law for surreal set less than. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s (𝐵 ∪ 𝐶)) | ||
Theorem | scutun12 33931 | Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 ∪ 𝐶) |s (𝐵 ∪ 𝐷)) = (𝐴 |s 𝐵)) | ||
Theorem | dmscut 33932 | The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ dom |s = <<s | ||
Theorem | scutf 33933 | Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.) |
⊢ |s : <<s ⟶ No | ||
Theorem | etasslt 33934* | A restatement of noeta 33873 using set less than. (Contributed by Scott Fenton, 10-Aug-2024.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ 𝑂)) | ||
Theorem | etasslt2 33935* | A version of etasslt 33934 with fewer hypotheses but a weaker upper bound. (Contributed by Scott Fenton, 10-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) | ||
Theorem | scutbdaybnd 33936 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Aug-2024.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ (𝐴 ∪ 𝐵)) ⊆ 𝑂) → ( bday ‘(𝐴 |s 𝐵)) ⊆ 𝑂) | ||
Theorem | scutbdaybnd2 33937 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) | ||
Theorem | scutbdaybnd2lim 33938 | 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 33939 | 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 33940* | 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 33941* | 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 33942 | If 𝐴 preceeds 𝐵, then 𝐴 and 𝐵 are disjoint. (Contributed by Scott Fenton, 18-Sep-2024.) |
⊢ (𝐴 <<s 𝐵 → (𝐴 ∩ 𝐵) = ∅) | ||
Syntax | c0s 33943 | Declare the class syntax for surreal zero. |
class 0s | ||
Syntax | c1s 33944 | Declare the class syntax for surreal one. |
class 1s | ||
Definition | df-0s 33945 | 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 33946 | 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 33947 | Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ 0s ∈ No | ||
Theorem | 1sno 33948 | Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ 1s ∈ No | ||
Theorem | bday0s 33949 | Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ ( bday ‘ 0s ) = ∅ | ||
Theorem | 0slt1s 33950 | Surreal zero is less than surreal one. Theorem from [Conway] p. 7. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ 0s <s 1s | ||
Theorem | bday0b 33951 | The only surreal with birthday ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ (𝑋 ∈ No → (( bday ‘𝑋) = ∅ ↔ 𝑋 = 0s )) | ||
Theorem | bday1s 33952 | The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ ( bday ‘ 1s ) = 1o | ||
Syntax | cmade 33953 | Declare the symbol for the made by function. |
class M | ||
Syntax | cold 33954 | Declare the symbol for the older than function. |
class O | ||
Syntax | cnew 33955 | Declare the symbol for the new on function. |
class N | ||
Syntax | cleft 33956 | Declare the symbol for the left option function. |
class L | ||
Syntax | cright 33957 | Declare the symbol for the right option function. |
class R | ||
Definition | df-made 33958 | 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 33959 | 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 33960 | 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 33961* | 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 33962* | 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 33963 | The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)))) | ||
Theorem | madeval2 33964* | Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)}) | ||
Theorem | oldval 33965 | The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ (𝐴 ∈ On → ( O ‘𝐴) = ∪ ( M “ 𝐴)) | ||
Theorem | newval 33966 | The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( N ‘𝐴) = (( M ‘𝐴) ∖ ( O ‘𝐴)) | ||
Theorem | madef 33967 | The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ M :On⟶𝒫 No | ||
Theorem | oldf 33968 | The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ O :On⟶𝒫 No | ||
Theorem | newf 33969 | The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ N :On⟶𝒫 No | ||
Theorem | old0 33970 | No surreal is older than ∅. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ ( O ‘∅) = ∅ | ||
Theorem | madessno 33971 | Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( M ‘𝐴) ⊆ No | ||
Theorem | oldssno 33972 | Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( O ‘𝐴) ⊆ No | ||
Theorem | newssno 33973 | New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( N ‘𝐴) ⊆ No | ||
Theorem | leftval 33974* | The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( L ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} | ||
Theorem | rightval 33975* | The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( R ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥} | ||
Theorem | leftf 33976 | The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ L : No ⟶𝒫 No | ||
Theorem | rightf 33977 | The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ R : No ⟶𝒫 No | ||
Theorem | elmade 33978* | Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋))) | ||
Theorem | elmade2 33979* | 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 33980* | Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ (𝐴 ∈ On → (𝑋 ∈ ( O ‘𝐴) ↔ ∃𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘𝑏))) | ||
Theorem | ssltleft 33981 | 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 33982 | 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 33983 | The left options of a surreal are strictly less than the right options of the same surreal. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ (𝐴 ∈ No → ( L ‘𝐴) <<s ( R ‘𝐴)) | ||
Theorem | made0 33984 | The only surreal made on day ∅ is 0s. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ ( M ‘∅) = { 0s } | ||
Theorem | new0 33985 | The only surreal new on day ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ ( N ‘∅) = { 0s } | ||
Theorem | madess 33986 | 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 33987 | The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( O ‘𝐴) ⊆ ( M ‘𝐴) | ||
Theorem | leftssold 33988 | The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)) | ||
Theorem | rightssold 33989 | The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)) | ||
Theorem | leftssno 33990 | The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( L ‘𝐴) ⊆ No | ||
Theorem | rightssno 33991 | The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( R ‘𝐴) ⊆ No | ||
Theorem | madecut 33992 | 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 33993 | 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 33994 | The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( O ‘suc 𝐴)) | ||
Theorem | oldsuc 33995 | The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ (𝐴 ∈ On → ( O ‘suc 𝐴) = (( O ‘𝐴) ∪ ( N ‘𝐴))) | ||
Theorem | oldlim 33996 | The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → ( O ‘𝐴) = ∪ ( O “ 𝐴)) | ||
Theorem | madebdayim 33997 | 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 33998 | 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 33999 | No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.) |
⊢ ¬ 𝑋 ∈ ( O ‘( bday ‘𝑋)) | ||
Theorem | leftirr 34000 | No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ¬ 𝑋 ∈ ( L ‘𝑋) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |