Home | Metamath
Proof Explorer Theorem List (p. 331 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wsuceq2 33001 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝐴 = 𝐵 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐵, 𝑋)) | ||
Theorem | wsuceq3 33002 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑋 = 𝑌 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐴, 𝑌)) | ||
Theorem | nfwsuc 33003 | Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑋 ⇒ ⊢ Ⅎ𝑥wsuc(𝑅, 𝐴, 𝑋) | ||
Theorem | wlimeq12 33004 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐵)) | ||
Theorem | wlimeq1 33005 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
⊢ (𝑅 = 𝑆 → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐴)) | ||
Theorem | wlimeq2 33006 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
⊢ (𝐴 = 𝐵 → WLim(𝑅, 𝐴) = WLim(𝑅, 𝐵)) | ||
Theorem | nfwlim 33007 | Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥WLim(𝑅, 𝐴) | ||
Theorem | elwlim 33008 | Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
⊢ (𝑋 ∈ WLim(𝑅, 𝐴) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑋 = sup(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅))) | ||
Theorem | wzel 33009 | The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → inf(𝐴, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | wsuclem 33010* | Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑧𝑅𝑦))) | ||
Theorem | wsucex 33011 | Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ V) | ||
Theorem | wsuccl 33012* | If 𝑋 is a set with an 𝑅 successor in 𝐴, then its well-founded successor is a member of 𝐴. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋𝑅𝑦) ⇒ ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ 𝐴) | ||
Theorem | wsuclb 33013 | A well-founded successor is a lower bound on points after 𝑋. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑅𝑌) ⇒ ⊢ (𝜑 → ¬ 𝑌𝑅wsuc(𝑅, 𝐴, 𝑋)) | ||
Theorem | wlimss 33014 | The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.) |
⊢ WLim(𝑅, 𝐴) ⊆ 𝐴 | ||
Syntax | cfrecs 33015 | Declare the syntax for the founded recursion generator. See df-frecs 33016. |
class frecs(𝑅, 𝐴, 𝐹) | ||
Definition | df-frecs 33016* | This is the definition for the founded recursion generator. Similar to df-wrecs 7938 and df-recs 7999, it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a founded set-like relationship for its properties, not a well-founded relationship. When this relationship is also a partial ordering, the proof does not use the Axiom of Infinity, but it requires Infinity when the order is not partial. We develop the theorems twice, once with partial ordering and once without. (Contributed by Scott Fenton, 23-Dec-2021.) |
⊢ frecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} | ||
Theorem | frecseq123 33017 | Equality theorem for founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺) → frecs(𝑅, 𝐴, 𝐹) = frecs(𝑆, 𝐵, 𝐺)) | ||
Theorem | nffrecs 33018 | Bound-variable hypothesis builder for the founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥frecs(𝑅, 𝐴, 𝐹) | ||
Theorem | frr3g 33019* | Functions defined by founded recursion are identical up to relation, domain, and characteristic function. General version of frr3. (Contributed by Scott Fenton, 10-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝑦𝐻(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) = (𝑦𝐻(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺) | ||
Theorem | fpr3g 33020* | Functions defined by founded recursion over a partial ordering are identical up to relation, domain, and characteristic function. This version of frr3g 33019 does not require infinity. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝑦𝐻(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) = (𝑦𝐻(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺) | ||
Theorem | frrlem1 33021* | Lemma for founded recursion. The final item we are interested in is the union of acceptable functions 𝐵. This lemma just changes bound variables for later use. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ 𝐵 = {𝑔 ∣ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))} | ||
Theorem | frrlem2 33022* | Lemma for founded recursion. An acceptable function is a function. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔) | ||
Theorem | frrlem3 33023* | Lemma for founded recursion. An acceptable function's domain is a subset of 𝐴. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → dom 𝑔 ⊆ 𝐴) | ||
Theorem | frrlem4 33024* | Lemma for founded recursion. Properties of the restriction of an acceptable function to the domain of another acceptable function. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))) | ||
Theorem | frrlem5 33025* | Lemma for founded recursion. State the founded recursion generator in terms of the acceptable functions. (Contributed by Scott Fenton, 27-Aug-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ 𝐹 = ∪ 𝐵 | ||
Theorem | frrlem6 33026* | Lemma for founded recursion. The founded recursion generator is a relationship. (Contributed by Scott Fenton, 27-Aug-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Rel 𝐹 | ||
Theorem | frrlem7 33027* | Lemma for founded recursion. The founded recursion generator's domain is a subclass of 𝐴. (Contributed by Scott Fenton, 27-Aug-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | frrlem8 33028* | Lemma for founded recursion. dom 𝐹 is closed under predecessor classes. (Contributed by Scott Fenton, 6-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑧 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹) | ||
Theorem | frrlem9 33029* | Lemma for founded recursion. Show that the founded recursive generator produces a function. Hypothesis three will be eliminated using different induction rules depending on if we use partial ordering or Infinity. (Contributed by Scott Fenton, 27-Aug-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | frrlem10 33030* | Lemma for founded recursion. Under the compatibility hypothesis, compute the value of 𝐹 within its domain. (Contributed by Scott Fenton, 6-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) ⇒ ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) | ||
Theorem | frrlem11 33031* | Lemma for founded recursion. For the next several theorems we will be aiming to prove that dom 𝐹 = 𝐴. To do this, we set up a function 𝐶 that supposedly contains an element of 𝐴 that is not in dom 𝐹 and we show that the element must be in dom 𝐹. Our choice of what to restrict 𝐹 to depends on if we assume partial ordering or Infinity. To begin with, we establish the functionhood of 𝐶. (Contributed by Scott Fenton, 7-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) & ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) | ||
Theorem | frrlem12 33032* | Lemma for founded recursion. Next, we calculate the value of 𝐶. (Contributed by Scott Fenton, 7-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) & ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) & ⊢ (𝜑 → 𝑅 Fr 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) | ||
Theorem | frrlem13 33033* | Lemma for founded recursion. Assuming that 𝑆 is a subset of 𝐴 and that 𝑧 is 𝑅-minimal, then 𝐶 is an acceptable function. (Contributed by Scott Fenton, 7-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) & ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) & ⊢ (𝜑 → 𝑅 Fr 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ∈ V) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ 𝐵) | ||
Theorem | frrlem14 33034* | Lemma for founded recursion. Finally, we tie all these threads together and show that dom 𝐹 = 𝐴 when given the right 𝑆. Specifically, we prove that there can be no 𝑅-minimal element of (𝐴 ∖ dom 𝐹). (Contributed by Scott Fenton, 7-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) & ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) & ⊢ (𝜑 → 𝑅 Fr 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ∈ V) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ⊆ 𝐴) & ⊢ ((𝜑 ∧ (𝐴 ∖ dom 𝐹) ≠ ∅) → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) ⇒ ⊢ (𝜑 → dom 𝐹 = 𝐴) | ||
Theorem | fprlem1 33035* | Lemma for founded partial recursion. Two acceptable functions are compatible. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
Theorem | fprlem2 33036* | Lemma for founded partial recursion. Establish a subset relationship. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)Pred(𝑅, 𝐴, 𝑤) ⊆ Pred(𝑅, 𝐴, 𝑧)) | ||
Theorem | fpr1 33037 | Law of founded partial recursion, part one. This development mostly follows the well-founded recursion development. Note that by requiring a partial ordering we can avoid using the Axiom of Infinity. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Fn 𝐴) | ||
Theorem | fpr2 33038 | Law of founded partial recursion, part two. Now we establish the value of 𝐹 within 𝐴. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = (𝑋𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
Theorem | fpr3 33039* | Law of founded partial recursion, part three. Finally, we show that 𝐹 is unique. We do this by showing that any function 𝐻 with the same properties we proved of 𝐹 in fpr1 33037 and fpr2 33038 is identical to 𝐹. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝑧𝐺(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝐹 = 𝐻) | ||
Theorem | frrlem15 33040* | Lemma for general founded recursion. Two acceptable functions are compatible. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
Theorem | frrlem16 33041* | Lemma for general founded recursion. Establish a subset relationship. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ TrPred (𝑅, 𝐴, 𝑧)Pred(𝑅, 𝐴, 𝑤) ⊆ TrPred(𝑅, 𝐴, 𝑧)) | ||
Theorem | frr1 33042 | Law of general founded recursion, part one. This may look like a restatement of the founded partial recursion theorems dropping the partial ordering requirement, but that change mandates that we use the Axiom of Infinity. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Fn 𝐴) | ||
Theorem | frr2 33043 | Law of general founded recursion, part two. Now we establish the value of 𝐹 within 𝐴. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = (𝑋𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
Theorem | frr3 33044* | Law of general founded recursion, part three. Finally, we show that 𝐹 is unique. We do this by showing that any function 𝐻 with the same properties we proved of 𝐹 in frr1 33042 and frr2 33043 is identical to 𝐹. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝑧𝐺(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝐹 = 𝐻) | ||
Syntax | csur 33045 | Declare the class of all surreal numbers (see df-no 33048). |
class No | ||
Syntax | cslt 33046 | Declare the less than relationship over surreal numbers (see df-slt 33049). |
class <s | ||
Syntax | cbday 33047 | Declare the birthday function for surreal numbers (see df-bday 33050). |
class bday | ||
Definition | df-no 33048* |
Define the class of surreal numbers. The surreal numbers are a proper
class of numbers developed by John H. Conway and introduced by Donald
Knuth in 1975. They form a proper class into which all ordered fields
can be embedded. The approach we take to defining them was first
introduced by Hary Goshnor, and is based on the conception of a
"sign
expansion" of a surreal number. We define the surreals as
ordinal-indexed sequences of 1o and
2o, analagous to Goshnor's
( − ) and ( + ).
After introducing this definition, we will abstract away from it using axioms that Norman Alling developed in "Foundations of Analysis over Surreal Number Fields." This is done in an effort to be agnostic towards the exact implementation of surreals. (Contributed by Scott Fenton, 9-Jun-2011.) |
⊢ No = {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1o, 2o}} | ||
Definition | df-slt 33049* | Next, we introduce surreal less-than, a comparison relationship over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011.) |
⊢ <s = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){〈1o, ∅〉, 〈1o, 2o〉, 〈∅, 2o〉} (𝑔‘𝑥)))} | ||
Definition | df-bday 33050 | Finally, we introduce the birthday function. This function maps each surreal to an ordinal. In our implementation, this is the domain of the sign function. The important properties of this function are established later. (Contributed by Scott Fenton, 11-Jun-2011.) |
⊢ bday = (𝑥 ∈ No ↦ dom 𝑥) | ||
Theorem | elno 33051* | Membership in the surreals. (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011.) |
⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o}) | ||
Theorem | sltval 33052* | The value of the surreal less than relationship. (Contributed by Scott Fenton, 14-Jun-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉, 〈1o, 2o〉, 〈∅, 2o〉} (𝐵‘𝑥)))) | ||
Theorem | bdayval 33053 | The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.) |
⊢ (𝐴 ∈ No → ( bday ‘𝐴) = dom 𝐴) | ||
Theorem | nofun 33054 | A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → Fun 𝐴) | ||
Theorem | nodmon 33055 | The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → dom 𝐴 ∈ On) | ||
Theorem | norn 33056 | The range of a surreal is a subset of the surreal signs. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → ran 𝐴 ⊆ {1o, 2o}) | ||
Theorem | nofnbday 33057 | A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → 𝐴 Fn ( bday ‘𝐴)) | ||
Theorem | nodmord 33058 | The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → Ord dom 𝐴) | ||
Theorem | elno2 33059 | An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.) |
⊢ (𝐴 ∈ No ↔ (Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ {1o, 2o})) | ||
Theorem | elno3 33060 | Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.) |
⊢ (𝐴 ∈ No ↔ (𝐴:dom 𝐴⟶{1o, 2o} ∧ dom 𝐴 ∈ On)) | ||
Theorem | sltval2 33061* | Alternate expression for surreal less than. Two surreals obey surreal less than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉, 〈1o, 2o〉, 〈∅, 2o〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) | ||
Theorem | nofv 33062 | The function value of a surreal is either a sign or the empty set. (Contributed by Scott Fenton, 22-Jun-2011.) |
⊢ (𝐴 ∈ No → ((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = 2o)) | ||
Theorem | nosgnn0 33063 | ∅ is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ ¬ ∅ ∈ {1o, 2o} | ||
Theorem | nosgnn0i 33064 | If 𝑋 is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011.) |
⊢ 𝑋 ∈ {1o, 2o} ⇒ ⊢ ∅ ≠ 𝑋 | ||
Theorem | noreson 33065 | The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ↾ 𝐵) ∈ No ) | ||
Theorem | sltintdifex 33066* | 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 33067 | 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 33068 | The Cartesian product of an ordinal and {1o} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.) |
⊢ (𝐴 ∈ On → (𝐴 × {1o}) ∈ No ) | ||
Theorem | noseponlem 33069* | Lemma for nosepon 33070. Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) | ||
Theorem | nosepon 33070* | 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 33071 | 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 33072 | Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021.) |
⊢ 𝑋 ∈ {1o, 2o} ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No ) | ||
Theorem | noextenddif 33073* | 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 33074 | 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 33075 | 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 33076 | 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 33077 | 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 𝑋)) | ||
Theorem | sltsolem1 33078 | Lemma for sltso 33079. 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 33079 | Surreal less than totally orders the surreals. Alling's axiom (O). (Contributed by Scott Fenton, 9-Jun-2011.) |
⊢ <s Or No | ||
Theorem | bdayfo 33080 | 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 | ||
Theorem | fvnobday 33081 | 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 33082* | Lemma for nosepne 33083. (Contributed by Scott Fenton, 24-Nov-2021.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) | ||
Theorem | nosepne 33083* | 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 33084* | 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 33085* | Lemma for nosepdm 33086. (Contributed by Scott Fenton, 24-Nov-2021.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ (dom 𝐴 ∪ dom 𝐵)) | ||
Theorem | nosepdm 33086* | 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 33087* | 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 33088* | 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 33089* | Lemma for nodense 33094. Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) | ||
Theorem | nodenselem5 33090* | Lemma for nodense 33094. If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 33089 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday ‘𝐴)) | ||
Theorem | nodenselem6 33091* | The restriction of a surreal to the abstraction from nodenselem4 33089 is still a surreal. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No ) | ||
Theorem | nodenselem7 33092* | Lemma for nodense 33094. 𝐴 and 𝐵 are equal at all elements of the abstraction. (Contributed by Scott Fenton, 17-Jun-2011.) |
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝐶) = (𝐵‘𝐶))) | ||
Theorem | nodenselem8 33093* | Lemma for nodense 33094. 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 33094* | 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 𝐵)) | ||
Theorem | bdayimaon 33095 | 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 33096 | Lemma for nolt02o 33097. If 𝐴(𝑋) is undefined with 𝐴 surreal and 𝑋 ordinal, then dom 𝐴 ⊆ 𝑋. (Contributed by Scott Fenton, 6-Dec-2021.) |
⊢ ((𝐴 ∈ No ∧ 𝑋 ∈ On ∧ (𝐴‘𝑋) = ∅) → dom 𝐴 ⊆ 𝑋) | ||
Theorem | nolt02o 33097 | 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 33098* | 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 33099* | A class of surreals has at most one maximum. (Contributed by Scott Fenton, 5-Dec-2021.) |
⊢ (𝑆 ⊆ No → ∃*𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ¬ 𝑥 <s 𝑦) | ||
Theorem | noprefixmo 33100* | 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 𝐺)) ∧ (𝑢‘𝐺) = 𝑥)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |