Home | Metamath
Proof Explorer Theorem List (p. 84 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 | tfrlem10 8301* | 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 8305, 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 8302* | 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 8303* | 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 8304* | 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 8305* | Lemma for transfinite recursion. Assuming ax-rep 5241, 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 8306* | Lemma for transfinite recursion. Without assuming ax-rep 5241, 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 8307* | Lemma for finite recursion. Without assuming ax-rep 5241, 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 8308 | A weak version of tfr1 8311 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ πΉ = recs(πΊ) β β’ (Fun πΉ β§ Lim dom πΉ) | ||
Theorem | tfr2a 8309 | A weak version of tfr2 8312 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ πΉ = recs(πΊ) β β’ (π΄ β dom πΉ β (πΉβπ΄) = (πΊβ(πΉ βΎ π΄))) | ||
Theorem | tfr2b 8310 | Without assuming ax-rep 5241, 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 8311 | 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 8312 | 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 8313* | 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 8314 | Alternate proof of tfr1 8311 using well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = recs(πΊ) β β’ πΉ Fn On | ||
Theorem | tfr2ALT 8315 | Alternate proof of tfr2 8312 using well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = recs(πΊ) β β’ (π΄ β On β (πΉβπ΄) = (πΊβ(πΉ βΎ π΄))) | ||
Theorem | tfr3ALT 8316* | Alternate proof of tfr3 8313 using well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = recs(πΊ) β β’ ((π΅ Fn On β§ βπ₯ β On (π΅βπ₯) = (πΊβ(π΅ βΎ π₯))) β π΅ = πΉ) | ||
Theorem | recsfnon 8317 | Strong transfinite recursion defines a function on ordinals. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ recs(πΉ) Fn On | ||
Theorem | recsval 8318 | Strong transfinite recursion in terms of all previous values. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ (π΄ β On β (recs(πΉ)βπ΄) = (πΉβ(recs(πΉ) βΎ π΄))) | ||
Theorem | tz7.44lem1 8319* | The ordered pair abstraction πΊ defined in the hypothesis is a function. This was a lemma for tz7.44-1 8320, tz7.44-2 8321, and tz7.44-3 8322 when they used that definition of πΊ. Now, they use the maps-to df-mpt 5188 idiom so this lemma is not needed anymore, but is kept in case other applications (for instance in intuitionistic set theory) need it. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
β’ πΊ = {β¨π₯, π¦β© β£ ((π₯ = β β§ π¦ = π΄) β¨ (Β¬ (π₯ = β β¨ Lim dom π₯) β§ π¦ = (π»β(π₯ββͺ dom π₯))) β¨ (Lim dom π₯ β§ π¦ = βͺ ran π₯))} β β’ Fun πΊ | ||
Theorem | tz7.44-1 8320* | 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 8321* | 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 8322* | 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 8323 | Extend class notation with the recursive definition generator, with characteristic function πΉ and initial value πΌ. |
class rec(πΉ, πΌ) | ||
Definition | df-rdg 8324* |
Define a recursive definition generator on On (the
class of ordinal
numbers) with characteristic function πΉ and initial value πΌ.
This combines functions πΉ in tfr1 8311
and πΊ in tz7.44-1 8320 into one
definition. This rather amazing operation allows 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 8285 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 8425,
from which
we prove the recursive textbook definition as Theorems oa0 8430,
oasuc 8438,
and oalim 8446 (with the help of Theorems rdg0 8335,
rdgsuc 8338, and
rdglim2a 8347). We can also restrict the rec operation to define
otherwise recursive functions on the natural numbers Ο; see
fr0g 8350 and frsuc 8351. 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 4486) 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 13836 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 14102 and integer powers df-exp 13897. 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 8325 | Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
β’ (πΉ = πΊ β rec(πΉ, π΄) = rec(πΊ, π΄)) | ||
Theorem | rdgeq2 8326 | Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
β’ (π΄ = π΅ β rec(πΉ, π΄) = rec(πΉ, π΅)) | ||
Theorem | rdgeq12 8327 | Equality theorem for the recursive definition generator. (Contributed by Scott Fenton, 28-Apr-2012.) |
β’ ((πΉ = πΊ β§ π΄ = π΅) β rec(πΉ, π΄) = rec(πΊ, π΅)) | ||
Theorem | nfrdg 8328 | 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 8329* | 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 8330 | The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.) |
β’ Fun rec(πΉ, π΄) | ||
Theorem | rdgdmlim 8331 | The domain of the recursive definition generator is a limit ordinal. (Contributed by NM, 16-Nov-2014.) |
β’ Lim dom rec(πΉ, π΄) | ||
Theorem | rdgfnon 8332 | 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 8333* | 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 8334* | 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 8335 | 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 8336 | The initial segments of the recursive definition generator are sets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
β’ (π΅ β dom rec(πΉ, π΄) β (rec(πΉ, π΄) βΎ π΅) β V) | ||
Theorem | rdgsucg 8337 | The value of the recursive definition generator at a successor. (Contributed by NM, 16-Nov-2014.) |
β’ (π΅ β dom rec(πΉ, π΄) β (rec(πΉ, π΄)βsuc π΅) = (πΉβ(rec(πΉ, π΄)βπ΅))) | ||
Theorem | rdgsuc 8338 | 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 8339 | The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 16-Nov-2014.) |
β’ ((π΅ β dom rec(πΉ, π΄) β§ Lim π΅) β (rec(πΉ, π΄)βπ΅) = βͺ (rec(πΉ, π΄) β π΅)) | ||
Theorem | rdglim 8340 | 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 8341 | The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.) |
β’ (π΄ β πΆ β (rec(πΉ, π΄)ββ ) = π΄) | ||
Theorem | rdgsucmptf 8342 | 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 8343 | 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 8342 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 8344* | This version of rdgsucmpt 8345 avoids the not-free hypothesis of rdgsucmptf 8342 by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ πΉ = rec((π₯ β V β¦ πΆ), π΄) & β’ (π¦ = π₯ β πΈ = πΆ) & β’ (π¦ = (πΉβπ΅) β πΈ = π·) β β’ ((π΅ β On β§ π· β π) β (πΉβsuc π΅) = π·) | ||
Theorem | rdgsucmpt 8345* | 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 8346* | 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 8347* | 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 | rdg0n 8348 | If π΄ is a proper class, then the recursive function generator at β is the empty set. (Contributed by Scott Fenton, 31-Oct-2024.) |
β’ (Β¬ π΄ β V β (rec(πΉ, π΄)ββ ) = β ) | ||
Theorem | frfnom 8349 | 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 8350 | The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.) |
β’ (π΄ β π΅ β ((rec(πΉ, π΄) βΎ Ο)ββ ) = π΄) | ||
Theorem | frsuc 8351 | 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 8352 | 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 8353 | 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 8352 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 | frsucmpt2 8354* | 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 8355* | 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 8356* | 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 8357* | Proposition 7.48(1) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) |
β’ πΉ Fn On β β’ (βπ₯ β On (πΉβπ₯) β (π΄ β (πΉ β π₯)) β ran πΉ β π΄) | ||
Theorem | tz7.48-3 8358* | Proposition 7.48(3) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) |
β’ πΉ Fn On β β’ (βπ₯ β On (πΉβπ₯) β (π΄ β (πΉ β π₯)) β Β¬ π΄ β V) | ||
Theorem | tz7.49 8359* | 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 8360* | 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 8361 | Extend class notation to include index-aware recursive definitions. |
class seqΟ(πΉ, πΌ) | ||
Definition | df-seqom 8362* | Index-aware recursive definitions over Ο. A mashup of df-rdg 8324 and df-seq 13836, 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 8363* | Lemma for seqΟ. Change bound variables. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
β’ rec((π β Ο, π β V β¦ β¨suc π, (ππΉπ)β©), β¨β , ( I βπΌ)β©) = rec((π β Ο, π β V β¦ β¨suc π, (ππΉπ)β©), β¨β , ( I βπΌ)β©) | ||
Theorem | seqomlem1 8364* | 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 8365* | 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 8366* | Lemma for seqΟ. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
β’ π = rec((π β Ο, π£ β V β¦ β¨suc π, (ππΉπ£)β©), β¨β , ( I βπΌ)β©) β β’ ((π β Ο)ββ ) = ( I βπΌ) | ||
Theorem | seqomlem4 8367* | 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 8368 | Equality theorem for seqΟ. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
β’ ((π΄ = π΅ β§ πΆ = π·) β seqΟ(π΄, πΆ) = seqΟ(π΅, π·)) | ||
Theorem | fnseqom 8369 | An index-aware recursive definition defines a function on the natural numbers. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
β’ πΊ = seqΟ(πΉ, πΌ) β β’ πΊ Fn Ο | ||
Theorem | seqom0g 8370 | 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 8371 | Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
β’ πΊ = seqΟ(πΉ, πΌ) β β’ (π΄ β Ο β (πΊβsuc π΄) = (π΄πΉ(πΊβπ΄))) | ||
Theorem | omsucelsucb 8372 | Membership is inherited by successors for natural numbers. (Contributed by AV, 15-Sep-2023.) |
β’ (π β Ο β suc π β suc Ο) | ||
Syntax | c1o 8373 | Extend the definition of a class to include the ordinal number 1. |
class 1o | ||
Syntax | c2o 8374 | Extend the definition of a class to include the ordinal number 2. |
class 2o | ||
Syntax | c3o 8375 | Extend the definition of a class to include the ordinal number 3. |
class 3o | ||
Syntax | c4o 8376 | Extend the definition of a class to include the ordinal number 4. |
class 4o | ||
Syntax | coa 8377 | Extend the definition of a class to include the ordinal addition operation. |
class +o | ||
Syntax | comu 8378 | Extend the definition of a class to include the ordinal multiplication operation. |
class Β·o | ||
Syntax | coe 8379 | Extend the definition of a class to include the ordinal exponentiation operation. |
class βo | ||
Definition | df-1o 8380 | Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
β’ 1o = suc β | ||
Definition | df-2o 8381 | Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
β’ 2o = suc 1o | ||
Definition | df-3o 8382 | Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ 3o = suc 2o | ||
Definition | df-4o 8383 | Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.) |
β’ 4o = suc 3o | ||
Definition | df-oadd 8384* | Define the ordinal addition operation. (Contributed by NM, 3-May-1995.) |
β’ +o = (π₯ β On, π¦ β On β¦ (rec((π§ β V β¦ suc π§), π₯)βπ¦)) | ||
Definition | df-omul 8385* | Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.) |
β’ Β·o = (π₯ β On, π¦ β On β¦ (rec((π§ β V β¦ (π§ +o π₯)), β )βπ¦)) | ||
Definition | df-oexp 8386* | Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004.) |
β’ βo = (π₯ β On, π¦ β On β¦ if(π₯ = β , (1o β π¦), (rec((π§ β V β¦ (π§ Β·o π₯)), 1o)βπ¦))) | ||
Theorem | df1o2 8387 | Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.) |
β’ 1o = {β } | ||
Theorem | df2o3 8388 | Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ 2o = {β , 1o} | ||
Theorem | df2o2 8389 | Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.) |
β’ 2o = {β , {β }} | ||
Theorem | 1oex 8390 | Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) Remove dependency on ax-10 2138, ax-11 2155, ax-12 2172, ax-un 7663. (Revised by Zhi Wang, 19-Sep-2024.) |
β’ 1o β V | ||
Theorem | 2oex 8391 | 2o is a set. (Contributed by BJ, 6-Apr-2019.) Remove dependency on ax-10 2138, ax-11 2155, ax-12 2172, ax-un 7663. (Proof shortened by Zhi Wang, 19-Sep-2024.) |
β’ 2o β V | ||
Theorem | 1on 8392 | Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) Avoid ax-un 7663. (Revised by BTernaryTau, 30-Nov-2024.) |
β’ 1o β On | ||
Theorem | 1onOLD 8393 | Obsolete version of 1on 8392 as of 30-Nov-2024. (Contributed by NM, 29-Oct-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ 1o β On | ||
Theorem | 2on 8394 | Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) Avoid ax-un 7663. (Revised by BTernaryTau, 30-Nov-2024.) |
β’ 2o β On | ||
Theorem | 2onOLD 8395 | Obsolete version of 2on 8394 as of 30-Nov-2024. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ 2o β On | ||
Theorem | 2on0 8396 | Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) |
β’ 2o β β | ||
Theorem | ord3 8397 | Ordinal 3 is an ordinal class. (Contributed by BTernaryTau, 6-Jan-2025.) |
β’ Ord 3o | ||
Theorem | 3on 8398 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
β’ 3o β On | ||
Theorem | 4on 8399 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
β’ 4o β On | ||
Theorem | 1oexOLD 8400 | Obsolete version of 1oex 8390 as of 19-Sep-2024. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ 1o β V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |