HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-8782) |
Hilbert Space Explorer
(8783-10363) |
User Sandboxes
(10364-10752) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | isoid 3901 | Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. |
         | ||
| Theorem | isocnv 3902 | Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. |
 
   | ||
| Theorem | isotr 3903 | Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. |
 
   | ||
| Theorem | isotrALT 3904 | Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. This proof is shorter than isotr 3903 in set.mm and uses fewer dummy variables, but it takes 240K vs. 207K for the web page. |
|
| ||
| Theorem | isomin 3905 |
Isomorphisms preserve minimal elements. Note that    
is Takeuti and Zaring's idiom for the initial segment
  . Proposition 6.31(1) of [TakeutiZaring] p. 33.
|
      | ||
| Theorem | isoini 3906 | Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. |
|
| ||
| Theorem | isofrlem 3907 | Lemma for isofr 3908. |
| Theorem | isofr 3908 | An isomorphism preserves foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33. |
| ||
| Theorem | isowe 3909 | An isomorphism preserves well ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33. |
| ||
| Theorem | f1oiso 3910 |
Any one-to-one onto function determines an isomorphism with an
induced relation . Proposition 6.33 of [TakeutiZaring] p. 34.
|
      
| ||
| Theorem | f1owe 3911 | Well-ordering of isomorphic relations. |
 
| ||
| Theorem | f1oweALT 3912 | Well-ordering of isomorphic relations. (This version is proved directly instead of wit the isomorphism predicate.) |
|
| ||
| Cantor's Theorem | ||
| Theorem | canth 3913 |
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 4490.
Note that must
be a set: this theorem does not hold when is
too large to be a set; see ncanth 3914 for a counterexample. (Use nex 1103
if you want the form     .)
|
 | ||
| Theorem | ncanth 3914 | Cantor's theorem fails for the universal class (which is not a set but a proper class by nvelv 2718). Specifically, the identity function maps the universe onto its power class. Compare canth 3913 that works for sets. See also the remark in ru 1941 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 3915 |
The indexed union of a set of ordinal numbers is an ordinal
number.
|
   
| ||
| Theorem | iinon 3916 |
The nonempty indexed intersection of a class of ordinal numbers
is an ordinal number.
|
 
| ||
| Transfinite recursion | ||
| Theorem | tfrlem1 3917 | A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. |
| ||
| Theorem | tfrlem2 3918 | Lemma for transfinite recursion. This provides some messy details needed to link tfrlem1 3917 into the main proof. |
| Theorem | tfrlem3 3919 |
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 3920 |
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 3921 | Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. |
| Theorem | tfrlem6 3922 | Lemma for transfinite recursion. The union of all acceptable functions is a relation. |
| Theorem | tfrlem7 3923 | Lemma for transfinite recursion. The union of all acceptable functions is a function. |
| Theorem | tfrlem8 3924 |
Lemma for transfinite recursion. The domain of is ordinal.
(The proof was shortened by Alan Sare, 11-Mar-2008.)
|
| Theorem | tfrlem9 3925 |
Lemma for transfinite recursion. Here we compute the value of
(the union of
all acceptable functions).
|
| Theorem | tfrlem10 3926 |
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 3929, 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 3927 |
Lemma for transfinite recursion. Compute the value of .
|
| Theorem | tfrlem12 3928 |
Lemma for transfinite recursion. Show is an acceptable
function.
|
| Theorem | tfrlem13 3929 |
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 3930 |
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 3931 |
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 3932 |
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 3933 |
is a function. Lemma
for tz7.44-1 3934, tz7.44-2 3935, and
tz7.44-3 3936.
|
  | ||
| Theorem | tz7.44-1 3934 |
The value of at . Part 1 of
Theorem 7.44 of
[TakeutiZaring] p. 49.
|
|
| ||
| Theorem | tz7.44-2 3935 |
The value of at a
successor ordinal. Part 2 of Theorem 7.44
of [TakeutiZaring] p. 49.
|
 | ||
| Theorem | tz7.44-3 3936 |
The value of at a
limit ordinal. Part 3 of Theorem 7.44 of
[TakeutiZaring] p. 49.
|
|
| ||
| Recursive definition generator | ||
| Syntax | crdg 3937 | Extend class notation with the recursive definition generator. |
  | ||
| Definition | df-rdg 3938 |
Define a recursive definition generator on (the class of ordinal
numbers) with characteristic function and initial value .
This combines functions in tfr1 3930 and in tz7.44-1 3934 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 4156,
from which we prove
the recursive textbook definition as theorems oa0 4161,
oasuc 4169, and
oalim 4173 (with the help of theorems rdg0 3947,
rdgsuc 3948, and rdglim 3949).
We can also restrict the operation to define otherwise recursive
functions on the natural numbers  ; see fr0t 3958 and frsuct 3959.
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 2366)
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 6309 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 6932 and integer powers df-exp 6570.
Note: We introduce |
|
| ||
| Theorem | dfrdg2 3939 | Alternate definition of a recursive definition generator. (This was the original definition, but it was later replaced with the slightly shorter df-rdg 3938.) |
|
| ||
| Theorem | rdgeq1 3940 | Equality theorem for the recursive definition generator. |
| | ||
| Theorem | rdgeq2 3941 | Equality theorem for the recursive definition generator. |
| | ||
| Theorem | hbrdg 3942 | Bound-variable hypothesis builder for the recursive definition generator. |
|
| ||