| Metamath
Proof Explorer Theorem List (p. 280 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 | newssno 27901 | New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( N ‘𝐴) ⊆ No | ||
| Theorem | leftval 27902* | The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( L ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} | ||
| Theorem | rightval 27903* | The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( R ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥} | ||
| Theorem | leftf 27904 | The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
| ⊢ L : No ⟶𝒫 No | ||
| Theorem | rightf 27905 | The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
| ⊢ R : No ⟶𝒫 No | ||
| Theorem | elmade 27906* | Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.) |
| ⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋))) | ||
| Theorem | elmade2 27907* | 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 27908* | Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ (𝐴 ∈ On → (𝑋 ∈ ( O ‘𝐴) ↔ ∃𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘𝑏))) | ||
| Theorem | ssltleft 27909 | 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 27910 | 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 27911 | The left options of a surreal are strictly less than the right options of the same surreal. (Contributed by Scott Fenton, 6-Aug-2024.) (Revised by Scott Fenton, 21-Feb-2025.) |
| ⊢ ( L ‘𝐴) <<s ( R ‘𝐴) | ||
| Theorem | made0 27912 | The only surreal made on day ∅ is 0s. (Contributed by Scott Fenton, 7-Aug-2024.) |
| ⊢ ( M ‘∅) = { 0s } | ||
| Theorem | new0 27913 | The only surreal new on day ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.) |
| ⊢ ( N ‘∅) = { 0s } | ||
| Theorem | old1 27914 | The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.) |
| ⊢ ( O ‘1o) = { 0s } | ||
| Theorem | madess 27915 | 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 27916 | The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( O ‘𝐴) ⊆ ( M ‘𝐴) | ||
| Theorem | leftssold 27917 | The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)) | ||
| Theorem | rightssold 27918 | The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)) | ||
| Theorem | leftssno 27919 | The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( L ‘𝐴) ⊆ No | ||
| Theorem | rightssno 27920 | The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ( R ‘𝐴) ⊆ No | ||
| Theorem | madecut 27921 | 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 27922 | 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 27923 | The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
| ⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( O ‘suc 𝐴)) | ||
| Theorem | oldsuc 27924 | The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
| ⊢ (𝐴 ∈ On → ( O ‘suc 𝐴) = (( O ‘𝐴) ∪ ( N ‘𝐴))) | ||
| Theorem | oldlim 27925 | The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.) |
| ⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → ( O ‘𝐴) = ∪ ( O “ 𝐴)) | ||
| Theorem | madebdayim 27926 | 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 27927 | 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 27928 | No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.) |
| ⊢ ¬ 𝑋 ∈ ( O ‘( bday ‘𝑋)) | ||
| Theorem | leftirr 27929 | No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ¬ 𝑋 ∈ ( L ‘𝑋) | ||
| Theorem | rightirr 27930 | No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ ¬ 𝑋 ∈ ( R ‘𝑋) | ||
| Theorem | left0s 27931 | The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ ( L ‘ 0s ) = ∅ | ||
| Theorem | right0s 27932 | The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ ( R ‘ 0s ) = ∅ | ||
| Theorem | left1s 27933 | The left set of 1s is the singleton of 0s. (Contributed by Scott Fenton, 4-Feb-2025.) |
| ⊢ ( L ‘ 1s ) = { 0s } | ||
| Theorem | right1s 27934 | The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025.) |
| ⊢ ( R ‘ 1s ) = ∅ | ||
| Theorem | lrold 27935 | The union of the left and right options of a surreal make its old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday ‘𝐴)) | ||
| Theorem | madebdaylemold 27936* | Lemma for madebday 27938. If the inductive hypothesis of madebday 27938 is satisfied, the converse of oldbdayim 27927 holds. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ ∀𝑏 ∈ 𝐴 ∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( bday ‘𝑋) ∈ 𝐴 → 𝑋 ∈ ( O ‘𝐴))) | ||
| Theorem | madebdaylemlrcut 27937* | Lemma for madebday 27938. If the inductive hypothesis of madebday 27938 is satisfied up to the birthday of 𝑋, then the conclusion of lrcut 27941 holds. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ ((∀𝑏 ∈ ( bday ‘𝑋)∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋) | ||
| Theorem | madebday 27938 | A surreal is part of the set made by ordinal 𝐴 iff its birthday is less than or equal to 𝐴. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No ) → (𝑋 ∈ ( M ‘𝐴) ↔ ( bday ‘𝑋) ⊆ 𝐴)) | ||
| Theorem | oldbday 27939 | A surreal is part of the set older than ordinal 𝐴 iff its birthday is less than 𝐴. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No ) → (𝑋 ∈ ( O ‘𝐴) ↔ ( bday ‘𝑋) ∈ 𝐴)) | ||
| Theorem | newbday 27940 | A surreal is an element of a new set iff its birthday is equal to that ordinal. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No ) → (𝑋 ∈ ( N ‘𝐴) ↔ ( bday ‘𝑋) = 𝐴)) | ||
| Theorem | lrcut 27941 | A surreal is equal to the cut of its left and right sets. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ (𝑋 ∈ No → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋) | ||
| Theorem | scutfo 27942 | The surreal cut function is onto. (Contributed by Scott Fenton, 23-Aug-2024.) |
| ⊢ |s : <<s –onto→ No | ||
| Theorem | sltn0 27943 | If 𝑋 is less than 𝑌, then either ( L ‘𝑌) or ( R ‘𝑋) is non-empty. (Contributed by Scott Fenton, 10-Dec-2024.) |
| ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑋 <s 𝑌) → (( L ‘𝑌) ≠ ∅ ∨ ( R ‘𝑋) ≠ ∅)) | ||
| Theorem | lruneq 27944 | If two surreals share a birthday, then the union of their left and right sets are equal. (Contributed by Scott Fenton, 17-Sep-2024.) |
| ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (( L ‘𝑋) ∪ ( R ‘𝑋)) = (( L ‘𝑌) ∪ ( R ‘𝑌))) | ||
| Theorem | sltlpss 27945 | If two surreals share a birthday, then 𝑋 <s 𝑌 iff the left set of 𝑋 is a proper subset of the left set of 𝑌. (Contributed by Scott Fenton, 17-Sep-2024.) |
| ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 ↔ ( L ‘𝑋) ⊊ ( L ‘𝑌))) | ||
| Theorem | slelss 27946 | If two surreals 𝐴 and 𝐵 share a birthday, then 𝐴 ≤s 𝐵 if and only if the left set of 𝐴 is a non-strict subset of the left set of 𝐵. (Contributed by Scott Fenton, 21-Mar-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( bday ‘𝐴) = ( bday ‘𝐵)) → (𝐴 ≤s 𝐵 ↔ ( L ‘𝐴) ⊆ ( L ‘𝐵))) | ||
| Theorem | 0elold 27947 | Zero is in the old set of any non-zero number. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐴 ≠ 0s ) ⇒ ⊢ (𝜑 → 0s ∈ ( O ‘( bday ‘𝐴))) | ||
| Theorem | 0elleft 27948 | Zero is in the left set of any positive number. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐴) ⇒ ⊢ (𝜑 → 0s ∈ ( L ‘𝐴)) | ||
| Theorem | 0elright 27949 | Zero is in the right set of any negative number. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 0s ) ⇒ ⊢ (𝜑 → 0s ∈ ( R ‘𝐴)) | ||
| Theorem | madefi 27950 | The made set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.) |
| ⊢ (𝐴 ∈ ω → ( M ‘𝐴) ∈ Fin) | ||
| Theorem | oldfi 27951 | The old set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.) |
| ⊢ (𝐴 ∈ ω → ( O ‘𝐴) ∈ Fin) | ||
| Theorem | cofsslt 27952* | If every element of 𝐴 is bounded above by some element of 𝐵 and 𝐵 precedes 𝐶, then 𝐴 precedes 𝐶. Note - we will often use the term "cofinal" to denote that every element of 𝐴 is bounded above by some element of 𝐵. Similarly, we will use the term "coinitial" to denote that every element of 𝐴 is bounded below by some element of 𝐵. (Contributed by Scott Fenton, 24-Sep-2024.) |
| ⊢ ((𝐴 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ≤s 𝑦 ∧ 𝐵 <<s 𝐶) → 𝐴 <<s 𝐶) | ||
| Theorem | coinitsslt 27953* | If 𝐵 is coinitial with 𝐶 and 𝐴 precedes 𝐶, then 𝐴 precedes 𝐵. (Contributed by Scott Fenton, 24-Sep-2024.) |
| ⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s 𝐵) | ||
| Theorem | cofcut1 27954* | If 𝐶 is cofinal with 𝐴 and 𝐷 is coinitial with 𝐵 and the cut of 𝐴 and 𝐵 lies between 𝐶 and 𝐷, then the cut of 𝐶 and 𝐷 is equal to the cut of 𝐴 and 𝐵. Theorem 2.6 of [Gonshor] p. 10. (Contributed by Scott Fenton, 25-Sep-2024.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) = (𝐶 |s 𝐷)) | ||
| Theorem | cofcut1d 27955* | If 𝐶 is cofinal with 𝐴 and 𝐷 is coinitial with 𝐵 and the cut of 𝐴 and 𝐵 lies between 𝐶 and 𝐷, then the cut of 𝐶 and 𝐷 is equal to the cut of 𝐴 and 𝐵. Theorem 2.6 of [Gonshor] p. 10. (Contributed by Scott Fenton, 23-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) & ⊢ (𝜑 → 𝐶 <<s {(𝐴 |s 𝐵)}) & ⊢ (𝜑 → {(𝐴 |s 𝐵)} <<s 𝐷) ⇒ ⊢ (𝜑 → (𝐴 |s 𝐵) = (𝐶 |s 𝐷)) | ||
| Theorem | cofcut2 27956* | If 𝐴 and 𝐶 are mutually cofinal and 𝐵 and 𝐷 are mutually coinitial, then the cut of 𝐴 and 𝐵 is equal to the cut of 𝐶 and 𝐷. Theorem 2.7 of [Gonshor] p. 10. (Contributed by Scott Fenton, 25-Sep-2024.) |
| ⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (∀𝑡 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀𝑟 ∈ 𝐷 ∃𝑠 ∈ 𝐵 𝑠 ≤s 𝑟)) → (𝐴 |s 𝐵) = (𝐶 |s 𝐷)) | ||
| Theorem | cofcut2d 27957* | If 𝐴 and 𝐶 are mutually cofinal and 𝐵 and 𝐷 are mutually coinitial, then the cut of 𝐴 and 𝐵 is equal to the cut of 𝐶 and 𝐷. Theorem 2.7 of [Gonshor] p. 10. (Contributed by Scott Fenton, 23-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝒫 No ) & ⊢ (𝜑 → 𝐷 ∈ 𝒫 No ) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) & ⊢ (𝜑 → ∀𝑡 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑡 ≤s 𝑢) & ⊢ (𝜑 → ∀𝑟 ∈ 𝐷 ∃𝑠 ∈ 𝐵 𝑠 ≤s 𝑟) ⇒ ⊢ (𝜑 → (𝐴 |s 𝐵) = (𝐶 |s 𝐷)) | ||
| Theorem | cofcutr 27958* | If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐴 is cofinal with ( L ‘𝑋) and 𝐵 is coinitial with ( R ‘𝑋). Theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 25-Sep-2024.) |
| ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)) | ||
| Theorem | cofcutr1d 27959* | If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐴 is cofinal with ( L ‘𝑋). First half of theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 23-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦) | ||
| Theorem | cofcutr2d 27960* | If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐵 is coinitial with ( R ‘𝑋). Second half of theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 25-Sep-2024.) |
| ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧) | ||
| Theorem | cofcutrtime 27961* | If 𝑋 is the cut of 𝐴 and 𝐵 and all of 𝐴 and 𝐵 are older than 𝑋, then ( L ‘𝑋) is cofinal with 𝐴 and ( R ‘𝑋) is coinitial with 𝐵. Note: we will call a cut where all of the elements of the cut are older than the cut itself a "timely" cut. Part of Theorem 4.02(12) of [Alling] p. 125. (Contributed by Scott Fenton, 27-Sep-2024.) |
| ⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧)) | ||
| Theorem | cofcutrtime1d 27962* | If 𝑋 is a timely cut of 𝐴 and 𝐵, then ( L ‘𝑋) is cofinal with 𝐴. (Contributed by Scott Fenton, 23-Jan-2025.) |
| ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋))) & ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦) | ||
| Theorem | cofcutrtime2d 27963* | If 𝑋 is a timely cut of 𝐴 and 𝐵, then ( R ‘𝑋) is coinitial with 𝐵. (Contributed by Scott Fenton, 23-Jan-2025.) |
| ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋))) & ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧) | ||
| Theorem | cofss 27964* | Cofinality for a subset. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ⊆ No ) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦) | ||
| Theorem | coiniss 27965* | Coinitiality for a subset. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ⊆ No ) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑦 ≤s 𝑥) | ||
| Theorem | cutlt 27966* | Eliminating all elements below a given element of a cut does not affect the cut. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ (𝜑 → 𝐿 <<s 𝑅) & ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐿) ⇒ ⊢ (𝜑 → 𝐴 = (({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) |s 𝑅)) | ||
| Theorem | cutpos 27967* | Reduce the elements of a cut for a positive number. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = (({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) |s ( R ‘𝐴))) | ||
| Theorem | cutmax 27968* | If 𝐴 has a maximum, then the maximum may be used alone in the cut. (Contributed by Scott Fenton, 20-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑦 ∈ 𝐴 𝑦 ≤s 𝑋) ⇒ ⊢ (𝜑 → (𝐴 |s 𝐵) = ({𝑋} |s 𝐵)) | ||
| Theorem | cutmin 27969* | If 𝐵 has a minimum, then the minimum may be used alone in the cut. (Contributed by Scott Fenton, 20-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 𝑋 ≤s 𝑦) ⇒ ⊢ (𝜑 → (𝐴 |s 𝐵) = (𝐴 |s {𝑋})) | ||
| Syntax | cnorec 27970 | Declare the syntax for surreal recursion of one variable. |
| class norec (𝐹) | ||
| Definition | df-norec 27971* | Define the recursion generator for surreal functions of one variable. This generator creates a recursive function of surreals from their value on their left and right sets. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ norec (𝐹) = frecs({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝐹) | ||
| Theorem | lrrecval 27972* | The next step in the development of the surreals is to establish induction and recursion across left and right sets. To that end, we are going to develop a relationship 𝑅 that is founded, partial, and set-like across the surreals. This first theorem just establishes the value of 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝑅𝐵 ↔ 𝐴 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)))) | ||
| Theorem | lrrecval2 27973* | Next, we establish an alternate expression for 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝑅𝐵 ↔ ( bday ‘𝐴) ∈ ( bday ‘𝐵))) | ||
| Theorem | lrrecpo 27974* | Now, we establish that 𝑅 is a partial ordering on No . (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ 𝑅 Po No | ||
| Theorem | lrrecse 27975* | Next, we show that 𝑅 is set-like over No . (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ 𝑅 Se No | ||
| Theorem | lrrecfr 27976* | Now we show that 𝑅 is founded over No . (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ 𝑅 Fr No | ||
| Theorem | lrrecpred 27977* | Finally, we calculate the value of the predecessor class over 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ (𝐴 ∈ No → Pred(𝑅, No , 𝐴) = (( L ‘𝐴) ∪ ( R ‘𝐴))) | ||
| Theorem | noinds 27978* | Induction principle for a single surreal. If a property passes from a surreal's left and right sets to the surreal itself, then it holds for all surreals. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 ∈ No → (∀𝑦 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 → 𝜑)) ⇒ ⊢ (𝐴 ∈ No → 𝜒) | ||
| Theorem | norecfn 27979 | Surreal recursion over one variable is a function over the surreals. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝐹 = norec (𝐺) ⇒ ⊢ 𝐹 Fn No | ||
| Theorem | norecov 27980 | Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝐹 = norec (𝐺) ⇒ ⊢ (𝐴 ∈ No → (𝐹‘𝐴) = (𝐴𝐺(𝐹 ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))))) | ||
| Syntax | cnorec2 27981 | Declare the syntax for surreal recursion on two arguments. |
| class norec2 (𝐹) | ||
| Definition | df-norec2 27982* | Define surreal recursion on two variables. This function is key to the development of most of surreal numbers. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ norec2 (𝐹) = frecs({〈𝑎, 𝑏〉 ∣ (𝑎 ∈ ( No × No ) ∧ 𝑏 ∈ ( No × No ) ∧ (((1st ‘𝑎){〈𝑐, 𝑑〉 ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (1st ‘𝑏) ∨ (1st ‘𝑎) = (1st ‘𝑏)) ∧ ((2nd ‘𝑎){〈𝑐, 𝑑〉 ∣ 𝑐 ∈ (( L ‘𝑑) ∪ ( R ‘𝑑))} (2nd ‘𝑏) ∨ (2nd ‘𝑎) = (2nd ‘𝑏)) ∧ 𝑎 ≠ 𝑏))}, ( No × No ), 𝐹) | ||
| Theorem | noxpordpo 27983* | To get through most of the textbook definitions in surreal numbers we will need recursion on two variables. This set of theorems sets up the preconditions for double recursion. This theorem establishes the partial ordering. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑎, 𝑏〉 ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑅(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} ⇒ ⊢ 𝑆 Po ( No × No ) | ||
| Theorem | noxpordfr 27984* | Next we establish the foundedness of the relationship. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑎, 𝑏〉 ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑅(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} ⇒ ⊢ 𝑆 Fr ( No × No ) | ||
| Theorem | noxpordse 27985* | Next we establish the set-like nature of the relationship. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑎, 𝑏〉 ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑅(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} ⇒ ⊢ 𝑆 Se ( No × No ) | ||
| Theorem | noxpordpred 27986* | Next we calculate the predecessor class of the relationship. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑎, 𝑏〉 ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑅(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → Pred(𝑆, ( No × No ), 〈𝐴, 𝐵〉) = ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) | ||
| Theorem | no2indslem 27987* | Double induction on surreals with explicit notation for the relationships. (Contributed by Scott Fenton, 22-Aug-2024.) |
| ⊢ 𝑅 = {〈𝑎, 𝑏〉 ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑧 → (𝜃 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝑦 = 𝐵 → (𝜏 ↔ 𝜂)) & ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → ((∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜒 ∧ ∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 ∧ ∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜃) → 𝜑)) ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂) | ||
| Theorem | no2inds 27988* | Double induction on surreals. The many substitution instances are to cover all possible cases. (Contributed by Scott Fenton, 22-Aug-2024.) |
| ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑧 → (𝜃 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝑦 = 𝐵 → (𝜏 ↔ 𝜂)) & ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → ((∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜒 ∧ ∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 ∧ ∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜃) → 𝜑)) ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂) | ||
| Theorem | norec2fn 27989 | The double-recursion operator on surreals yields a function on pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ 𝐹 = norec2 (𝐺) ⇒ ⊢ 𝐹 Fn ( No × No ) | ||
| Theorem | norec2ov 27990 | The value of the double-recursion surreal function. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ 𝐹 = norec2 (𝐺) ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝐹𝐵) = (〈𝐴, 𝐵〉𝐺(𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})))) | ||
| Theorem | no3inds 27991* | Triple induction over surreal numbers. (Contributed by Scott Fenton, 9-Oct-2024.) |
| ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃)) & ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃)) & ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏)) & ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌)) & ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇)) & ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆)) & ⊢ ((𝑎 ∈ No ∧ 𝑏 ∈ No ∧ 𝑐 ∈ No ) → (((∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜃 ∧ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜒 ∧ ∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜁) ∧ (∀𝑑 ∈ (( L ‘𝑎) ∪ ( R ‘𝑎))𝜓 ∧ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜏 ∧ ∀𝑒 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))𝜎) ∧ ∀𝑓 ∈ (( L ‘𝑐) ∪ ( R ‘𝑐))𝜂) → 𝜑)) ⇒ ⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑍 ∈ No ) → 𝜆) | ||
| Syntax | cadds 27992 | Declare the syntax for surreal addition. |
| class +s | ||
| Definition | df-adds 27993* | Define surreal addition. This is the first of the field operations on the surreals. Definition from [Conway] p. 5. Definition from [Gonshor] p. 13. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ +s = norec2 ((𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st ‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd ‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)})))) | ||
| Theorem | addsfn 27994 | Surreal addition is a function over pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ +s Fn ( No × No ) | ||
| Theorem | addsval 27995* | The value of surreal addition. Definition from [Conway] p. 5. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s 𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑦 = (𝑟 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑧 = (𝐴 +s 𝑟)}))) | ||
| Theorem | addsval2 27996* | The value of surreal addition with different choices for each bound variable. Definition from [Conway] p. 5. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝐵)𝑡 = (𝐴 +s 𝑠)}))) | ||
| Theorem | addsrid 27997 | Surreal addition to zero is identity. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ (𝐴 ∈ No → (𝐴 +s 0s ) = 𝐴) | ||
| Theorem | addsridd 27998 | Surreal addition to zero is identity. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 +s 0s ) = 𝐴) | ||
| Theorem | addscom 27999 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (𝐵 +s 𝐴)) | ||
| Theorem | addscomd 28000 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 +s 𝐵) = (𝐵 +s 𝐴)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |