| Metamath
Proof Explorer Theorem List (p. 84 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 | undefval 8301 | Value of the undefined value function. Normally we will not reference the explicit value but will use undefnel 8303 instead. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 24-Dec-2016.) |
| ⊢ (𝑆 ∈ 𝑉 → (Undef‘𝑆) = 𝒫 ∪ 𝑆) | ||
| Theorem | undefnel2 8302 | The undefined value generated from a set is not a member of the set. (Contributed by NM, 15-Sep-2011.) |
| ⊢ (𝑆 ∈ 𝑉 → ¬ (Undef‘𝑆) ∈ 𝑆) | ||
| Theorem | undefnel 8303 | The undefined value generated from a set is not a member of the set. (Contributed by NM, 15-Sep-2011.) |
| ⊢ (𝑆 ∈ 𝑉 → (Undef‘𝑆) ∉ 𝑆) | ||
| Theorem | undefne0 8304 | The undefined value generated from a set is not empty. (Contributed by NM, 3-Sep-2018.) |
| ⊢ (𝑆 ∈ 𝑉 → (Undef‘𝑆) ≠ ∅) | ||
| Syntax | cfrecs 8305 | Declare the syntax for the well-founded recursion generator. See df-frecs 8306. |
| class frecs(𝑅, 𝐴, 𝐹) | ||
| Definition | df-frecs 8306* | This is the definition for the well-founded recursion generator. Similar to df-wrecs 8337 and df-recs 8411, it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a well-founded set-like relationship for its properties, not a well-ordered relationship. This proof requires either a partial order or the axiom of infinity. We develop the theorems twice, once with a partial order and once without. The second development occurs later in the database, after ax-inf 9678 has been introduced. (Contributed by Scott Fenton, 23-Dec-2021.) |
| ⊢ frecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} | ||
| Theorem | frecseq123 8307 | Equality theorem for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺) → frecs(𝑅, 𝐴, 𝐹) = frecs(𝑆, 𝐵, 𝐺)) | ||
| Theorem | nffrecs 8308 | Bound-variable hypothesis builder for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥frecs(𝑅, 𝐴, 𝐹) | ||
| Theorem | csbfrecsg 8309 | Move class substitution in and out of the well-founded recursive function generator. (Contributed by Scott Fenton, 18-Nov-2024.) |
| ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌frecs(𝑅, 𝐷, 𝐹) = frecs(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝐹)) | ||
| Theorem | fpr3g 8310* | Functions defined by well-founded recursion over a partial order are identical up to relation, domain, and characteristic function. This version of frr3g 9796 does not require infinity. (Contributed by Scott Fenton, 24-Aug-2022.) |
| ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝑦𝐻(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) = (𝑦𝐻(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺) | ||
| Theorem | frrlem1 8311* | Lemma for well-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 8312* | Lemma for well-founded recursion. An acceptable function is a function. (Contributed by Paul Chapman, 21-Apr-2012.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔) | ||
| Theorem | frrlem3 8313* | Lemma for well-founded recursion. An acceptable function's domain is a subset of 𝐴. (Contributed by Paul Chapman, 21-Apr-2012.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → dom 𝑔 ⊆ 𝐴) | ||
| Theorem | frrlem4 8314* | Lemma for well-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 8315* | Lemma for well-founded recursion. State the well-founded recursion generator in terms of the acceptable functions. (Contributed by Scott Fenton, 27-Aug-2022.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ 𝐹 = ∪ 𝐵 | ||
| Theorem | frrlem6 8316* | Lemma for well-founded recursion. The well-founded recursion generator is a relation. (Contributed by Scott Fenton, 27-Aug-2022.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Rel 𝐹 | ||
| Theorem | frrlem7 8317* | Lemma for well-founded recursion. The well-founded recursion generator's domain is a subclass of 𝐴. (Contributed by Scott Fenton, 27-Aug-2022.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
| Theorem | frrlem8 8318* | Lemma for well-founded recursion. dom 𝐹 is closed under predecessor classes. (Contributed by Scott Fenton, 6-Dec-2022.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑧 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹) | ||
| Theorem | frrlem9 8319* | Lemma for well-founded recursion. Show that the well-founded recursive generator produces a function. Hypothesis three will be eliminated using different induction rules depending on if we use partial orders or the axiom of infinity. (Contributed by Scott Fenton, 27-Aug-2022.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
| Theorem | frrlem10 8320* | Lemma for well-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 8321* | Lemma for well-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 orders or the axiom of infinity. To begin with, we establish the functionality of 𝐶. (Contributed by Scott Fenton, 7-Dec-2022.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) & ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {〈𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) | ||
| Theorem | frrlem12 8322* | Lemma for well-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 8323* | Lemma for well-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 8324* | Lemma for well-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 8325* | Lemma for well-founded recursion with a partial order. Two acceptable functions are compatible. (Contributed by Scott Fenton, 11-Sep-2023.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
| Theorem | fprlem2 8326* | Lemma for well-founded recursion with a partial order. Establish a subset relation. (Contributed by Scott Fenton, 11-Sep-2023.) |
| ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)Pred(𝑅, 𝐴, 𝑤) ⊆ Pred(𝑅, 𝐴, 𝑧)) | ||
| Theorem | fpr2a 8327 | Weak version of fpr2 8329 which is useful for proofs that avoid the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024.) |
| ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ dom 𝐹) → (𝐹‘𝑋) = (𝑋𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
| Theorem | fpr1 8328 | Law of well-founded recursion over a partial order, part one. Establish the functionality and domain of the recursive function generator. Note that by requiring a partial order we can avoid using the axiom of infinity. (Contributed by Scott Fenton, 11-Sep-2023.) |
| ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Fn 𝐴) | ||
| Theorem | fpr2 8329 | Law of well-founded recursion over a partial order, part two. Now we establish the value of 𝐹 within 𝐴. (Contributed by Scott Fenton, 11-Sep-2023.) (Proof shortened by Scott Fenton, 18-Nov-2024.) |
| ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = (𝑋𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
| Theorem | fpr3 8330* | Law of well-founded recursion over a partial order, 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 8328 and fpr2 8329 is identical to 𝐹. (Contributed by Scott Fenton, 11-Sep-2023.) |
| ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝑧𝐺(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝐹 = 𝐻) | ||
| Theorem | frrrel 8331 | Show without using the axiom of replacement that the well-founded recursion generator gives a relation. (Contributed by Scott Fenton, 18-Nov-2024.) |
| ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Rel 𝐹 | ||
| Theorem | frrdmss 8332 | Show without using the axiom of replacement that the domain of the well-founded recursion generator is a subclass of 𝐴. (Contributed by Scott Fenton, 18-Nov-2024.) |
| ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
| Theorem | frrdmcl 8333 | Show without using the axiom of replacement that for a "function" defined by well-founded recursion, the predecessor class of an element of its domain is a subclass of its domain. (Contributed by Scott Fenton, 21-Apr-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
| ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐹) | ||
| Theorem | fprfung 8334 | A "function" defined by well-founded recursion is indeed a function when the relation is a partial order. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024.) |
| ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → Fun 𝐹) | ||
| Theorem | fprresex 8335 | The restriction of a function defined by well-founded recursion to the predecessor of an element of its domain is a set. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024.) |
| ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ dom 𝐹) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V) | ||
| Syntax | cwrecs 8336 | Declare syntax for the well-ordered recursive function generator. |
| class wrecs(𝑅, 𝐴, 𝐹) | ||
| Definition | df-wrecs 8337 | Define the well-ordered recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function 𝐹, a relation 𝑅, and a base set 𝐴, this definition generates a function 𝐺 = wrecs(𝑅, 𝐴, 𝐹) that has property that, at any point 𝑥 ∈ 𝐴, (𝐺‘𝑥) = (𝐹‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑥))). See wfr1 8375, wfr2 8376, and wfr3 8377. (Contributed by Scott Fenton, 7-Jun-2018.) (Revised by BJ, 27-Oct-2024.) |
| ⊢ wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd )) | ||
| Theorem | dfwrecsOLD 8338* | Obsolete definition of the well-ordered recursive function generator as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 7-Jun-2018.) |
| ⊢ wrecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} | ||
| Theorem | wrecseq123 8339 | General equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺) → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑆, 𝐵, 𝐺)) | ||
| Theorem | wrecseq123OLD 8340 | Obsolete version of wrecseq123 8339 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 7-Jun-2018.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺) → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑆, 𝐵, 𝐺)) | ||
| Theorem | nfwrecs 8341 | Bound-variable hypothesis builder for the well-ordered recursive function generator. (Contributed by Scott Fenton, 9-Jun-2018.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥wrecs(𝑅, 𝐴, 𝐹) | ||
| Theorem | nfwrecsOLD 8342 | Obsolete version of nfwrecs 8341 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 9-Jun-2018.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥wrecs(𝑅, 𝐴, 𝐹) | ||
| Theorem | wrecseq1 8343 | Equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) |
| ⊢ (𝑅 = 𝑆 → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑆, 𝐴, 𝐹)) | ||
| Theorem | wrecseq2 8344 | Equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) |
| ⊢ (𝐴 = 𝐵 → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑅, 𝐵, 𝐹)) | ||
| Theorem | wrecseq3 8345 | Equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) |
| ⊢ (𝐹 = 𝐺 → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑅, 𝐴, 𝐺)) | ||
| Theorem | csbwrecsg 8346 | Move class substitution in and out of the well-founded recursive function generator. (Contributed by ML, 25-Oct-2020.) (Revised by Scott Fenton, 18-Nov-2024.) |
| ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌wrecs(𝑅, 𝐷, 𝐹) = wrecs(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝐹)) | ||
| Theorem | wfr3g 8347* | Functions defined by well-ordered recursion are identical up to relation, domain, and characteristic function. (Contributed by Scott Fenton, 11-Feb-2011.) |
| ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺) | ||
| Theorem | wfrlem1OLD 8348* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. The final item we are interested in is the union of acceptable functions 𝐵. This lemma just changes bound variables for later use. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ 𝐵 = {𝑔 ∣ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))} | ||
| Theorem | wfrlem2OLD 8349* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. An acceptable function is a function. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔) | ||
| Theorem | wfrlem3OLD 8350* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. An acceptable function's domain is a subset of 𝐴. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → dom 𝑔 ⊆ 𝐴) | ||
| Theorem | wfrlem3OLDa 8351* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. Show membership in the class of acceptable functions. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 31-Jul-2020.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝐺 ∈ 𝐵 ↔ ∃𝑧(𝐺 Fn 𝑧 ∧ (𝑧 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤 ∈ 𝑧 (𝐺‘𝑤) = (𝐹‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑤))))) | ||
| Theorem | wfrlem4OLD 8352* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. Properties of the restriction of an acceptable function to the domain of another one. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by AV, 18-Jul-2022.) |
| ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))) | ||
| Theorem | wfrlem5OLD 8353* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. The values of two acceptable functions agree within their domains. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
| Theorem | wfrrelOLD 8354 | Obsolete version of wfrrel 8369 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 8-Jun-2018.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Rel 𝐹 | ||
| Theorem | wfrdmssOLD 8355 | Obsolete version of wfrdmss 8370 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
| Theorem | wfrlem8OLD 8356 | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. Compute the predecessor class for an 𝑅 minimal element of (𝐴 ∖ dom 𝐹). (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑋) = ∅ ↔ Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, dom 𝐹, 𝑋)) | ||
| Theorem | wfrdmclOLD 8357 | Obsolete version of wfrdmcl 8371 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐹) | ||
| Theorem | wfrlem10OLD 8358* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. When 𝑧 is an 𝑅 minimal element of (𝐴 ∖ dom 𝐹), then its predecessor class is equal to dom 𝐹. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → Pred(𝑅, 𝐴, 𝑧) = dom 𝐹) | ||
| Theorem | wfrfunOLD 8359 | Obsolete version of wfrfun 8372 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Fun 𝐹 | ||
| Theorem | wfrlem12OLD 8360* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. Here, we compute the value of the recursive definition generator. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑦 ∈ dom 𝐹 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) | ||
| Theorem | wfrlem13OLD 8361* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. From here through wfrlem16OLD 8364, we aim to prove that dom 𝐹 = 𝐴. We do this by supposing that there is an element 𝑧 of 𝐴 that is not in dom 𝐹. We then define 𝐶 by extending dom 𝐹 with the appropriate value at 𝑧. We then show that 𝑧 cannot be an 𝑅 minimal element of (𝐴 ∖ dom 𝐹), meaning that (𝐴 ∖ dom 𝐹) must be empty, so dom 𝐹 = 𝐴. Here, we show that 𝐶 is a function extending the domain of 𝐹 by one. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ⇒ ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝐶 Fn (dom 𝐹 ∪ {𝑧})) | ||
| Theorem | wfrlem14OLD 8362* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. Compute the value of 𝐶. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ⇒ ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (𝑦 ∈ (dom 𝐹 ∪ {𝑧}) → (𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))))) | ||
| Theorem | wfrlem15OLD 8363* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. When 𝑧 is 𝑅 minimal, 𝐶 is an acceptable function. This step is where the Axiom of Replacement becomes required. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ⇒ ⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → 𝐶 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) | ||
| Theorem | wfrlem16OLD 8364* | Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. If 𝑧 is 𝑅 minimal in (𝐴 ∖ dom 𝐹), then 𝐶 is acceptable and thus a subset of 𝐹, but dom 𝐶 is bigger than dom 𝐹. Thus, 𝑧 cannot be minimal, so (𝐴 ∖ dom 𝐹) must be empty, and (due to wfrdmssOLD 8355), dom 𝐹 = 𝐴. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ⇒ ⊢ dom 𝐹 = 𝐴 | ||
| Theorem | wfrlem17OLD 8365 | Obsolete version as of 18-Nov-2024. Without using ax-rep 5279, show that all restrictions of wrecs are sets. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 31-Jul-2020.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ dom 𝐹 → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V) | ||
| Theorem | wfr2aOLD 8366 | Obsolete version of wfr2a 8374 as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 30-Jul-2020.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ dom 𝐹 → (𝐹‘𝑋) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
| Theorem | wfr1OLD 8367 | Obsolete version of wfr1 8375 as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 22-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ 𝐹 Fn 𝐴 | ||
| Theorem | wfr2OLD 8368 | Obsolete version of wfr2 8376 as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 18-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ 𝐴 → (𝐹‘𝑋) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
| Theorem | wfrrel 8369 | The well-ordered recursion generator generates a relation. Avoids the axiom of replacement. (Contributed by Scott Fenton, 8-Jun-2018.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Rel 𝐹 | ||
| Theorem | wfrdmss 8370 | The domain of the well-ordered recursion generator is a subclass of 𝐴. Avoids the axiom of replacement. (Contributed by Scott Fenton, 21-Apr-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
| Theorem | wfrdmcl 8371 | The predecessor class of an element of the well-ordered recursion generator's domain is a subset of its domain. Avoids the axiom of replacement. (Contributed by Scott Fenton, 21-Apr-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐹) | ||
| Theorem | wfrfun 8372 | The "function" generated by the well-ordered recursion generator is indeed a function. Avoids the axiom of replacement. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by Scott Fenton, 17-Nov-2024.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → Fun 𝐹) | ||
| Theorem | wfrresex 8373 | Show without using the axiom of replacement that the restriction of the well-ordered recursion generator to a predecessor class is a set. (Contributed by Scott Fenton, 18-Nov-2024.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ dom 𝐹) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V) | ||
| Theorem | wfr2a 8374 | A weak version of wfr2 8376 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Scott Fenton, 30-Jul-2020.) (Proof shortened by Scott Fenton, 18-Nov-2024.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ dom 𝐹) → (𝐹‘𝑋) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
| Theorem | wfr1 8375 | The Principle of Well-Ordered Recursion, part 1 of 3. We start with an arbitrary function 𝐺. Then, using a base class 𝐴 and a set-like well-ordering 𝑅 of 𝐴, we define a function 𝐹. This function is said to be defined by "well-ordered recursion". The purpose of these three theorems is to demonstrate the properties of 𝐹. We begin by showing that 𝐹 is a function over 𝐴. (Contributed by Scott Fenton, 22-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by Scott Fenton, 18-Nov-2024.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Fn 𝐴) | ||
| Theorem | wfr2 8376 | The Principle of Well-Ordered Recursion, part 2 of 3. Next, we show that the value of 𝐹 at any 𝑋 ∈ 𝐴 is 𝐺 applied to all "previous" values of 𝐹. (Contributed by Scott Fenton, 18-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
| Theorem | wfr3 8377* | The principle of Well-Ordered Recursion, part 3 of 3. Finally, we show that 𝐹 is unique. We do this by showing that any function 𝐻 with the same properties we proved of 𝐹 in wfr1 8375 and wfr2 8376 is identical to 𝐹. (Contributed by Scott Fenton, 18-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by Scott Fenton, 18-Nov-2024.) |
| ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝐺‘(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝐹 = 𝐻) | ||
| Theorem | wfr3OLD 8378* | Obsolete form of wfr3 8377 as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 18-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝐺‘(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧)))) → 𝐹 = 𝐻) | ||
| Theorem | iunon 8379* | The indexed union of a set of ordinal numbers 𝐵(𝑥) is an ordinal number. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 5-Dec-2016.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ On) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ On) | ||
| Theorem | iinon 8380* | The nonempty indexed intersection of a class of ordinal numbers 𝐵(𝑥) is an ordinal number. (Contributed by NM, 13-Oct-2003.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
| ⊢ ((∀𝑥 ∈ 𝐴 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ On) | ||
| Theorem | onfununi 8381* | A property of functions on ordinal numbers. Generalization of Theorem Schema 8E of [Enderton] p. 218. (Contributed by Eric Schmidt, 26-May-2009.) |
| ⊢ (Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥)) & ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) ⇒ ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)) | ||
| Theorem | onovuni 8382* | A variant of onfununi 8381 for operations. (Contributed by Eric Schmidt, 26-May-2009.) (Revised by Mario Carneiro, 11-Sep-2015.) |
| ⊢ (Lim 𝑦 → (𝐴𝐹𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐴𝐹𝑥)) & ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐴𝐹𝑥) ⊆ (𝐴𝐹𝑦)) ⇒ ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐴𝐹∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐴𝐹𝑥)) | ||
| Theorem | onoviun 8383* | A variant of onovuni 8382 with indexed unions. (Contributed by Eric Schmidt, 26-May-2009.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
| ⊢ (Lim 𝑦 → (𝐴𝐹𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐴𝐹𝑥)) & ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐴𝐹𝑥) ⊆ (𝐴𝐹𝑦)) ⇒ ⊢ ((𝐾 ∈ 𝑇 ∧ ∀𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅) → (𝐴𝐹∪ 𝑧 ∈ 𝐾 𝐿) = ∪ 𝑧 ∈ 𝐾 (𝐴𝐹𝐿)) | ||
| Theorem | onnseq 8384* | There are no length ω decreasing sequences in the ordinals. See also noinfep 9700 for a stronger version assuming Regularity. (Contributed by Mario Carneiro, 19-May-2015.) |
| ⊢ ((𝐹‘∅) ∈ On → ∃𝑥 ∈ ω ¬ (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) | ||
| Syntax | wsmo 8385 | Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals. |
| wff Smo 𝐴 | ||
| Definition | df-smo 8386* | Definition of a strictly monotone ordinal function. Definition 7.46 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 15-Nov-2011.) |
| ⊢ (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) | ||
| Theorem | dfsmo2 8387* | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.) |
| ⊢ (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) | ||
| Theorem | issmo 8388* | Conditions for which 𝐴 is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.) Avoid ax-13 2377. (Revised by GG, 19-May-2023.) |
| ⊢ 𝐴:𝐵⟶On & ⊢ Ord 𝐵 & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) & ⊢ dom 𝐴 = 𝐵 ⇒ ⊢ Smo 𝐴 | ||
| Theorem | issmo2 8389* | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.) |
| ⊢ (𝐹:𝐴⟶𝐵 → ((𝐵 ⊆ On ∧ Ord 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) → Smo 𝐹)) | ||
| Theorem | smoeq 8390 | Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.) |
| ⊢ (𝐴 = 𝐵 → (Smo 𝐴 ↔ Smo 𝐵)) | ||
| Theorem | smodm 8391 | The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.) |
| ⊢ (Smo 𝐴 → Ord dom 𝐴) | ||
| Theorem | smores 8392 | A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
| ⊢ ((Smo 𝐴 ∧ 𝐵 ∈ dom 𝐴) → Smo (𝐴 ↾ 𝐵)) | ||
| Theorem | smores3 8393 | A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.) |
| ⊢ ((Smo (𝐴 ↾ 𝐵) ∧ 𝐶 ∈ (dom 𝐴 ∩ 𝐵) ∧ Ord 𝐵) → Smo (𝐴 ↾ 𝐶)) | ||
| Theorem | smores2 8394 | A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.) |
| ⊢ ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴)) | ||
| Theorem | smodm2 8395 | The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → Ord 𝐴) | ||
| Theorem | smofvon2 8396 | The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.) |
| ⊢ (Smo 𝐹 → (𝐹‘𝐵) ∈ On) | ||
| Theorem | iordsmo 8397 | The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.) |
| ⊢ Ord 𝐴 ⇒ ⊢ Smo ( I ↾ 𝐴) | ||
| Theorem | smo0 8398 | The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.) |
| ⊢ Smo ∅ | ||
| Theorem | smofvon 8399 | If 𝐵 is a strictly monotone ordinal function, and 𝐴 is in the domain of 𝐵, then the value of the function at 𝐴 is an ordinal. (Contributed by Andrew Salmon, 20-Nov-2011.) |
| ⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵) → (𝐵‘𝐴) ∈ On) | ||
| Theorem | smoel 8400 | If 𝑥 is less than 𝑦 then a strictly monotone function's value will be strictly less at 𝑥 than at 𝑦. (Contributed by Andrew Salmon, 22-Nov-2011.) |
| ⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐵‘𝐶) ∈ (𝐵‘𝐴)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |