HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-8757) |
Hilbert Space Explorer
(8758-10338) |
User Sandboxes
(10339-10701) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | isofr 3901 | An isomorphism preserves foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33. |
      
    
 | ||
| Theorem | isowe 3902 | An isomorphism preserves well ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33. |
| ||
| Theorem | f1oiso 3903 |
Any one-to-one onto function determines an isomorphism with an
induced relation . Proposition 6.33 of [TakeutiZaring] p. 34.
|
            
 
| ||
| Theorem | f1owe 3904 | Well-ordering of isomorphic relations. |
 
| ||
| Theorem | f1oweALT 3905 | Well-ordering of isomorphic relations. (This version is proved directly instead of wit the isomorphism predicate.) |
|
| ||
| Cantor's Theorem | ||
| Theorem | canth 3906 |
No set is equinumerous
to its power set (Cantor's theorem), i.e.
no function can map it onto its power set. Compare Theorem 6B(b)
of [Enderton] p. 132. For the
equinumerosity version, see canth2 4479.
Note that must
be a set: this theorem does not hold when is
too large to be a set; see ncanth 3907 for a counterexample. (Use nex 1101
if you want the form     .)
|
 | ||
| Theorem | ncanth 3907 | Cantor's theorem fails for the universal class (which is not a set but a proper class by nvelv 2712). Specifically, the identity function maps the universe onto its power class. Compare canth 3906 that works for sets. See also the remark in ru 1937 about NF, in which Cantor's theorem fails for sets that are "too large." This theorem gives some intuition behind that failure: in NF the universal class is a set, and it equals its own power set. |
 | ||
| Miscellaneous ordinal theorems (that depend on functions and relations) | ||
| Theorem | iunon 3908 |
The indexed union of a set of ordinal numbers is an ordinal
number.
|
   
| ||
| Theorem | iinon 3909 |
The nonempty indexed intersection of a class of ordinal numbers
is an ordinal number.
|
  
| ||
| Transfinite recursion | ||
| Theorem | tfrlem1 3910 | A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. |
| ||
| Theorem | tfrlem2 3911 | Lemma for transfinite recursion. This provides some messy details needed to link tfrlem1 3910 into the main proof. |
| Theorem | tfrlem3 3912 |
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.
|
| Theorem | tfrlem4 3913 |
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.
|
| Theorem | tfrlem5 3914 | Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. |
| Theorem | tfrlem6 3915 | Lemma for transfinite recursion. The union of all acceptable functions is a relation. |
| Theorem | tfrlem7 3916 | Lemma for transfinite recursion. The union of all acceptable functions is a function. |
| Theorem | tfrlem8 3917 |
Lemma for transfinite recursion. The domain of is ordinal.
(The proof was shortened by Alan Sare, 11-Mar-2008.)
|
| Theorem | tfrlem9 3918 |
Lemma for transfinite recursion. Here we compute the value of
(the union of
all acceptable functions).
|
| Theorem | tfrlem10 3919 |
Lemma for transfinite recursion. We define class  by extending
with one
ordered pair. We will assume, falsely, that domain of
is a member
of, and thus not equal to, . Using this
assumption we will prove facts about that will lead to a
contradiction in tfrlem13 3922, thus showing the domain of does in
fact equal .
Here we show (under the false assumption) that
is a function
extending the domain of by one. (The proof
was shortened by Alan Sare, 20-Feb-2008.)
|
| Theorem | tfrlem11 3920 |
Lemma for transfinite recursion. Compute the value of .
|
| Theorem | tfrlem12 3921 |
Lemma for transfinite recursion. Show is an acceptable
function.
|
| Theorem | tfrlem13 3922 |
Lemma for transfinite recursion. If 
is in , then
is
acceptable, and thus a subset of , but
is
bigger than . This is a
contradiction, so
must be
.
|
| Theorem | tfr1 3923 |
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
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.
|
 | ||
| Theorem | tfr2 3924 |
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
.
|
|
| ||
| Theorem | tfr3 3925 |
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 .
|
|
| ||
| Theorem | tz7.44lem1 3926 |
is a function. Lemma
for tz7.44-1 3927, tz7.44-2 3928, and
tz7.44-3 3929.
|
  | ||
| Theorem | tz7.44-1 3927 |
The value of at . Part 1 of
Theorem 7.44 of
[TakeutiZaring] p. 49.
|
|
| ||
| Theorem | tz7.44-2 3928 |
The value of at a
successor ordinal. Part 2 of Theorem 7.44
of [TakeutiZaring] p. 49.
|
 | ||
| Theorem | tz7.44-3 3929 |
The value of at a
limit ordinal. Part 3 of Theorem 7.44 of
[TakeutiZaring] p. 49.
|
 | ||
| Recursive definition generator | ||
| Syntax | crdg 3930 | Extend class notation with the recursive definition generator. |
  | ||
| Definition | df-rdg 3931 |
Define a recursive definition generator on (the class of ordinal
numbers) with characteristic function and initial value .
This combines functions in tfr1 3923 and in tz7.44-1 3927 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 4149,
from which we prove
the recursive textbook definition as theorems oa0 4154,
oasuc 4162, and
oalim 4166 (with the help of theorems rdg0 3940,
rdgsuc 3941, and rdglim 3942).
We can also restrict the operation to define otherwise recursive
functions on the natural numbers  ; see fr0t 3951 and frsuct 3952.
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  operators (see df-if 2361)
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-seq1 6283 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 6903 and integer powers df-exp 6542.
Note: We introduce |
|
| ||
| Theorem | dfrdg2 3932 | Alternate definition of a recursive definition generator. (This was the original definition, but it was later replaced with the slightly shorter df-rdg 3931.) |
|
| ||
| Theorem | rdgeq1 3933 | Equality theorem for the recursive definition generator. |
| | ||
| Theorem | rdgeq2 3934 | Equality theorem for the recursive definition generator. |
| | ||
| Theorem | hbrdg 3935 | Bound-variable hypothesis builder for the recursive definition generator. |
|
| ||
| Theorem | rdglem1 3936 | Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. |
|
| ||
| Theorem | rdglem2 3937 | Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. |
|
| ||
| Theorem | rdgfnon 3938 | The recursive definition generator is a function on ordinal numbers. |
| | ||
| Theorem | rdgval 3939 | Value of the recursive definition generator. |
|
| ||