Home Metamath Proof ExplorerTheorem List (p. 65 of 328) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-21514) Hilbert Space Explorer (21515-23037) Users' Mathboxes (23038-32776)

Theorem List for Metamath Proof Explorer - 6401-6500   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremsmorndom 6401 The range of a strictly monotone ordinal function dominates the domain. (Contributed by Mario Carneiro, 13-Mar-2013.)

Theoremsmoiso2 6402 The strictly monotone ordinal functions are also epsilon isomorphisms of subclasses of . (Contributed by Mario Carneiro, 20-Mar-2013.)

2.4.21  "Strong" transfinite recursion

Syntaxcrecs 6403 Notation for a function defined by strong transfinite recursion.
recs

Definitiondf-recs 6404* Define a function recs 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 6439 for more details on why this definition is desirable. Unlike df-rdg 6439 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 6432 and recsval 6433 for the primary contract of this definition.

EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7263, zorn2 8149, and dfac8alem 7672. (Contributed by Stefan O'Rear, 18-Jan-2015.) (New usage is discouraged.)

recs

Theoremrecseq 6405 Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
recs recs

Theoremnfrecs 6406 Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
recs

Theoremtfrlem1 6407* A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremtfrlem2 6408* Lemma for transfinite recursion. This provides some messy details needed to link tfrlem1 6407 into the main proof. (Contributed by NM, 23-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremtfrlem3 6409* 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.)

Theoremtfrlem3a 6410* 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, 22-Jul-2012.)

Theoremtfrlem4 6411* 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.)

Theoremtfrlem5 6412* Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.)

Theoremrecsfval 6413* Lemma for transfinite recursion. The definition recs is the union of all acceptable functions. (Contributed by Mario Carneiro, 9-May-2015.)
recs

Theoremtfrlem6 6414* 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.)
recs

Theoremtfrlem7 6415* Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994.)
recs

Theoremtfrlem8 6416* Lemma for transfinite recursion. The domain of recs is ordinal. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Alan Sare, 11-Mar-2008.)
recs

Theoremtfrlem9 6417* Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994.)
recs recs recs

Theoremtfrlem9a 6418* Lemma for transfinite recursion. Without using ax-rep 4147, show that all the restrictions of recs are sets. (Contributed by Mario Carneiro, 16-Nov-2014.)
recs recs

Theoremtfrlem10 6419* 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, . Using this assumption we will prove facts about that will lead to a contradiction in tfrlem14 6423, thus showing the domain of recs does in fact equal . 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.)
recs recs recs       recs recs

Theoremtfrlem11 6420* Lemma for transfinite recursion. Compute the value of . (Contributed by NM, 18-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
recs recs recs       recs recs

Theoremtfrlem12 6421* Lemma for transfinite recursion. Show is an acceptable function. (Contributed by NM, 15-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
recs recs recs       recs

Theoremtfrlem13 6422* Lemma for transfinite recursion. If recs is a set function, then is acceptable, and thus a subset of recs, but is bigger than 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.)
recs

Theoremtfrlem14 6423* Lemma for transfinite recursion. Assuming ax-rep 4147, recs recs , so since recs is an ordinal, it must be equal to . (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
recs

Theoremtfrlem15 6424* Lemma for transfinite recursion. Without assuming ax-rep 4147, 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.)
recs recs

Theoremtfrlem16 6425* Lemma for finite recursion. Without assuming ax-rep 4147, 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.)
recs

Theoremtfr1a 6426 A weak version of tfr1 6429 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
recs

Theoremtfr2a 6427 A weak version of tfr2 6430 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
recs

Theoremtfr2b 6428 Without assuming ax-rep 4147, 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

Theoremtfr1 6429 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

Theoremtfr2 6430 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

Theoremtfr3 6431* 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

Theoremrecsfnon 6432 Strong transfinite recursion defines a function on ordinals. (Contributed by Stefan O'Rear, 18-Jan-2015.)
recs

Theoremrecsval 6433 Strong transfinite recursion in terms of all previous values. (Contributed by Stefan O'Rear, 18-Jan-2015.)
recs recs

Theoremtz7.44lem1 6434* is a function. Lemma for tz7.44-1 6435, tz7.44-2 6436, and tz7.44-3 6437. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)

Theoremtz7.44-1 6435* 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.)

Theoremtz7.44-2 6436* 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.)

Theoremtz7.44-3 6437* 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.)

2.4.22  Recursive definition generator

Syntaxcrdg 6438 Extend class notation with the recursive definition generator, with characteristic function and initial value .

Definitiondf-rdg 6439* Define a recursive definition generator on (the class of ordinal numbers) with characteristic function and initial value . This combines functions in tfr1 6429 and in tz7.44-1 6435 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 operation. But once we get past this hurdle, otherwise recursive definitions become relatively simple, as in for example oav 6526, from which we prove the recursive textbook definition as theorems oa0 6531, oasuc 6539, and oalim 6547 (with the help of theorems rdg0 6450, rdgsuc 6453, and rdglim2a 6462). We can also restrict the operation to define otherwise recursive functions on the natural numbers ; see fr0g 6464 and frsuc 6465. Our 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 operations (see df-if 3579) 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 11063 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 11305 and integer powers df-exp 11121.

Note: We introduce 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.)

recs

Theoremrdgeq1 6440 Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)

Theoremrdgeq2 6441 Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)

Theoremrdgeq12 6442 Equality theorem for the recursive definition generator. (Contributed by Scott Fenton, 28-Apr-2012.)

Theoremnfrdg 6443 Bound-variable hypothesis builder for the recursive definition generator. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)

Theoremrdglem1 6444* 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.)

Theoremrdgfun 6445 The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.)

Theoremrdgdmlim 6446 The domain of the recursive definition generator is a limit ordinal. (Contributed by NM, 16-Nov-2014.)

Theoremrdgfnon 6447 The recursive definition generator is a function on ordinal numbers. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)

Theoremrdgvalg 6448* Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)

Theoremrdgval 6449* Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)

Theoremrdg0 6450 The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)

Theoremrdgseg 6451 The initial segments of the recursive definition generator are sets. (Contributed by Mario Carneiro, 16-Nov-2014.)

Theoremrdgsucg 6452 The value of the recursive definition generator at a successor. (Contributed by NM, 16-Nov-2014.)

Theoremrdgsuc 6453 The value of the recursive definition generator at a successor. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)

Theoremrdglimg 6454 The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 16-Nov-2014.)

Theoremrdglim 6455 The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)

Theoremrdg0g 6456 The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.)

Theoremrdgsucmptf 6457 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.)

Theoremrdgsucmptnf 6458 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 6457 to help eliminate redundant sethood antecedents. (Contributed by NM, 22-Oct-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)

Theoremrdgsucmpt2 6459* This version of rdgsucmpt 6460 avoids the not-free hypothesis of rdgsucmptf 6457 by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015.)

Theoremrdgsucmpt 6460* 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.)

Theoremrdglim2 6461* 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.)

Theoremrdglim2a 6462* 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.)

2.4.23  Finite recursion

Theoremfrfnom 6463 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.)

Theoremfr0g 6464 The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.)

Theoremfrsuc 6465 The successor value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 16-Nov-2014.)

Theoremfrsucmpt 6466 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.)

Theoremfrsucmptn 6467 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 6466 to help eliminate redundant sethood antecedents. (Contributed by Scott Fenton, 19-Feb-2011.) (Revised by Mario Carneiro, 11-Sep-2015.)

Theoremfrsucmpt2 6468* 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.)

Theoremtz7.48lem 6469* A way of showing an ordinal function is one-to-one. (Contributed by NM, 9-Feb-1997.)

Theoremtz7.48-2 6470* Proposition 7.48(2) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) (Revised by David Abernethy, 5-May-2013.)

Theoremtz7.48-1 6471* Proposition 7.48(1) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.)

Theoremtz7.48-3 6472* Proposition 7.48(3) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.)

Theoremtz7.49 6473* Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 10-Jan-2013.)

Theoremtz7.49c 6474* Corollary of Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 19-Jan-2013.)

Syntaxcseqom 6475 Extend class notation to include index-aware recursive definitions.
seq𝜔

Definitiondf-seqom 6476* Index-aware recursive definitions over . A mashup of df-rdg 6439 and df-seq 11063, 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𝜔

Theoremseqomlem0 6477* Lemma for seq𝜔. Change bound variables. (Contributed by Stefan O'Rear, 1-Nov-2014.)

Theoremseqomlem1 6478* 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.)

Theoremseqomlem2 6479* Lemma for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.)

Theoremseqomlem3 6480* Lemma for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.)

Theoremseqomlem4 6481* Lemma for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.)

Theoremseqomeq12 6482 Equality theorem for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.)
seq𝜔 seq𝜔

Theoremfnseqom 6483 An index-aware recursive definition defines a function on the natural numbers. (Contributed by Stefan O'Rear, 1-Nov-2014.)
seq𝜔

Theoremseqom0g 6484 Value of an index-aware recursive definition at 0. (Contributed by Stefan O'Rear, 1-Nov-2014.)
seq𝜔

Theoremseqomsuc 6485 Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.)
seq𝜔

2.4.24  Abian's "most fundamental" fixed point theorem

Theoremabianfplem 6486* Lemma for abianfp 6487. We prove by transfinite induction that if has a fixed point , then its iterates also equal . This lemma is used for the "trivial" direction of the main theorem. (Contributed by NM, 4-Sep-2004.)

Theoremabianfp 6487* "A most fundamental fixed point theorem" of Alexander Abian (1923-1999), apparently proved in 1998. Let , , ,... be the iterates of . The theorem reads (using our variable names): "Let be a mapping from a set into itself. Then has a fixed point if and only if: There exists an element of such that for every ordinal , is an element of , and if is not a fixed point of then the 's are all distinct for every ordinal ." See df-rdg 6439 for the operation. The proof's key idea is to assume that does not have a fixed point, then use the Axiom of Replacement in the form of f1dmex 5767 to derive that the class of all ordinal numbers exists, contradicting onprc 4592. Our version of this theorem does not require the hypothesis that be a mapping. Reference: http://us2.metamath.org:88/abian-themostfixed.html. For an application of this theorem, see http://groups.google.com/group/sci.stat.math/msg/1737ee1133c24aeb for its use in a proof of Tarski's fixed point theorem. (Contributed by NM, 5-Sep-2004.) (Revised by David Abernethy, 19-Jun-2012.)

2.4.25  Ordinal arithmetic

Syntaxc1o 6488 Extend the definition of a class to include the ordinal number 1.

Syntaxc2o 6489 Extend the definition of a class to include the ordinal number 2.

Syntaxc3o 6490 Extend the definition of a class to include the ordinal number 3.

Syntaxc4o 6491 Extend the definition of a class to include the ordinal number 4.

Syntaxcoa 6492 Extend the definition of a class to include the ordinal addition operation.

Syntaxcomu 6493 Extend the definition of a class to include the ordinal multiplication operation.

Syntaxcoe 6494 Extend the definition of a class to include the ordinal exponentiation operation.

Definitiondf-1o 6495 Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)

Definitiondf-2o 6496 Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)

Definitiondf-3o 6497 Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-4o 6498 Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.)