HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-8743)
|
Hilbert Space Explorer
(8744-10676)
|
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Cantor's Theorem | ||
| Theorem | canth 3901 |
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 4473.
Note that must
be a set: this theorem does not hold when is
too large to be a set; see ncanth 3902 for a counterexample. (Use nex 1100
if you want the form       .)
|
     | ||
| Theorem | ncanth 3902 | Cantor's theorem fails for the universal class (which is not a set but a proper class by nvelv 2709). Specifically, the identity function maps the universe onto its power class. Compare canth 3901 that works for sets. See also the remark in ru 1935 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 3903 |
The indexed union of a set of ordinal numbers     is an ordinal
number.
|
    
| ||
| Theorem | iinon 3904 |
The nonempty indexed intersection of a class of ordinal numbers
is an ordinal number.
|
   
| ||
| Transfinite recursion | ||
| Theorem | tfrlem1 3905 | A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. |
  
| ||
| Theorem | tfrlem2 3906 | Lemma for transfinite recursion. This provides some messy details needed to link tfrlem1 3905 into the main proof. |
| Theorem | tfrlem3 3907 |
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 3908 |
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 3909 | Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. |
| Theorem | tfrlem6 3910 | Lemma for transfinite recursion. The union of all acceptable functions is a relation. |
| Theorem | tfrlem7 3911 | Lemma for transfinite recursion. The union of all acceptable functions is a function. |
| Theorem | tfrlem8 3912 |
Lemma for transfinite recursion. The domain of is ordinal.
(The proof was shortened by Alan Sare, 11-Mar-2008.)
|
| Theorem | tfrlem9 3913 |
Lemma for transfinite recursion. Here we compute the value of
(the union of
all acceptable functions).
|
| Theorem | tfrlem10 3914 |
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 3917, 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 3915 |
Lemma for transfinite recursion. Compute the value of .
|
| Theorem | tfrlem12 3916 |
Lemma for transfinite recursion. Show is an acceptable
function.
|
| Theorem | tfrlem13 3917 |
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 3918 |
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 3919 |
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 3920 |
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 3921 |
is a function. Lemma
for tz7.44-1 3922, tz7.44-2 3923, and
tz7.44-3 3924.
|
 
  | ||
| Theorem | tz7.44-1 3922 |
The value of at . Part 1 of
Theorem 7.44 of
[TakeutiZaring] p. 49.
|
|
| ||
| Theorem | tz7.44-2 3923 |
The value of at a
successor ordinal. Part 2 of Theorem 7.44
of [TakeutiZaring] p. 49.
|
 | ||
| Theorem | tz7.44-3 3924 |
The value of at a
limit ordinal. Part 3 of Theorem 7.44 of
[TakeutiZaring] p. 49.
|
 | ||
| Recursive definition generator | ||
| Syntax | crdg 3925 | Extend class notation with the recursive definition generator. |
  | ||
| Definition | df-rdg 3926 |
Define a recursive definition generator on (the class of ordinal
numbers) with characteristic function and initial value .
This combines functions in tfr1 3918 and in tz7.44-1 3922 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 4143,
from which we prove
the recursive textbook definition as theorems oa0 4148,
oasuc 4156, and
oalim 4160 (with the help of theorems rdg0 3935,
rdgsuc 3936, and rdglim 3937).
We can also restrict the operation to define otherwise recursive
functions on the natural numbers  ; see fr0t 3946 and frsuct 3947.
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 2359)
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 6259 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 6885 and integer powers df-exp 6515.
Note: We introduce |
|
| ||
| Theorem | dfrdg2 3927 | Alternate definition of a recursive definition generator. (This was the original definition, but it was later replaced with the slightly shorter df-rdg 3926.) |
|
| ||
| Theorem | rdgeq1 3928 | Equality theorem for the recursive definition generator. |
| | ||
| Theorem | rdgeq2 3929 | Equality theorem for the recursive definition generator. |
| | ||
| Theorem | hbrdg 3930 | Bound-variable hypothesis builder for the recursive definition generator. |
|
| ||
| Theorem | rdglem1 3931 | Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. |
 | ||
| Theorem | rdglem2 3932 | Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. |
|
| ||
| Theorem | rdgfnon 3933 | The recursive definition generator is a function on ordinal numbers. |
| | ||
| Theorem | rdgval 3934 | Value of the recursive definition generator. |
|
| ||
| Theorem | rdg0 3935 | The initial value of the recursive definition generator. |
|
| ||
| Theorem | rdgsuc 3936 | The value of the recursive definition generator at a successor. |
|
| ||
| Theorem | rdglim 3937 | The value of the recursive definition generator at a limit ordinal. |
| | ||
| Theorem | rdg0t 3938 | The initial value of the recursive definition generator. |
| | ||
| Theorem | rdgsuct 3939 | The value of the recursive definition generator at a successor. |
| | ||
| Theorem | rdgsucopab 3940 | The value of the recursive definition generator at a successor (special case where the characteristic function is an ordered pair abstraction). |
 | ||