HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-8760)
|
Hilbert Space Explorer
(8761-10688)
|
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | isoini 3901 | Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. |
     
 
   
 
       | ||
| Theorem | isofrlem 3902 | Lemma for isofr 3903. |
| Theorem | isofr 3903 | An isomorphism preserves foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33. |
 | ||
| Theorem | isowe 3904 | An isomorphism preserves well ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33. |
| ||
| Theorem | f1oiso 3905 |
Any one-to-one onto function determines an isomorphism with an
induced relation . Proposition 6.33 of [TakeutiZaring] p. 34.
|
        
| ||
| Theorem | f1owe 3906 | Well-ordering of isomorphic relations. |
 
| ||
| Theorem | f1oweALT 3907 | Well-ordering of isomorphic relations. (This version is proved directly instead of wit the isomorphism predicate.) |
|
| ||
| Cantor's Theorem | ||
| Theorem | canth 3908 |
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 4480.
Note that must
be a set: this theorem does not hold when is
too large to be a set; see ncanth 3909 for a counterexample. (Use nex 1099
if you want the form     .)
|
 | ||
| Theorem | ncanth 3909 | 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 3908 that works for sets. See also the remark in ru 1934 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 3910 |
The indexed union of a set of ordinal numbers is an ordinal
number.
|
   
| ||
| Theorem | iinon 3911 |
The nonempty indexed intersection of a class of ordinal numbers
is an ordinal number.
|
  
| ||
| Transfinite recursion | ||
| Theorem | tfrlem1 3912 | A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. |
| ||
| Theorem | tfrlem2 3913 | Lemma for transfinite recursion. This provides some messy details needed to link tfrlem1 3912 into the main proof. |
| Theorem | tfrlem3 3914 |
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 3915 |
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 3916 | Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. |
| Theorem | tfrlem6 3917 | Lemma for transfinite recursion. The union of all acceptable functions is a relation. |
| Theorem | tfrlem7 3918 | Lemma for transfinite recursion. The union of all acceptable functions is a function. |
| Theorem | tfrlem8 3919 |
Lemma for transfinite recursion. The domain of is ordinal.
(The proof was shortened by Alan Sare, 11-Mar-2008.)
|
| Theorem | tfrlem9 3920 |
Lemma for transfinite recursion. Here we compute the value of
(the union of
all acceptable functions).
|
| Theorem | tfrlem10 3921 |
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 3924, 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 3922 |
Lemma for transfinite recursion. Compute the value of .
|
| Theorem | tfrlem12 3923 |
Lemma for transfinite recursion. Show is an acceptable
function.
|
| Theorem | tfrlem13 3924 |
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 3925 |
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 3926 |
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 3927 |
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 3928 |
is a function. Lemma
for tz7.44-1 3929, tz7.44-2 3930, and
tz7.44-3 3931.
|
  | ||
| Theorem | tz7.44-1 3929 |
The value of at . Part 1 of
Theorem 7.44 of
[TakeutiZaring] p. 49.
|
|
| ||
| Theorem | tz7.44-2 3930 |
The value of at a
successor ordinal. Part 2 of Theorem 7.44
of [TakeutiZaring] p. 49.
|
 | ||
| Theorem | tz7.44-3 3931 |
The value of at a
limit ordinal. Part 3 of Theorem 7.44 of
[TakeutiZaring] p. 49.
|
|
| ||
| Recursive definition generator | ||
| Syntax | crdg 3932 | Extend class notation with the recursive definition generator. |
  | ||
| Definition | df-rdg 3933 |
Define a recursive definition generator on (the class of ordinal
numbers) with characteristic function and initial value .
This combines functions in tfr1 3925 and in tz7.44-1 3929 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 4150,
from which we prove
the recursive textbook definition as theorems oa0 4155,
oasuc 4163, and
oalim 4167 (with the help of theorems rdg0 3942,
rdgsuc 3943, and rdglim 3944).
We can also restrict the operation to define otherwise recursive
functions on the natural numbers  ; see fr0t 3953 and frsuct 3954.
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 2358)
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 6264 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 6888 and integer powers df-exp 6520.
Note: We introduce |
|
| ||
| Theorem | dfrdg2 3934 | Alternate definition of a recursive definition generator. (This was the original definition, but it was later replaced with the slightly shorter df-rdg 3933.) |
|
| ||
| Theorem | rdgeq1 3935 | Equality theorem for the recursive definition generator. |
| | ||
| Theorem | rdgeq2 3936 | Equality theorem for the recursive definition generator. |
| | ||
| Theorem | hbrdg 3937 | Bound-variable hypothesis builder for the recursive definition generator. |
|
| ||
| Theorem | rdglem1 3938 | Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. |
|
| ||
| Theorem | rdglem2 3939 | Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. |
|
| ||
| Theorem | rdgfnon 3940 | The recursive definition generator is a function on ordinal numbers. |
| | ||
| Theorem | rdgval 3941 | Value of the recursive definition generator. |
| | ||