Home | Metamath
Proof Explorer Theorem List (p. 81 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | recseq 8001 | Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺)) | ||
Theorem | nfrecs 8002 | Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥recs(𝐹) | ||
Theorem | tfrlem1 8003* | 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 8004* | 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 8005* | 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 8006* | 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 8007* | 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 8008* | 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 8009* | 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 8010* | 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 8011* | 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 8012* | 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 8013* | Lemma for transfinite recursion. Without using ax-rep 5182, show that all the restrictions of recs are sets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹) ↾ 𝐵) ∈ V) | ||
Theorem | tfrlem10 8014* | 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 8018, 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 8015* | 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 8016* | 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 8017* | 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 8018* | Lemma for transfinite recursion. Assuming ax-rep 5182, 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 8019* | Lemma for transfinite recursion. Without assuming ax-rep 5182, 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 8020* | Lemma for finite recursion. Without assuming ax-rep 5182, 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 8021 | A weak version of tfr1 8024 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ (Fun 𝐹 ∧ Lim dom 𝐹) | ||
Theorem | tfr2a 8022 | A weak version of tfr2 8025 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴))) | ||
Theorem | tfr2b 8023 | Without assuming ax-rep 5182, 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 8024 | 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 8025 | 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 8026* | 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 8027 | Alternate proof of tfr1 8024 using well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ 𝐹 Fn On | ||
Theorem | tfr2ALT 8028 | Alternate proof of tfr2 8025 using well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴))) | ||
Theorem | tfr3ALT 8029* | Alternate proof of tfr3 8026 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 8030 | Strong transfinite recursion defines a function on ordinals. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ recs(𝐹) Fn On | ||
Theorem | recsval 8031 | Strong transfinite recursion in terms of all previous values. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (𝐴 ∈ On → (recs(𝐹)‘𝐴) = (𝐹‘(recs(𝐹) ↾ 𝐴))) | ||
Theorem | tz7.44lem1 8032* | 𝐺 is a function. Lemma for tz7.44-1 8033, tz7.44-2 8034, and tz7.44-3 8035. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
⊢ 𝐺 = {〈𝑥, 𝑦〉 ∣ ((𝑥 = ∅ ∧ 𝑦 = 𝐴) ∨ (¬ (𝑥 = ∅ ∨ Lim dom 𝑥) ∧ 𝑦 = (𝐻‘(𝑥‘∪ dom 𝑥))) ∨ (Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥))} ⇒ ⊢ Fun 𝐺 | ||
Theorem | tz7.44-1 8033* | 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 8034* | The value of 𝐹 at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49. (Contributed by NM, 23-Apr-1995.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ 𝐺 = (𝑥 ∈ V ↦ if(𝑥 = ∅, 𝐴, if(Lim dom 𝑥, ∪ ran 𝑥, (𝐻‘(𝑥‘∪ dom 𝑥))))) & ⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝐺‘(𝐹 ↾ 𝑦))) & ⊢ (𝑦 ∈ 𝑋 → (𝐹 ↾ 𝑦) ∈ V) & ⊢ 𝐹 Fn 𝑋 & ⊢ Ord 𝑋 ⇒ ⊢ (suc 𝐵 ∈ 𝑋 → (𝐹‘suc 𝐵) = (𝐻‘(𝐹‘𝐵))) | ||
Theorem | tz7.44-3 8035* | 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 8036 | Extend class notation with the recursive definition generator, with characteristic function 𝐹 and initial value 𝐼. |
class rec(𝐹, 𝐼) | ||
Definition | df-rdg 8037* |
Define a recursive definition generator on On (the
class of ordinal
numbers) with characteristic function 𝐹 and initial value 𝐼.
This combines functions 𝐹 in tfr1 8024
and 𝐺 in tz7.44-1 8033 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 7999 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 8127,
from which
we prove the recursive textbook definition as theorems oa0 8132,
oasuc 8140,
and oalim 8148 (with the help of theorems rdg0 8048,
rdgsuc 8051, and
rdglim2a 8060). We can also restrict the rec operation to define
otherwise recursive functions on the natural numbers ω; see
fr0g 8062 and frsuc 8063. 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 4466) 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 13360 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 13624 and integer powers df-exp 13420. 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 8038 | Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ (𝐹 = 𝐺 → rec(𝐹, 𝐴) = rec(𝐺, 𝐴)) | ||
Theorem | rdgeq2 8039 | Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ (𝐴 = 𝐵 → rec(𝐹, 𝐴) = rec(𝐹, 𝐵)) | ||
Theorem | rdgeq12 8040 | Equality theorem for the recursive definition generator. (Contributed by Scott Fenton, 28-Apr-2012.) |
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐵) → rec(𝐹, 𝐴) = rec(𝐺, 𝐵)) | ||
Theorem | nfrdg 8041 | 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 8042* | 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 8043 | The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ Fun rec(𝐹, 𝐴) | ||
Theorem | rdgdmlim 8044 | The domain of the recursive definition generator is a limit ordinal. (Contributed by NM, 16-Nov-2014.) |
⊢ Lim dom rec(𝐹, 𝐴) | ||
Theorem | rdgfnon 8045 | The recursive definition generator is a function on ordinal numbers. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ rec(𝐹, 𝐴) Fn On | ||
Theorem | rdgvalg 8046* | Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐴, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(rec(𝐹, 𝐴) ↾ 𝐵))) | ||
Theorem | rdgval 8047* | Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐵 ∈ On → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐴, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(rec(𝐹, 𝐴) ↾ 𝐵))) | ||
Theorem | rdg0 8048 | The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rec(𝐹, 𝐴)‘∅) = 𝐴 | ||
Theorem | rdgseg 8049 | The initial segments of the recursive definition generator are sets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V) | ||
Theorem | rdgsucg 8050 | The value of the recursive definition generator at a successor. (Contributed by NM, 16-Nov-2014.) |
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | rdgsuc 8051 | The value of the recursive definition generator at a successor. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ (𝐵 ∈ On → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | rdglimg 8052 | The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 16-Nov-2014.) |
⊢ ((𝐵 ∈ dom rec(𝐹, 𝐴) ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ (rec(𝐹, 𝐴) “ 𝐵)) | ||
Theorem | rdglim 8053 | The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ (rec(𝐹, 𝐴) “ 𝐵)) | ||
Theorem | rdg0g 8054 | The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.) |
⊢ (𝐴 ∈ 𝐶 → (rec(𝐹, 𝐴)‘∅) = 𝐴) | ||
Theorem | rdgsucmptf 8055 | The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by NM, 22-Oct-2003.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐷 & ⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴) & ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | rdgsucmptnf 8056 | The value of the recursive definition generator at a successor (special case where the characteristic function is an ordered-pair class abstraction and where the mapping class 𝐷 is a proper class). This is a technical lemma that can be used together with rdgsucmptf 8055 to help eliminate redundant sethood antecedents. (Contributed by NM, 22-Oct-2003.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐷 & ⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴) & ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (¬ 𝐷 ∈ V → (𝐹‘suc 𝐵) = ∅) | ||
Theorem | rdgsucmpt2 8057* | This version of rdgsucmpt 8058 avoids the not-free hypothesis of rdgsucmptf 8055 by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴) & ⊢ (𝑦 = 𝑥 → 𝐸 = 𝐶) & ⊢ (𝑦 = (𝐹‘𝐵) → 𝐸 = 𝐷) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | rdgsucmpt 8058* | The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by Mario Carneiro, 9-Sep-2013.) |
⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴) & ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | rdglim2 8059* | The value of the recursive definition generator at a limit ordinal, in terms of the union of all smaller values. (Contributed by NM, 23-Apr-1995.) |
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = (rec(𝐹, 𝐴)‘𝑥)}) | ||
Theorem | rdglim2a 8060* | The value of the recursive definition generator at a limit ordinal, in terms of indexed union of all smaller values. (Contributed by NM, 28-Jun-1998.) |
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ 𝑥 ∈ 𝐵 (rec(𝐹, 𝐴)‘𝑥)) | ||
Theorem | frfnom 8061 | The function generated by finite recursive definition generation is a function on omega. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ (rec(𝐹, 𝐴) ↾ ω) Fn ω | ||
Theorem | fr0g 8062 | The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.) |
⊢ (𝐴 ∈ 𝐵 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴) | ||
Theorem | frsuc 8063 | The successor value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐵 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝐵) = (𝐹‘((rec(𝐹, 𝐴) ↾ ω)‘𝐵))) | ||
Theorem | frsucmpt 8064 | The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation). (Contributed by NM, 14-Sep-2003.) (Revised by Scott Fenton, 2-Nov-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐷 & ⊢ 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) & ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ((𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | frsucmptn 8065 | The value of the finite recursive definition generator at a successor (special case where the characteristic function is a mapping abstraction and where the mapping class 𝐷 is a proper class). This is a technical lemma that can be used together with frsucmpt 8064 to help eliminate redundant sethood antecedents. (Contributed by Scott Fenton, 19-Feb-2011.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐷 & ⊢ 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) & ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (¬ 𝐷 ∈ V → (𝐹‘suc 𝐵) = ∅) | ||
Theorem | frsucmpt2w 8066* | Version of frsucmpt2 8067 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) & ⊢ (𝑦 = 𝑥 → 𝐸 = 𝐶) & ⊢ (𝑦 = (𝐹‘𝐵) → 𝐸 = 𝐷) ⇒ ⊢ ((𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | frsucmpt2 8067* | The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation), using double-substitution instead of a bound variable condition. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) & ⊢ (𝑦 = 𝑥 → 𝐸 = 𝐶) & ⊢ (𝑦 = (𝐹‘𝐵) → 𝐸 = 𝐷) ⇒ ⊢ ((𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | tz7.48lem 8068* | A way of showing an ordinal function is one-to-one. (Contributed by NM, 9-Feb-1997.) |
⊢ 𝐹 Fn On ⇒ ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ◡(𝐹 ↾ 𝐴)) | ||
Theorem | tz7.48-2 8069* | Proposition 7.48(2) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) (Revised by David Abernethy, 5-May-2013.) |
⊢ 𝐹 Fn On ⇒ ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → Fun ◡𝐹) | ||
Theorem | tz7.48-1 8070* | Proposition 7.48(1) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) |
⊢ 𝐹 Fn On ⇒ ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ran 𝐹 ⊆ 𝐴) | ||
Theorem | tz7.48-3 8071* | Proposition 7.48(3) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) |
⊢ 𝐹 Fn On ⇒ ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ 𝐴 ∈ V) | ||
Theorem | tz7.49 8072* | Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 10-Jan-2013.) |
⊢ 𝐹 Fn On & ⊢ (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ◡(𝐹 ↾ 𝑥))) | ||
Theorem | tz7.49c 8073* | Corollary of Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 19-Jan-2013.) |
⊢ 𝐹 Fn On ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴) | ||
Syntax | cseqom 8074 | Extend class notation to include index-aware recursive definitions. |
class seqω(𝐹, 𝐼) | ||
Definition | df-seqom 8075* | Index-aware recursive definitions over ω. A mashup of df-rdg 8037 and df-seq 13360, this allows for recursive definitions that use an index in the recursion in cases where Infinity is not admitted. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ seqω(𝐹, 𝐼) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) “ ω) | ||
Theorem | seqomlem0 8076* | Lemma for seqω. Change bound variables. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ rec((𝑎 ∈ ω, 𝑏 ∈ V ↦ 〈suc 𝑎, (𝑎𝐹𝑏)〉), 〈∅, ( I ‘𝐼)〉) = rec((𝑐 ∈ ω, 𝑑 ∈ V ↦ 〈suc 𝑐, (𝑐𝐹𝑑)〉), 〈∅, ( I ‘𝐼)〉) | ||
Theorem | seqomlem1 8077* | Lemma for seqω. The underlying recursion generates a sequence of pairs with the expected first values. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.) |
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ⇒ ⊢ (𝐴 ∈ ω → (𝑄‘𝐴) = 〈𝐴, (2nd ‘(𝑄‘𝐴))〉) | ||
Theorem | seqomlem2 8078* | Lemma for seqω. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.) |
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ⇒ ⊢ (𝑄 “ ω) Fn ω | ||
Theorem | seqomlem3 8079* | Lemma for seqω. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ⇒ ⊢ ((𝑄 “ ω)‘∅) = ( I ‘𝐼) | ||
Theorem | seqomlem4 8080* | Lemma for seqω. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.) |
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ⇒ ⊢ (𝐴 ∈ ω → ((𝑄 “ ω)‘suc 𝐴) = (𝐴𝐹((𝑄 “ ω)‘𝐴))) | ||
Theorem | seqomeq12 8081 | Equality theorem for seqω. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → seqω(𝐴, 𝐶) = seqω(𝐵, 𝐷)) | ||
Theorem | fnseqom 8082 | An index-aware recursive definition defines a function on the natural numbers. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ 𝐺 = seqω(𝐹, 𝐼) ⇒ ⊢ 𝐺 Fn ω | ||
Theorem | seqom0g 8083 | Value of an index-aware recursive definition at 0. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by AV, 17-Sep-2021.) |
⊢ 𝐺 = seqω(𝐹, 𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝐺‘∅) = 𝐼) | ||
Theorem | seqomsuc 8084 | Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ 𝐺 = seqω(𝐹, 𝐼) ⇒ ⊢ (𝐴 ∈ ω → (𝐺‘suc 𝐴) = (𝐴𝐹(𝐺‘𝐴))) | ||
Theorem | omsucelsucb 8085 | Membership is inherited by successors for natural numbers. (Contributed by AV, 15-Sep-2023.) |
⊢ (𝑁 ∈ ω ↔ suc 𝑁 ∈ suc ω) | ||
Syntax | c1o 8086 | Extend the definition of a class to include the ordinal number 1. |
class 1o | ||
Syntax | c2o 8087 | Extend the definition of a class to include the ordinal number 2. |
class 2o | ||
Syntax | c3o 8088 | Extend the definition of a class to include the ordinal number 3. |
class 3o | ||
Syntax | c4o 8089 | Extend the definition of a class to include the ordinal number 4. |
class 4o | ||
Syntax | coa 8090 | Extend the definition of a class to include the ordinal addition operation. |
class +o | ||
Syntax | comu 8091 | Extend the definition of a class to include the ordinal multiplication operation. |
class ·o | ||
Syntax | coe 8092 | Extend the definition of a class to include the ordinal exponentiation operation. |
class ↑o | ||
Definition | df-1o 8093 | Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
⊢ 1o = suc ∅ | ||
Definition | df-2o 8094 | Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
⊢ 2o = suc 1o | ||
Definition | df-3o 8095 | Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 3o = suc 2o | ||
Definition | df-4o 8096 | Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 4o = suc 3o | ||
Definition | df-oadd 8097* | Define the ordinal addition operation. (Contributed by NM, 3-May-1995.) |
⊢ +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) | ||
Definition | df-omul 8098* | Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.) |
⊢ ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦)) | ||
Definition | df-oexp 8099* | Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004.) |
⊢ ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1o ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦))) | ||
Theorem | 1on 8100 | Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) |
⊢ 1o ∈ On |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |