![]() |
Metamath
Proof Explorer Theorem List (p. 280 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-old 27901 | 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 27902 | 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 27903* | 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 27904* | 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 27905 | The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)))) | ||
Theorem | madeval2 27906* | Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)}) | ||
Theorem | oldval 27907 | The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ (𝐴 ∈ On → ( O ‘𝐴) = ∪ ( M “ 𝐴)) | ||
Theorem | newval 27908 | The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( N ‘𝐴) = (( M ‘𝐴) ∖ ( O ‘𝐴)) | ||
Theorem | madef 27909 | The made function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ M :On⟶𝒫 No | ||
Theorem | oldf 27910 | The older function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ O :On⟶𝒫 No | ||
Theorem | newf 27911 | The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ N :On⟶𝒫 No | ||
Theorem | old0 27912 | No surreal is older than ∅. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ ( O ‘∅) = ∅ | ||
Theorem | madessno 27913 | Made sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( M ‘𝐴) ⊆ No | ||
Theorem | oldssno 27914 | Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( O ‘𝐴) ⊆ No | ||
Theorem | newssno 27915 | New sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( N ‘𝐴) ⊆ No | ||
Theorem | leftval 27916* | The value of the left options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( L ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} | ||
Theorem | rightval 27917* | The value of the right options function. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( R ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥} | ||
Theorem | leftf 27918 | The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ L : No ⟶𝒫 No | ||
Theorem | rightf 27919 | The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ R : No ⟶𝒫 No | ||
Theorem | elmade 27920* | Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024.) |
⊢ (𝐴 ∈ On → (𝑋 ∈ ( M ‘𝐴) ↔ ∃𝑙 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑟 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑙 <<s 𝑟 ∧ (𝑙 |s 𝑟) = 𝑋))) | ||
Theorem | elmade2 27921* | 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 27922* | Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ (𝐴 ∈ On → (𝑋 ∈ ( O ‘𝐴) ↔ ∃𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘𝑏))) | ||
Theorem | ssltleft 27923 | 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 27924 | 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 27925 | 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 27926 | The only surreal made on day ∅ is 0s. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ ( M ‘∅) = { 0s } | ||
Theorem | new0 27927 | The only surreal new on day ∅ is 0s. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ ( N ‘∅) = { 0s } | ||
Theorem | old1 27928 | The only surreal older than 1o is 0s. (Contributed by Scott Fenton, 4-Feb-2025.) |
⊢ ( O ‘1o) = { 0s } | ||
Theorem | madess 27929 | 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 27930 | The older-than set is a subset of the made set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( O ‘𝐴) ⊆ ( M ‘𝐴) | ||
Theorem | leftssold 27931 | The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)) | ||
Theorem | rightssold 27932 | The right options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)) | ||
Theorem | leftssno 27933 | The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( L ‘𝐴) ⊆ No | ||
Theorem | rightssno 27934 | The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( R ‘𝐴) ⊆ No | ||
Theorem | madecut 27935 | 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 27936 | 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 27937 | The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( O ‘suc 𝐴)) | ||
Theorem | oldsuc 27938 | The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ (𝐴 ∈ On → ( O ‘suc 𝐴) = (( O ‘𝐴) ∪ ( N ‘𝐴))) | ||
Theorem | oldlim 27939 | The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → ( O ‘𝐴) = ∪ ( O “ 𝐴)) | ||
Theorem | madebdayim 27940 | 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 27941 | 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 27942 | No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.) |
⊢ ¬ 𝑋 ∈ ( O ‘( bday ‘𝑋)) | ||
Theorem | leftirr 27943 | No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ¬ 𝑋 ∈ ( L ‘𝑋) | ||
Theorem | rightirr 27944 | No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ¬ 𝑋 ∈ ( R ‘𝑋) | ||
Theorem | left0s 27945 | The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ ( L ‘ 0s ) = ∅ | ||
Theorem | right0s 27946 | The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ ( R ‘ 0s ) = ∅ | ||
Theorem | left1s 27947 | The left set of 1s is the singleton of 0s. (Contributed by Scott Fenton, 4-Feb-2025.) |
⊢ ( L ‘ 1s ) = { 0s } | ||
Theorem | right1s 27948 | The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025.) |
⊢ ( R ‘ 1s ) = ∅ | ||
Theorem | lrold 27949 | 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 27950* | Lemma for madebday 27952. If the inductive hypothesis of madebday 27952 is satisfied, the converse of oldbdayim 27941 holds. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ ((𝐴 ∈ On ∧ ∀𝑏 ∈ 𝐴 ∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( bday ‘𝑋) ∈ 𝐴 → 𝑋 ∈ ( O ‘𝐴))) | ||
Theorem | madebdaylemlrcut 27951* | Lemma for madebday 27952. If the inductive hypothesis of madebday 27952 is satisfied up to the birthday of 𝑋, then the conclusion of lrcut 27955 holds. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ ((∀𝑏 ∈ ( bday ‘𝑋)∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋) | ||
Theorem | madebday 27952 | 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 27953 | 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 27954 | 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 27955 | 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 27956 | The surreal cut function is onto. (Contributed by Scott Fenton, 23-Aug-2024.) |
⊢ |s : <<s –onto→ No | ||
Theorem | sltn0 27957 | 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 27958 | 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 27959 | 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 27960 | 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 27961 | 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 27962 | Zero is in the left set of any positive number. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐴) ⇒ ⊢ (𝜑 → 0s ∈ ( L ‘𝐴)) | ||
Theorem | 0elright 27963 | Zero is in the right set of any negative number. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 0s ) ⇒ ⊢ (𝜑 → 0s ∈ ( R ‘𝐴)) | ||
Theorem | madefi 27964 | The made set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.) |
⊢ (𝐴 ∈ ω → ( M ‘𝐴) ∈ Fin) | ||
Theorem | oldfi 27965 | The old set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.) |
⊢ (𝐴 ∈ ω → ( O ‘𝐴) ∈ Fin) | ||
Theorem | cofsslt 27966* | 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 27967* | If 𝐵 is coinitial with 𝐶 and 𝐴 precedes 𝐶, then 𝐴 precedes 𝐵. (Contributed by Scott Fenton, 24-Sep-2024.) |
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s 𝐵) | ||
Theorem | cofcut1 27968* | 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 27969* | 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 27970* | 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 27971* | 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 27972* | 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 27973* | 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 27974* | 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 27975* | 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 27976* | 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 27977* | 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 27978* | Cofinality for a subset. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐴 ⊆ No ) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦) | ||
Theorem | coiniss 27979* | Coinitiality for a subset. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐴 ⊆ No ) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑦 ≤s 𝑥) | ||
Theorem | cutlt 27980* | 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 27981* | 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 27982* | 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 27983* | 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 27984 | Declare the syntax for surreal recursion of one variable. |
class norec (𝐹) | ||
Definition | df-norec 27985* | 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 27986* | 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 27987* | Next, we establish an alternate expression for 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝑅𝐵 ↔ ( bday ‘𝐴) ∈ ( bday ‘𝐵))) | ||
Theorem | lrrecpo 27988* | Now, we establish that 𝑅 is a partial ordering on No . (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ 𝑅 Po No | ||
Theorem | lrrecse 27989* | Next, we show that 𝑅 is set-like over No . (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ 𝑅 Se No | ||
Theorem | lrrecfr 27990* | Now we show that 𝑅 is founded over No . (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ 𝑅 Fr No | ||
Theorem | lrrecpred 27991* | 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 27992* | 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 27993 | Surreal recursion over one variable is a function over the surreals. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝐹 = norec (𝐺) ⇒ ⊢ 𝐹 Fn No | ||
Theorem | norecov 27994 | Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝐹 = norec (𝐺) ⇒ ⊢ (𝐴 ∈ No → (𝐹‘𝐴) = (𝐴𝐺(𝐹 ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))))) | ||
Syntax | cnorec2 27995 | Declare the syntax for surreal recursion on two arguments. |
class norec2 (𝐹) | ||
Definition | df-norec2 27996* | 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 27997* | 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 27998* | 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 27999* | 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 28000* | 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 ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |