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 | rankxpl 4701 | A lower bound on the rank of a cross product. |
               
| ||
| Theorem | rankxpu 4702 | An upper bound on the rank of a cross product. |
 | ||
| Theorem | rankxplim 4703 | The rank of a cross product when the rank of the union of its arguments is a limit ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxpsuc 4706 for the successor case. |
 
| ||
| Theorem | rankxplim2 4704 | If the rank of a cross product is a limit ordinal, so is the rank of the union of its arguments. |
|
| ||
| Theorem | rankxplim3 4705 | The rank of a cross product is a limit ordinal iff its union is. |
  | ||
| Theorem | rankxpsuc 4706 | The rank of a cross product when the rank of the union of its arguments is a successor ordinal. Part of Exercise 4 of [Kunen] p. 107. See rankxplim 4703 for the limit ordinal case. |
| ||
| Scott's trick; collection principle; Hilbert's epsilon | ||
| Theorem | scottex 4707 | Scott's trick collects all sets that have a certain property and are of smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of [Jech] p. 72, is a set. |
     
| ||
| Theorem | scott0 4708 |
Scott's trick collects all sets that have a certain property and are of
smallest possible rank. This theorem shows that the resulting
collection, expressed as in Equation 9.3 of [Jech] p. 72, contains at
least one representative with the property, if there is one. In other
words, the collection is empty iff no set has the property (i.e.
is empty).
|
|
| ||
| Theorem | scottexs 4709 |
Theorem scheme version of scottex 4707. The collection of all of
minimum rank such that  is true, is a set.
|
  ![]](rbrack.gif){kind=small} | ||
| Theorem | scott0s 4710 |
Theorem scheme version of scott0 4708. The collection of all of
minimum rank such that is true, is not empty iff there is
an such that
holds.
|
 | ||
| Theorem | cplem1 4711 | Lemma for the Collection Principle cp 4713. |
| Theorem | cplem2 4712 | Lemma for the Collection Principle cp 4713. |
| Theorem | cp 4713 |
Collection Principle. This remarkable theorem scheme is in effect a
very strong generalization of the Axiom of Replacement. The proof
makes use of Scott's trick scottex 4707 that collapses a proper class into
a set of minimum rank. The wff can be thought of as
 . Scheme "Collection
Principle" of [Jech] p. 72.
|
 
| ||
| Theorem | bnd 4714 |
A very strong generalization of the Axiom of Replacement (compare
zfrep6 3616), derived from the Collection Principle cp 4713.
Its strength
lies in the rather profound fact that does not have to
be a "function-like" wff, as it does in the standard Axiom of
Replacement. This theorem is sometimes called the Boundedness Axiom.
|
|
| ||
| Theorem | bnd2 4715 |
A variant of the Boundedness Axiom bnd 4714 that picks a subset out
of a possibly proper class in which a property is true.
|
|
| ||
| Theorem | kardex 4716 |
The collection of all sets equinumerous to a set and having least
possible rank is a set. This is the part of the justification of the
definition of kard of [Enderton] p.
222.
|
| ||
| Theorem | karden 4717 |
If we allow the Axiom of Regularity, we can avoid the Axiom of Choice by
defining the cardinal number of a set as the set of all sets
equinumerous to it and having least possible rank. This theorem proves
the equinumerosity relationship for this definition (compare carden 4822).
The hypotheses correspond to the definition of kard of [Enderton] p. 222
(which we don't define separately since currently we do not use it
elsewhere). This theorem along with kardex 4716 justify the definition of
kard. The restriction to least rank prevents the proper class that
would result from .
|
| ||
| Theorem | htalem 4718 |
Lemma for defining an emulation of Hilbert's epsilon. Hilbert's epsilon
is described at http://plato.stanford.edu/entries/epsilon-calculus/.
This theorem is equivalent to Hilbert's "transfinite axiom,"
described
on that page, with the additional  
antecedent. The
element
is the epsilon
that the theorem emulates.
|
| Theorem | hta 4719 |
A ZFC emulation of Hilbert's transfinite axiom. The set has the
properties of Hilbert's epsilon, except that it also depends on a
well-ordering .
This theorem arose from discussions with Raph
Levien on 5-Mar-2004 about translating the HOL proof language, which
uses Hilbert's epsilon. See http://ghilbert.org/choice.txt and
http://us.metamath.org/downloads/megillaward2004.pdf.
Hilbert's epsilon is described at
http://plato.stanford.edu/entries/epsilon-calculus/.
This theorem
differs from Hilbert's transfinite axiom described on that page in
that it requires
If a well-ordering For a version of this theorem scheme using class (meta)variables instead of wff (meta)variables, see htalem 4718. |
| ||
| Axiom of Choice equivalents | ||
| Theorem | aceq1 4720 | Equivalence of two versions of the Axiom of Choice ax-ac 4735. The proof uses neither AC nor the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. |
 
| ||
| Theorem | aceq0 4721 | Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. The right-hand side is our original ax-ac 4735. |
| ||
| Theorem | aceq2 4722 | Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. |
|
| ||
| Theorem | aceq3lem 4723 | Lemma for aceq3 4724. |
| Theorem | aceq3 4724 | Equivalence of two versions of the Axiom of Choice. The left-hand side is similar to the Axiom of Choice (first form) of [Enderton] p. 49. The right-hand side is the Axiom of Choice of [TakeutiZaring] p. 83. The proof does not depend on AC. |
 
| ||
| Theorem | aceq4 4725 | Equivalence of two versions of the Axiom of Choice. The left-hand side is similar to the Axiom of Choice (first form) of [Enderton] p. 49. The right-hand side is Axiom AC of [BellMachover] p. 488. The proof does not depend on AC. |
|
| ||
| Theorem | aceq5lem1 4726 | Lemma for aceq5 4731. |
| Theorem | aceq5lem2 4727 | Lemma for aceq5 4731. |
| Theorem | aceq5lem3 4728 | Lemma for aceq5 4731. |
| Theorem | aceq5lem4 4729 | Lemma for aceq5 4731. |
| Theorem | aceq5lem5 4730 | Lemma for aceq5 4731. |
| Theorem | aceq5 4731 | Equivalence of two versions of the Axiom of Choice. The left-hand side is similar to the Axiom of Choice (first form) of [Enderton] p. 49. The right-hand side is Theorem 6M(4) of [Enderton] p. 151 and asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. The proof does not depend on AC. |
| ||
| Theorem | aceq6a 4732 | Our Axiom of Choice (in the form of ac3 4738) implies the Axiom of Choice (first form) of [Enderton] p. 49. The proof uses neither AC nor the Axiom of Regularity. See aceq6b 4733 for the converse (which does use the Axiom of Regularity). |
|
| ||
| Theorem | aceq6b 4733 | Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 4738). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 4589 and preleq 4594 that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see aceq6a 4732.) |
|
| ||
| Theorem | aceq7 4734 | Equivalence of the Axiom of Choice (first form) of [Enderton] p. 49 and our Axiom of Choice (in the form of ac2 4737). The proof does not depend AC on but does depend on the Axiom of Regularity. |
|
| ||
| ZFC Set Theory - add the Axiom of Choice | ||
| Introduce the Axiom of Choice | ||
| Axiom | ax-ac 4735 |
Axiom of Choice. The Axiom of Choice (AC) is usually considered an
extension of ZF set theory rather than a proper part of it. It is
sometimes considered philosophically controversial because it asserts
the existence of a set without telling us what the set is. ZF set
theory that includes AC is called ZFC.
The unpublished version given here says that given any set This version was specifically crafted to be short when expanded to primitives. Kurt Maes' 5-quantifier version ackm 4773 is slightly shorter when the biconditional of ax-ac 4735 is expanded into implication and negation. Standard textbook versions of AC are derived as ac8 4754, ac5 4743, and ac7 4739. The Axiom of Regularity ax-reg 4584 (among others) is used to derive our version from the standard ones; this reverse derivation is shown as theorem aceq6b 4733. Equivalents to AC are the well-ordering theorem weth 4778 and Zorn's lemma zorn 4788. See ac4 4741 for comments about stronger versions of AC. |
|
| ||
| Theorem | axac 4736 | Axiom of Choice expressed with fewest number of different variables. The penultimate step shows the logical equivalence to ax-ac 4735. |
|
| ||
| Theorem | ac2 4737 | Axiom of Choice equivalent. By using restricted quantifiers, we can express the Axiom of Choice with a single conjunction. (If you want to figure it out, the rewritten equivalent ac3 4738 is easier to understand.) Note: aceq0 4721 shows the logical equivalence to ax-ac 4735. |
|
| ||
| Theorem | ac3 4738 |
Axiom of Choice using abbreviations. The logical equivalence to
ax-ac 4735 can be established by chaining aceq0 4721 and aceq2 4722. A standard
textbook version of AC is derived from this one in aceq6a 4732, and this
version of AC is derived from the textbook version in aceq6b 4733.
The following sketch will help you understand this version of the axiom.
Given any set
For example, suppose
|
