Home | Metamath
Proof Explorer Theorem List (p. 74 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wfrlem1 7301* | 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 Scott Fenton, 21-Apr-2011.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ 𝐵 = {𝑔 ∣ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))} | ||
Theorem | wfrlem2 7302* | Lemma for well-founded recursion. An acceptable function is a function. (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔) | ||
Theorem | wfrlem3 7303* | Lemma for well-founded recursion. An acceptable function's domain is a subset of 𝐴. (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → dom 𝑔 ⊆ 𝐴) | ||
Theorem | wfrlem3a 7304* | Lemma for well-founded recursion. Show membership in the class of acceptable functions. (Contributed by Scott Fenton, 31-Jul-2020.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝐺 ∈ 𝐵 ↔ ∃𝑧(𝐺 Fn 𝑧 ∧ (𝑧 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤 ∈ 𝑧 (𝐺‘𝑤) = (𝐹‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑤))))) | ||
Theorem | wfrlem4 7305* | Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another one. (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))) | ||
Theorem | wfrlem5 7306* | Lemma for well-founded recursion. The values of two acceptable functions agree within their domains. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
Theorem | wfrrel 7307 | The well-founded recursion generator generates a relationship. (Contributed by Scott Fenton, 8-Jun-2018.) |
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Rel 𝐹 | ||
Theorem | wfrdmss 7308 | The domain of the well-founded recursion generator is a subclass of 𝐴. (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | wfrlem8 7309 | Lemma for well-founded recursion. Compute the prececessor class for an 𝑅 minimal element of (𝐴 ∖ dom 𝐹). (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑋) = ∅ ↔ Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, dom 𝐹, 𝑋)) | ||
Theorem | wfrdmcl 7310 | Given 𝐹 = wrecs(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ dom 𝐹, then its predecessor class is a subset of dom 𝐹. (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐹) | ||
Theorem | wfrlem10 7311* | Lemma for well-founded recursion. When 𝑧 is an 𝑅 minimal element of (𝐴 ∖ dom 𝐹), then its predecessor class is equal to dom 𝐹. (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → Pred(𝑅, 𝐴, 𝑧) = dom 𝐹) | ||
Theorem | wfrfun 7312 | The well-founded function generator generates a function. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Fun 𝐹 | ||
Theorem | wfrlem12 7313* | Lemma for well-founded recursion. Here, we compute the value of the recursive definition generator. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑦 ∈ dom 𝐹 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) | ||
Theorem | wfrlem13 7314* | Lemma for well-founded recursion. From here through wfrlem16 7317, 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. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ⇒ ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝐶 Fn (dom 𝐹 ∪ {𝑧})) | ||
Theorem | wfrlem14 7315* | Lemma for well-founded recursion. Compute the value of 𝐶. (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ⇒ ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (𝑦 ∈ (dom 𝐹 ∪ {𝑧}) → (𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))))) | ||
Theorem | wfrlem15 7316* | Lemma for well-founded recursion. When 𝑧 is 𝑅 minimal, 𝐶 is an acceptable function. This step is where the Axiom of Replacement becomes required. (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ⇒ ⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → 𝐶 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) | ||
Theorem | wfrlem16 7317* | Lemma for well-founded 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 wfrdmss 7308), dom 𝐹 = 𝐴. (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) ⇒ ⊢ dom 𝐹 = 𝐴 | ||
Theorem | wfrlem17 7318 | Without using ax-rep 4699, show that all restrictions of wrecs are sets. (Contributed by Scott Fenton, 31-Jul-2020.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ dom 𝐹 → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V) | ||
Theorem | wfr2a 7319 | A weak version of wfr2 7321 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Scott Fenton, 30-Jul-2020.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ dom 𝐹 → (𝐹‘𝑋) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
Theorem | wfr1 7320 | The Principle of Well-Founded Recursion, part 1 of 3. We start with an arbitrary function 𝐺. Then, using a base class 𝐴 and a well-ordering 𝑅 of 𝐴, we define a function 𝐹. This function is said to be defined by "well-founded 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.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ 𝐹 Fn 𝐴 | ||
Theorem | wfr2 7321 | The Principle of Well-Founded Recursion, part 2 of 3. Next, we show that the value of 𝐹 at any 𝑋 ∈ 𝐴 is 𝐺 recursively applied to all "previous" values of 𝐹. (Contributed by Scott Fenton, 18-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ 𝐴 → (𝐹‘𝑋) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
Theorem | wfr3 7322* | The principle of Well-Founded 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 7320 and wfr2 7321 is identical to 𝐹. (Contributed by Scott Fenton, 18-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝐺‘(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧)))) → 𝐹 = 𝐻) | ||
Theorem | iunon 7323* | 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 7324* | 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 7325* | 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 7326* | A variant of onfununi 7325 for operations. (Contributed by Eric Schmidt, 26-May-2009.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ (Lim 𝑦 → (𝐴𝐹𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐴𝐹𝑥)) & ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐴𝐹𝑥) ⊆ (𝐴𝐹𝑦)) ⇒ ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐴𝐹∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐴𝐹𝑥)) | ||
Theorem | onoviun 7327* | A variant of onovuni 7326 with indexed unions. (Contributed by Eric Schmidt, 26-May-2009.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
⊢ (Lim 𝑦 → (𝐴𝐹𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐴𝐹𝑥)) & ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐴𝐹𝑥) ⊆ (𝐴𝐹𝑦)) ⇒ ⊢ ((𝐾 ∈ 𝑇 ∧ ∀𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅) → (𝐴𝐹∪ 𝑧 ∈ 𝐾 𝐿) = ∪ 𝑧 ∈ 𝐾 (𝐴𝐹𝐿)) | ||
Theorem | onnseq 7328* | There are no length ω decreasing sequences in the ordinals. See also noinfep 8440 for a stronger version assuming Regularity. (Contributed by Mario Carneiro, 19-May-2015.) |
⊢ ((𝐹‘∅) ∈ On → ∃𝑥 ∈ ω ¬ (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) | ||
Syntax | wsmo 7329 | Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals. |
wff Smo 𝐴 | ||
Definition | df-smo 7330* | 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 7331* | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.) |
⊢ (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) | ||
Theorem | issmo 7332* | Conditions for which 𝐴 is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.) |
⊢ 𝐴:𝐵⟶On & ⊢ Ord 𝐵 & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) & ⊢ dom 𝐴 = 𝐵 ⇒ ⊢ Smo 𝐴 | ||
Theorem | issmo2 7333* | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ (𝐹:𝐴⟶𝐵 → ((𝐵 ⊆ On ∧ Ord 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) → Smo 𝐹)) | ||
Theorem | smoeq 7334 | Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ (𝐴 = 𝐵 → (Smo 𝐴 ↔ Smo 𝐵)) | ||
Theorem | smodm 7335 | The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ (Smo 𝐴 → Ord dom 𝐴) | ||
Theorem | smores 7336 | 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 7337 | A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.) |
⊢ ((Smo (𝐴 ↾ 𝐵) ∧ 𝐶 ∈ (dom 𝐴 ∩ 𝐵) ∧ Ord 𝐵) → Smo (𝐴 ↾ 𝐶)) | ||
Theorem | smores2 7338 | A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.) |
⊢ ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴)) | ||
Theorem | smodm2 7339 | The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → Ord 𝐴) | ||
Theorem | smofvon2 7340 | The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ (Smo 𝐹 → (𝐹‘𝐵) ∈ On) | ||
Theorem | iordsmo 7341 | The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ Ord 𝐴 ⇒ ⊢ Smo ( I ↾ 𝐴) | ||
Theorem | smo0 7342 | The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.) |
⊢ Smo ∅ | ||
Theorem | smofvon 7343 | 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 7344 | 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 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐵‘𝐶) ∈ (𝐵‘𝐴)) | ||
Theorem | smoiun 7345* | The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.) |
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵) → ∪ 𝑥 ∈ 𝐴 (𝐵‘𝑥) ⊆ (𝐵‘𝐴)) | ||
Theorem | smoiso 7346 | If 𝐹 is an isomorphism from an ordinal 𝐴 onto 𝐵, which is a subset of the ordinals, then 𝐹 is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.) |
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → Smo 𝐹) | ||
Theorem | smoel2 7347 | A strictly monotone ordinal function preserves the epsilon relation. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)) → (𝐹‘𝐶) ∈ (𝐹‘𝐵)) | ||
Theorem | smo11 7348 | A strictly monotone ordinal function is one-to-one. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ Smo 𝐹) → 𝐹:𝐴–1-1→𝐵) | ||
Theorem | smoord 7349 | A strictly monotone ordinal function preserves strict ordering. (Contributed by Mario Carneiro, 4-Mar-2013.) |
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ∈ 𝐷 ↔ (𝐹‘𝐶) ∈ (𝐹‘𝐷))) | ||
Theorem | smoword 7350 | A strictly monotone ordinal function preserves weak ordering. (Contributed by Mario Carneiro, 4-Mar-2013.) |
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ⊆ 𝐷 ↔ (𝐹‘𝐶) ⊆ (𝐹‘𝐷))) | ||
Theorem | smogt 7351 | A strictly monotone ordinal function is greater than or equal to its argument. Exercise 1 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 23-Nov-2011.) (Revised by Mario Carneiro, 28-Feb-2013.) |
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝐶 ∈ 𝐴) → 𝐶 ⊆ (𝐹‘𝐶)) | ||
Theorem | smorndom 7352 | The range of a strictly monotone ordinal function dominates the domain. (Contributed by Mario Carneiro, 13-Mar-2013.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵) → 𝐴 ⊆ 𝐵) | ||
Theorem | smoiso2 7353 | The strictly monotone ordinal functions are also epsilon isomorphisms of subclasses of On. (Contributed by Mario Carneiro, 20-Mar-2013.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ⊆ On) → ((𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹) ↔ 𝐹 Isom E , E (𝐴, 𝐵))) | ||
Syntax | crecs 7354 | Notation for a function defined by strong transfinite recursion. |
class recs(𝐹) | ||
Definition | df-recs 7355 | Define a function recs(𝐹) on On, the class of ordinal numbers, by transfinite recursion given a rule 𝐹 which sets the next value given all values so far. See df-rdg 7393 for more details on why this definition is desirable. Unlike df-rdg 7393 which restricts the update rule to use only the previous value, this version allows the update rule to use all previous values, which is why it is described as "strong", although it is actually more primitive. See recsfnon 7386 and recsval 7387 for the primary contract of this definition. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Scott Fenton, 3-Aug-2020.) |
⊢ recs(𝐹) = wrecs( E , On, 𝐹) | ||
Theorem | dfrecs3 7356* | The old definition of transfinite recursion. This version is preferred for developement, as it demonstrates the properties of transfinite recursion without relying on well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.) |
⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} | ||
Theorem | recseq 7357 | Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺)) | ||
Theorem | nfrecs 7358 | Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥recs(𝐹) | ||
Theorem | tfrlem1 7359* | A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by Mario Carneiro, 24-May-2019.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹)) & ⊢ (𝜑 → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥))) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)) | ||
Theorem | tfrlem3a 7360* | Lemma for transfinite recursion. Let 𝐴 be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by NM, 9-Apr-1995.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝐺 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝐺 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝐺‘𝑤) = (𝐹‘(𝐺 ↾ 𝑤)))) | ||
Theorem | tfrlem3 7361* | Lemma for transfinite recursion. Let 𝐴 be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by NM, 9-Apr-1995.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))} | ||
Theorem | tfrlem4 7362* | Lemma for transfinite recursion. 𝐴 is the class of all "acceptable" functions, and 𝐹 is their union. First we show that an acceptable function is in fact a function. (Contributed by NM, 9-Apr-1995.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝑔 ∈ 𝐴 → Fun 𝑔) | ||
Theorem | tfrlem5 7363* | Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
Theorem | recsfval 7364* | Lemma for transfinite recursion. The definition recs is the union of all acceptable functions. (Contributed by Mario Carneiro, 9-May-2015.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ recs(𝐹) = ∪ 𝐴 | ||
Theorem | tfrlem6 7365* | Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ Rel recs(𝐹) | ||
Theorem | tfrlem7 7366* | Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ Fun recs(𝐹) | ||
Theorem | tfrlem8 7367* | Lemma for transfinite recursion. The domain of recs is an ordinal. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Alan Sare, 11-Mar-2008.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ Ord dom recs(𝐹) | ||
Theorem | tfrlem9 7368* | Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))) | ||
Theorem | tfrlem9a 7369* | Lemma for transfinite recursion. Without using ax-rep 4699, show that all the restrictions of recs are sets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) ∈ V) | ||
Theorem | tfrlem10 7370* | Lemma for transfinite recursion. We define class 𝐶 by extending recs with one ordered pair. We will assume, falsely, that domain of recs is a member of, and thus not equal to, On. Using this assumption we will prove facts about 𝐶 that will lead to a contradiction in tfrlem14 7374, thus showing the domain of recs does in fact equal On. Here we show (under the false assumption) that 𝐶 is a function extending the domain of recs(𝐹) by one. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐶 = (recs(𝐹) ∪ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) ⇒ ⊢ (dom recs(𝐹) ∈ On → 𝐶 Fn suc dom recs(𝐹)) | ||
Theorem | tfrlem11 7371* | Lemma for transfinite recursion. Compute the value of 𝐶. (Contributed by NM, 18-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐶 = (recs(𝐹) ∪ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) ⇒ ⊢ (dom recs(𝐹) ∈ On → (𝐵 ∈ suc dom recs(𝐹) → (𝐶‘𝐵) = (𝐹‘(𝐶 ↾ 𝐵)))) | ||
Theorem | tfrlem12 7372* | Lemma for transfinite recursion. Show 𝐶 is an acceptable function. (Contributed by NM, 15-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐶 = (recs(𝐹) ∪ {〈dom recs(𝐹), (𝐹‘recs(𝐹))〉}) ⇒ ⊢ (recs(𝐹) ∈ V → 𝐶 ∈ 𝐴) | ||
Theorem | tfrlem13 7373* | Lemma for transfinite recursion. If recs is a set function, then 𝐶 is acceptable, and thus a subset of recs, but dom 𝐶 is bigger than dom recs. This is a contradiction, so recs must be a proper class function. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ ¬ recs(𝐹) ∈ V | ||
Theorem | tfrlem14 7374* | Lemma for transfinite recursion. Assuming ax-rep 4699, dom recs ∈ V ↔ recs ∈ V, so since dom recs is an ordinal, it must be equal to On. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ dom recs(𝐹) = On | ||
Theorem | tfrlem15 7375* | Lemma for transfinite recursion. Without assuming ax-rep 4699, we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed by Mario Carneiro, 14-Nov-2014.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝐵 ∈ On → (𝐵 ∈ dom recs(𝐹) ↔ (recs(𝐹) ↾ 𝐵) ∈ V)) | ||
Theorem | tfrlem16 7376* | Lemma for finite recursion. Without assuming ax-rep 4699, we can show that the domain of the constructed function is a limit ordinal, and hence contains all the finite ordinals. (Contributed by Mario Carneiro, 14-Nov-2014.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ Lim dom recs(𝐹) | ||
Theorem | tfr1a 7377 | A weak version of tfr1 7380 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ (Fun 𝐹 ∧ Lim dom 𝐹) | ||
Theorem | tfr2a 7378 | A weak version of tfr2 7381 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴))) | ||
Theorem | tfr2b 7379 | Without assuming ax-rep 4699, we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ (Ord 𝐴 → (𝐴 ∈ dom 𝐹 ↔ (𝐹 ↾ 𝐴) ∈ V)) | ||
Theorem | tfr1 7380 | Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47. We start with an arbitrary class 𝐺, normally a function, and define a class 𝐴 of all "acceptable" functions. The final function we're interested in is the union 𝐹 = recs(𝐺) of them. 𝐹 is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of 𝐹. In this first part we show that 𝐹 is a function whose domain is all ordinal numbers. (Contributed by NM, 17-Aug-1994.) (Revised by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ 𝐹 Fn On | ||
Theorem | tfr2 7381 | Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47. Here we show that the function 𝐹 has the property that for any function 𝐺 whatsoever, the "next" value of 𝐹 is 𝐺 recursively applied to all "previous" values of 𝐹. (Contributed by NM, 9-Apr-1995.) (Revised by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴))) | ||
Theorem | tfr3 7382* | Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47. Finally, we show that 𝐹 is unique. We do this by showing that any class 𝐵 with the same properties of 𝐹 that we showed in parts 1 and 2 is identical to 𝐹. (Contributed by NM, 18-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ ((𝐵 Fn On ∧ ∀𝑥 ∈ On (𝐵‘𝑥) = (𝐺‘(𝐵 ↾ 𝑥))) → 𝐵 = 𝐹) | ||
Theorem | tfr1ALT 7383 | Alternate proof of tfr1 7380 using well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ 𝐹 Fn On | ||
Theorem | tfr2ALT 7384 | Alternate proof of tfr2 7381 using well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴))) | ||
Theorem | tfr3ALT 7385* | Alternate proof of tfr3 7382 using well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ ((𝐵 Fn On ∧ ∀𝑥 ∈ On (𝐵‘𝑥) = (𝐺‘(𝐵 ↾ 𝑥))) → 𝐵 = 𝐹) | ||
Theorem | recsfnon 7386 | Strong transfinite recursion defines a function on ordinals. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ recs(𝐹) Fn On | ||
Theorem | recsval 7387 | Strong transfinite recursion in terms of all previous values. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (𝐴 ∈ On → (recs(𝐹)‘𝐴) = (𝐹‘(recs(𝐹) ↾ 𝐴))) | ||
Theorem | tz7.44lem1 7388* | 𝐺 is a function. Lemma for tz7.44-1 7389, tz7.44-2 7390, and tz7.44-3 7391. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ 𝐺 = {〈𝑥, 𝑦〉 ∣ ((𝑥 = ∅ ∧ 𝑦 = 𝐴) ∨ (¬ (𝑥 = ∅ ∨ Lim dom 𝑥) ∧ 𝑦 = (𝐻‘(𝑥‘∪ dom 𝑥))) ∨ (Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥))} ⇒ ⊢ Fun 𝐺 | ||
Theorem | tz7.44-1 7389* | The value of 𝐹 at ∅. Part 1 of Theorem 7.44 of [TakeutiZaring] p. 49. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))))) & ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦))) & ⊢ 𝐴 ∈ V ⇒ ⊢ (∅ ∈ 𝑋 → (𝐹‘∅) = 𝐴) | ||
Theorem | tz7.44-2 7390* | The value of 𝐹 at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))))) & ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦))) & ⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V) & ⊢ 𝐹 Fn 𝑋 & ⊢ Ord 𝑋 ⇒ ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵))) | ||
Theorem | tz7.44-3 7391* | The value of 𝐹 at a limit ordinal. Part 3 of Theorem 7.44 of [TakeutiZaring] p. 49. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))))) & ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦))) & ⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V) & ⊢ 𝐹 Fn 𝑋 & ⊢ Ord 𝑋 ⇒ ⊢ ((𝐵 ∈ 𝑋 ∧ Lim 𝐵) → (𝐹‘𝐵) = ∪ (𝐹 “ 𝐵)) | ||
Syntax | crdg 7392 | Extend class notation with the recursive definition generator, with characteristic function 𝐹 and initial value 𝐼. |
class rec(𝐹, 𝐼) | ||
Definition | df-rdg 7393* |
Define a recursive definition generator on On (the
class of ordinal
numbers) with characteristic function 𝐹 and initial value 𝐼.
This combines functions 𝐹 in tfr1 7380
and 𝐺 in tz7.44-1 7389 into one
definition. This rather amazing operation allows us to define, with
compact direct definitions, functions that are usually defined in
textbooks only with indirect self-referencing recursive definitions. A
recursive definition requires advanced metalogic to justify - in
particular, eliminating a recursive definition is very difficult and
often not even shown in textbooks. On the other hand, the elimination
of a direct definition is a matter of simple mechanical substitution.
The price paid is the daunting complexity of our rec operation
(especially when df-recs 7355 that it is built on is also eliminated). But
once we get past this hurdle, definitions that would otherwise be
recursive become relatively simple, as in for example oav 7478,
from which
we prove the recursive textbook definition as theorems oa0 7483,
oasuc 7491,
and oalim 7499 (with the help of theorems rdg0 7404,
rdgsuc 7407, and
rdglim2a 7416). We can also restrict the rec operation to define
otherwise recursive functions on the natural numbers ω; see
fr0g 7418 and frsuc 7419. Our rec
operation apparently does not appear
in published literature, although closely related is Definition 25.2 of
[Quine] p. 177, which he uses to
"turn...a recursion into a genuine or
direct definition" (p. 174). Note that the if operations (see
df-if 4037) select cases based on whether the domain of
𝑔
is zero, a
successor, or a limit ordinal.
An important use of this definition is in the recursive sequence generator df-seq 12664 on the natural numbers (as a subset of the complex numbers), allowing us to define, with direct definitions, recursive infinite sequences such as the factorial function df-fac 12923 and integer powers df-exp 12723. Note: We introduce rec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐼, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))) | ||
Theorem | rdgeq1 7394 | Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ (𝐹 = 𝐺 → rec(𝐹, 𝐴) = rec(𝐺, 𝐴)) | ||
Theorem | rdgeq2 7395 | Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ (𝐴 = 𝐵 → rec(𝐹, 𝐴) = rec(𝐹, 𝐵)) | ||
Theorem | rdgeq12 7396 | Equality theorem for the recursive definition generator. (Contributed by Scott Fenton, 28-Apr-2012.) |
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → rec(𝐹, 𝐴) = rec(𝐺, 𝐵)) | ||
Theorem | nfrdg 7397 | Bound-variable hypothesis builder for the recursive definition generator. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥rec(𝐹, 𝐴) | ||
Theorem | rdglem1 7398* | Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. (Contributed by NM, 9-Apr-1995.) |
⊢ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))} | ||
Theorem | rdgfun 7399 | The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ Fun rec(𝐹, 𝐴) | ||
Theorem | rdgdmlim 7400 | The domain of the recursive definition generator is a limit ordinal. (Contributed by NM, 16-Nov-2014.) |
⊢ Lim dom rec(𝐹, 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |