Home | Metamath
Proof Explorer Theorem List (p. 83 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fpr2a 8201 | Weak version of fpr2 8203 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 8202 | 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 8203 | 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 8204* | 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 8202 and fpr2 8203 is identical to 𝐹. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝑧𝐺(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝐹 = 𝐻) | ||
Theorem | frrrel 8205 | 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 8206 | 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 8207 | 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 8208 | A "function" defined by well-founded recursion is indeed a function when the relationship is a partial order. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → Fun 𝐹) | ||
Theorem | fprresex 8209 | 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 8210 | Declare syntax for the well-ordered recursive function generator. |
class wrecs(𝑅, 𝐴, 𝐹) | ||
Definition | df-wrecs 8211 | 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 8249, wfr2 8250, and wfr3 8251. (Contributed by Scott Fenton, 7-Jun-2018.) (Revised by BJ, 27-Oct-2024.) |
⊢ wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd )) | ||
Theorem | dfwrecsOLD 8212* | 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 8213 | 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 8214 | Obsolete proof of wrecseq123 8213 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 7-Jun-2018.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺) → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑆, 𝐵, 𝐺)) | ||
Theorem | nfwrecs 8215 | 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 8216 | Obsolete proof of nfwrecs 8215 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 9-Jun-2018.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥wrecs(𝑅, 𝐴, 𝐹) | ||
Theorem | wrecseq1 8217 | Equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) |
⊢ (𝑅 = 𝑆 → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑆, 𝐴, 𝐹)) | ||
Theorem | wrecseq2 8218 | Equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) |
⊢ (𝐴 = 𝐵 → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑅, 𝐵, 𝐹)) | ||
Theorem | wrecseq3 8219 | Equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) |
⊢ (𝐹 = 𝐺 → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑅, 𝐴, 𝐺)) | ||
Theorem | csbwrecsg 8220 | 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 8221* | 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 8222* | 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. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ 𝐵 = {𝑔 ∣ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))} | ||
Theorem | wfrlem2OLD 8223* | Lemma for well-ordered recursion. An acceptable function is a function. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔) | ||
Theorem | wfrlem3OLD 8224* | Lemma for well-ordered recursion. An acceptable function's domain is a subset of 𝐴. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → dom 𝑔 ⊆ 𝐴) | ||
Theorem | wfrlem3OLDa 8225* | Lemma for well-ordered recursion. Show membership in the class of acceptable functions. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 31-Jul-2020.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝐺 ∈ 𝐵 ↔ ∃𝑧(𝐺 Fn 𝑧 ∧ (𝑧 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤 ∈ 𝑧 (𝐺‘𝑤) = (𝐹‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑤))))) | ||
Theorem | wfrlem4OLD 8226* | Lemma for well-ordered recursion. Properties of the restriction of an acceptable function to the domain of another one. Obsolete as of 18-Nov-2024. (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 8227* | Lemma for well-ordered recursion. The values of two acceptable functions agree within their domains. Obsolete as of 18-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 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
Theorem | wfrrelOLD 8228 | Obsolete proof of wfrrel 8243 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 8-Jun-2018.) |
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Rel 𝐹 | ||
Theorem | wfrdmssOLD 8229 | Obsolete proof of wfrdmss 8244 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | wfrlem8OLD 8230 | Lemma for well-ordered recursion. Compute the prececessor class for an 𝑅 minimal element of (𝐴 ∖ dom 𝐹). Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑋) = ∅ ↔ Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, dom 𝐹, 𝑋)) | ||
Theorem | wfrdmclOLD 8231 | Obsolete proof of wfrdmcl 8245 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 8232* | Lemma for well-ordered recursion. When 𝑧 is an 𝑅 minimal element of (𝐴 ∖ dom 𝐹), then its predecessor class is equal to dom 𝐹. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → Pred(𝑅, 𝐴, 𝑧) = dom 𝐹) | ||
Theorem | wfrfunOLD 8233 | Obsolete proof of wfrfun 8246 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 8234* | Lemma for well-ordered recursion. Here, we compute the value of the recursive definition generator. Obsolete as of 18-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(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑦 ∈ dom 𝐹 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) | ||
Theorem | wfrlem13OLD 8235* | Lemma for well-ordered recursion. From here through wfrlem16OLD 8238, 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. Obsolete as of 18-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(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ⇒ ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝐶 Fn (dom 𝐹 ∪ {𝑧})) | ||
Theorem | wfrlem14OLD 8236* | Lemma for well-ordered recursion. Compute the value of 𝐶. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ⇒ ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (𝑦 ∈ (dom 𝐹 ∪ {𝑧}) → (𝐶‘𝑦) = (𝐺‘(𝐶 ↾ Pred(𝑅, 𝐴, 𝑦))))) | ||
Theorem | wfrlem15OLD 8237* | Lemma for well-ordered recursion. When 𝑧 is 𝑅 minimal, 𝐶 is an acceptable function. This step is where the Axiom of Replacement becomes required. Obsolete as of 18-Nov-2024. (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 8238* | 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 8229), dom 𝐹 = 𝐴. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) & ⊢ 𝐶 = (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ⇒ ⊢ dom 𝐹 = 𝐴 | ||
Theorem | wfrlem17OLD 8239 | Without using ax-rep 5241, show that all restrictions of wrecs are sets. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 31-Jul-2020.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ dom 𝐹 → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V) | ||
Theorem | wfr2aOLD 8240 | Obsolete proof of wfr2a 8248 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 8241 | Obsolete proof of wfr1 8249 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 8242 | Obsolete proof of wfr2 8250 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 8243 | 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 8244 | 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 8245 | 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 8246 | 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 8247 | 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 8248 | A weak version of wfr2 8250 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 8249 | 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 8250 | 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 8251* | 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 8249 and wfr2 8250 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 8252* | Obsolete form of wfr3 8251 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 8253* | 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 8254* | 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 8255* | 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 8256* | A variant of onfununi 8255 for operations. (Contributed by Eric Schmidt, 26-May-2009.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ (Lim 𝑦 → (𝐴𝐹𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐴𝐹𝑥)) & ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐴𝐹𝑥) ⊆ (𝐴𝐹𝑦)) ⇒ ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐴𝐹∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐴𝐹𝑥)) | ||
Theorem | onoviun 8257* | A variant of onovuni 8256 with indexed unions. (Contributed by Eric Schmidt, 26-May-2009.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
⊢ (Lim 𝑦 → (𝐴𝐹𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐴𝐹𝑥)) & ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐴𝐹𝑥) ⊆ (𝐴𝐹𝑦)) ⇒ ⊢ ((𝐾 ∈ 𝑇 ∧ ∀𝑧 ∈ 𝐾 𝐿 ∈ On ∧ 𝐾 ≠ ∅) → (𝐴𝐹∪ 𝑧 ∈ 𝐾 𝐿) = ∪ 𝑧 ∈ 𝐾 (𝐴𝐹𝐿)) | ||
Theorem | onnseq 8258* | There are no length ω decreasing sequences in the ordinals. See also noinfep 9530 for a stronger version assuming Regularity. (Contributed by Mario Carneiro, 19-May-2015.) |
⊢ ((𝐹‘∅) ∈ On → ∃𝑥 ∈ ω ¬ (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) | ||
Syntax | wsmo 8259 | Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals. |
wff Smo 𝐴 | ||
Definition | df-smo 8260* | 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 8261* | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.) |
⊢ (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) | ||
Theorem | issmo 8262* | Conditions for which 𝐴 is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.) Avoid ax-13 2372. (Revised by Gino Giotto, 19-May-2023.) |
⊢ 𝐴:𝐵⟶On & ⊢ Ord 𝐵 & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) & ⊢ dom 𝐴 = 𝐵 ⇒ ⊢ Smo 𝐴 | ||
Theorem | issmo2 8263* | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ (𝐹:𝐴⟶𝐵 → ((𝐵 ⊆ On ∧ Ord 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) → Smo 𝐹)) | ||
Theorem | smoeq 8264 | Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ (𝐴 = 𝐵 → (Smo 𝐴 ↔ Smo 𝐵)) | ||
Theorem | smodm 8265 | The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ (Smo 𝐴 → Ord dom 𝐴) | ||
Theorem | smores 8266 | 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 8267 | A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.) |
⊢ ((Smo (𝐴 ↾ 𝐵) ∧ 𝐶 ∈ (dom 𝐴 ∩ 𝐵) ∧ Ord 𝐵) → Smo (𝐴 ↾ 𝐶)) | ||
Theorem | smores2 8268 | A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.) |
⊢ ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴)) | ||
Theorem | smodm2 8269 | The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → Ord 𝐴) | ||
Theorem | smofvon2 8270 | The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ (Smo 𝐹 → (𝐹‘𝐵) ∈ On) | ||
Theorem | iordsmo 8271 | The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ Ord 𝐴 ⇒ ⊢ Smo ( I ↾ 𝐴) | ||
Theorem | smo0 8272 | The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.) |
⊢ Smo ∅ | ||
Theorem | smofvon 8273 | 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 8274 | 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 8275* | The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.) |
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵) → ∪ 𝑥 ∈ 𝐴 (𝐵‘𝑥) ⊆ (𝐵‘𝐴)) | ||
Theorem | smoiso 8276 | 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 8277 | A strictly monotone ordinal function preserves the membership relation. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)) → (𝐹‘𝐶) ∈ (𝐹‘𝐵)) | ||
Theorem | smo11 8278 | A strictly monotone ordinal function is one-to-one. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ Smo 𝐹) → 𝐹:𝐴–1-1→𝐵) | ||
Theorem | smoord 8279 | A strictly monotone ordinal function preserves strict ordering. (Contributed by Mario Carneiro, 4-Mar-2013.) |
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ∈ 𝐷 ↔ (𝐹‘𝐶) ∈ (𝐹‘𝐷))) | ||
Theorem | smoword 8280 | A strictly monotone ordinal function preserves weak ordering. (Contributed by Mario Carneiro, 4-Mar-2013.) |
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ⊆ 𝐷 ↔ (𝐹‘𝐶) ⊆ (𝐹‘𝐷))) | ||
Theorem | smogt 8281 | 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 | smocdmdom 8282 | The codomain of a strictly monotone ordinal function dominates the domain. (Contributed by Mario Carneiro, 13-Mar-2013.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵) → 𝐴 ⊆ 𝐵) | ||
Theorem | smoiso2 8283 | The strictly monotone ordinal functions are also isomorphisms of subclasses of On equipped with the membership relation. (Contributed by Mario Carneiro, 20-Mar-2013.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ⊆ On) → ((𝐹:𝐴–onto→𝐵 ∧ Smo 𝐹) ↔ 𝐹 Isom E , E (𝐴, 𝐵))) | ||
Syntax | crecs 8284 | Notation for a function defined by strong transfinite recursion. |
class recs(𝐹) | ||
Definition | df-recs 8285 | 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 8324 for more details on why this definition is desirable. Unlike df-rdg 8324 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 8317 and recsval 8318 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 8286* | The old definition of transfinite recursion. This version is preferred for development, as it demonstrates the properties of transfinite recursion without relying on well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (Proof revised by Scott Fenton, 18-Nov-2024.) |
⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} | ||
Theorem | dfrecs3OLD 8287* | Obsolete proof of dfrecs3 8286 as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 3-Aug-2020.) |
⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} | ||
Theorem | recseq 8288 | Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺)) | ||
Theorem | nfrecs 8289 | Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥recs(𝐹) | ||
Theorem | tfrlem1 8290* | 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 8291* | 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 8292* | 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 8293* | 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 8294* | 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 8295* | 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 8296* | 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 8297* | 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 8298* | 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 8299* | 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 8300* | Lemma for transfinite recursion. Without using ax-rep 5241, show that all the restrictions of recs are sets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) ∈ V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |