Home(or GIF version for IE).
| Home |
Metamath Proof Explorer | < Previous Next > |
| Bad symbols?
Use Firefox (or GIF version for IE). |
| 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. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ((A × B) ≠ ∅ → (rank ‘(A ∪ B)) ⊆ (rank ‘(A × B))) | ||
| Theorem | rankxpu 4702 | An upper bound on the rank of a cross product. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (rank ‘(A × B)) ⊆ suc suc (rank ‘(A ∪ B)) | ||
| 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. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ((Lim (rank ‘(A ∪ B)) ⋀ (A × B) ≠ ∅) → (rank ‘(A × B)) = (rank ‘(A ∪ B))) | ||
| Theorem | rankxplim2 4704 | If the rank of a cross product is a limit ordinal, so is the rank of the union of its arguments. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (Lim (rank ‘(A × B)) → Lim (rank ‘(A ∪ B))) | ||
| Theorem | rankxplim3 4705 | The rank of a cross product is a limit ordinal iff its union is. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (Lim (rank ‘(A × B)) ↔ Lim ∪(rank ‘(A × B))) | ||
| 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. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (((rank ‘(A ∪ B)) = suc C ⋀ (A × B) ≠ ∅) → (rank ‘(A × B)) = suc suc (rank ‘(A ∪ B))) | ||
| 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. |
| ⊢ {x ∈ A∣∀y ∈ A (rank ‘x) ⊆ (rank ‘y)} ∈ V | ||
| 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. A is empty). |
| ⊢ (A = ∅ ↔ {x ∈ A∣∀y ∈ A (rank ‘x) ⊆ (rank ‘y)} = ∅) | ||
| Theorem | scottexs 4709 | Theorem scheme version of scottex 4707. The collection of all x of minimum rank such that φ(x) is true, is a set. |
| ⊢ {x∣(φ ⋀ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ∈ V | ||
| Theorem | scott0s 4710 | Theorem scheme version of scott0 4708. The collection of all x of minimum rank such that φ(x) is true, is not empty iff there is an x such that φ(x) holds. |
| ⊢ (∃xφ ↔ {x∣(φ ⋀ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ≠ ∅) | ||
| 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 φ(x, y). Scheme "Collection Principle" of [Jech] p. 72. |
| ⊢ ∃w∀x ∈ z (∃yφ → ∃y ∈ w φ) | ||
| 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 φ(x, y) 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. |
| ⊢ (∀x ∈ z ∃yφ → ∃w∀x ∈ z ∃y ∈ w φ) | ||
| Theorem | bnd2 4715 | A variant of the Boundedness Axiom bnd 4714 that picks a subset z out of a possibly proper class B in which a property is true. |
| ⊢ A ∈ V ⇒ ⊢ (∀x ∈ A ∃y ∈ B φ → ∃z(z ⊆ B ⋀ ∀x ∈ A ∃y ∈ z φ)) | ||
| Theorem | kardex 4716 | The collection of all sets equinumerous to a set A and having least possible rank is a set. This is the part of the justification of the definition of kard of [Enderton] p. 222. |
| ⊢ {x∣(x ≈ A ⋀ ∀y(y ≈ A → (rank ‘x) ⊆ (rank ‘y)))} ∈ V | ||
| 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 {x∣x ≈ A}. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ C = {x∣(x ≈ A ⋀ ∀y(y ≈ A → (rank ‘x) ⊆ (rank ‘y)))} & ⊢ D = {x∣(x ≈ B ⋀ ∀y(y ≈ B → (rank ‘x) ⊆ (rank ‘y)))} ⇒ ⊢ (C = D ↔ A ≈ B) | ||
| 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 R We A antecedent. The element B is the epsilon that the theorem emulates. |
| Theorem | hta 4719 |
A ZFC emulation of Hilbert's transfinite axiom. The set B has the
properties of Hilbert's epsilon, except that it also depends on a
well-ordering R. 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 R We A as an antecedent. Class A collects the sets of least rank for which φ(x) is true. Class B, which emulates the epsilon, is the minimum element in a well-ordering R on A. If a well-ordering R on A can be expressed in a closed form, as might be the case if we are working with say natural numbers, we can eliminate the antecedent with modus ponens, giving us the exact equivalent of Hilbert's transfinite axiom. Otherwise, we replace R with a dummy set variable, say w, and attach w We A as an antecedent in each step of the ZFC version of the HOL proof until the epsilon is eliminated. At that point, B (which will have w as a free variable) will no longer be present, and we can eliminate w We A by applying 19.23aiv 1293 and weth 4778, using scottexs 4709 to establish the existence of A. For a version of this theorem scheme using class (meta)variables instead of wff (meta)variables, see htalem 4718. |
| ⊢ A = {x∣(φ ⋀ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} & ⊢ B = ∪{x ∈ A∣∀y ∈ A ¬ yRx} ⇒ ⊢ (R We A → (φ → [B / x]φ)) | ||
| 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. |
| ⊢ (∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ⋀ v ∈ u) ↔ ∃y∀z∀w((z ∈ w ⋀ w ∈ x) → ∃x∀z(∃x((z ∈ w ⋀ w ∈ x) ⋀ (z ∈ x ⋀ x ∈ y)) ↔ z = x))) | ||
| 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. |
| ⊢ (∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ⋀ v ∈ u) ↔ ∃y∀z∀w((z ∈ w ⋀ w ∈ x) → ∃v∀u(∃t((u ∈ w ⋀ w ∈ t) ⋀ (u ∈ t ⋀ t ∈ y)) ↔ u = v))) | ||
| Theorem | aceq2 4722 | Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. |
| ⊢ (∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ⋀ v ∈ u) ↔ ∃y∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v))) | ||
| 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. |
| ⊢ (∀x∃f(f ⊆ x ⋀ f Fn dom x) ↔ ∀x∃f∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z)) | ||
| 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. |
| ⊢ (∀x∃f(f ⊆ x ⋀ f Fn dom x) ↔ ∀x∃f(f Fn x ⋀ ∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z))) | ||
| 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. |
| ⊢ (∀x∃f(f ⊆ x ⋀ f Fn dom x) ↔ ∀x((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y))) | ||
| 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). |
| ⊢ (∀x∃y∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v)) → ∀x∃f(f ⊆ x ⋀ f Fn dom x)) | ||
| 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.) |
| ⊢ (∀x∃f(f ⊆ x ⋀ f Fn dom x) → ∀x∃y∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v))) | ||
| 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. |
| ⊢ (∀x∃f(f ⊆ x ⋀ f Fn dom x) ↔ ∀x∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ⋀ v ∈ u)) | ||
| 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 x, there exists a y that is a collection of unordered pairs, one pair for each non-empty member of x. One entry in the pair is the member of x, and the other entry is some arbitrary member of that member of x. See the rewritten version ac3 4738 for a more detailed explanation. 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. |
| ⊢ ∃y∀z∀w((z ∈ w ⋀ w ∈ x) → ∃v∀u(∃t((u ∈ w ⋀ w ∈ t) ⋀ (u ∈ t ⋀ t ∈ y)) ↔ u = v)) | ||
| Theorem | axac 4736 | Axiom of Choice expressed with fewest number of different variables. The penultimate step shows the logical equivalence to ax-ac 4735. |
| ⊢ ∃x∀y∀z((y ∈ z ⋀ z ∈ w) → ∃w∀y(∃w((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ x)) ↔ y = w)) | ||
| 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. |
| ⊢ ∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ⋀ v ∈ u) | ||
| 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 x, the axiom says that there exists a y that is a collection of unordered pairs, one pair for each non-empty member of x. One entry in the pair is the member of x, and the other entry is some arbitrary member of that member of x. Using the Axiom of Regularity, we can show that y is really a set of ordered pairs, very similar to the ordered pair construction opthreg 4595. The key theorem for this (used in the proof of aceq6b 4733) is preleq 4594. With this modified definition of ordered pair, it can be seen that y is actually a choice function on the members of x. For example, suppose x = {{1, 2}, {1, 3}, {2, 3}}. Take y = {{{1, 2}, 1}, {{1, 3}, 1}, {{2, 3}, 2}}. For the member (of x) z = {1, 2}, the only assignment to w and v that satisfies the axiom is w = 1 and v = {{1, 2}, 1}, so there is exactly one w as required. We verify the other two members of x similarly. Thus y satisfies the axiom. Using our modified ordered pair definition, it is easy to see that y is the choice function {⟨{1, 2}, 1⟩, ⟨{1, 3}, 1⟩, ⟨{2, 3}, 2⟩}. Of course other choices for y will also satisfy the axiom, for example y = {{{1, 2}, 2}, {{1, 3}, 1}, {{2, 3}, 3}}. What AC tells us is that there exists at least one such y, but it doesn't tell us which one. |
| ⊢ ∃y∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v)) | ||
| Theorem | ac7 4739 | An Axiom of Choice equivalent similar to the Axiom of Choice (first form) of [Enderton] p. 49. |
| ⊢ ∃f(f ⊆ x ⋀ f Fn dom x) | ||
| Theorem | ac7g 4740 | An Axiom of Choice equivalent similar to the Axiom of Choice (first form) of [Enderton] p. 49. |
| ⊢ (R ∈ A → ∃f(f ⊆ R ⋀ f Fn dom R)) | ||
| Theorem | ac4 4741 |
Equivalent of Axiom of Choice. We do not insist that f be a
function. However, theorem ac5 4743, derived from this one, shows that
this form of the axiom does imply that at least one such set f whose
existence we assert is in fact a function. Axiom of Choice of
[TakeutiZaring] p. 83.
Takeuti and Zaring call this "weak choice" in contrast to "strong choice" ∃F∀z(z ≠ ∅ → (F ‘z) ∈ z), which asserts the existence of a universal choice function but requires second-order quantification on (proper) class variable F and thus cannot be expressed in our first-order formalization. However, it has been shown that ZF plus strong choice is a conservative extension of ZF plus weak choice. See Ulrich Felgner, "Comparison of the axioms of local and universal choice," Fundamenta Mathematica, 71, 43-62 (1971). Weak choice can be strengthened in a different direction to choose from a collection of proper classes; see ac6s5 4753. |
| ⊢ ∃f∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) | ||
| Theorem | ac4c 4742 | Equivalent of Axiom of Choice (class version) |
| ⊢ A ∈ V ⇒ ⊢ ∃f∀x ∈ A (x ≠ ∅ → (f ‘x) ∈ x) | ||
| Theorem | ac5 4743 | An Axiom of Choice equivalent: there exists a function f (called a choice function) with domain A that maps each nonempty member of the domain to an element of that member. Axiom AC of [BellMachover] p. 488. Note that the assertion that f be a function is not necessary; see ac4 4741. |
| ⊢ A ∈ V ⇒ ⊢ ∃f(f Fn A ⋀ ∀x ∈ A (x ≠ ∅ → (f ‘x) ∈ x)) | ||
| Theorem | ac5b 4744 | Equivalent of Axiom of Choice. |
| ⊢ A ∈ V ⇒ ⊢ (∀x ∈ A x ≠ ∅ → ∃f(f:A–→∪A ⋀ ∀x ∈ A (f ‘x) ∈ x)) | ||
| Theorem | ac6lem 4745 | Lemma for ac6 4746. |
| Theorem | ac6 4746 | Equivalent of Axiom of Choice. This is useful for proving that there exists, for example, a sequence mapping natural numbers to members of a large set B, where φ depends on x (the natural number) and y (to specify a member of B). A stronger version of this theorem, ac6s 4747, allows B to be a proper class. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ (y = (f ‘x) → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ)) | ||
| Theorem | ac6s 4747 | Equivalent of Axiom of Choice. Using the Boundedness Axiom bnd2 4715, we derive this strong version of ac6 4746 that doesn't require B to be a set. |
| ⊢ A ∈ V & ⊢ (y = (f ‘x) → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ)) | ||
| Theorem | ac6n 4748 | Equivalent of Axiom of Choice. Contrapositive of ac6s 4747. |
| ⊢ A ∈ V & ⊢ (y = (f ‘x) → (φ ↔ ψ)) ⇒ ⊢ (∀f(f:A–→B → ∃x ∈ A ψ) → ∃x ∈ A ∀y ∈ B φ) | ||
| Theorem | ac6s2 4749 | Generalization of the Axiom of Choice to classes. Slightly strengthened version of ac6s3 4750. |
| ⊢ A ∈ V & ⊢ (y = (f ‘x) → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ A ∃yφ → ∃f(f Fn A ⋀ ∀x ∈ A ψ)) | ||
| Theorem | ac6s3 4750 | Generalization of the Axiom of Choice to classes. Theorem 10.46 of [TakeutiZaring] p. 97. |
| ⊢ A ∈ V & ⊢ (y = (f ‘x) → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ A ∃yφ → ∃f∀x ∈ A ψ) | ||
| Theorem | ac6sf 4751 | Version of ac6 4746 with bound-variable hypothesis. |
| ⊢ (ψ → ∀yψ) & ⊢ A ∈ V & ⊢ (y = (f ‘x) → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ)) | ||
| Theorem | ac6s4 4752 | Generalization of the Axiom of Choice to proper classes. B is a collection B(x) of nonempty, possible proper classes. |
| ⊢ A ∈ V ⇒ ⊢ (∀x ∈ A B ≠ ∅ → ∃f(f Fn A ⋀ ∀x ∈ A (f ‘x) ∈ B)) | ||
| Theorem | ac6s5 4753 | Generalization of the Axiom of Choice to proper classes. B is a collection B(x) of nonempty, possible proper classes. Remark after Theorem 10.46 of [TakeutiZaring] p. 98. |
| ⊢ A ∈ V ⇒ ⊢ (∀x ∈ A B ≠ ∅ → ∃f∀x ∈ A (f ‘x) ∈ B) | ||
| Theorem | ac8 4754 | An Axiom of Choice equivalent. Given a family x of mutually disjoint nonempty sets, there exists a set y containing exactly one member from each set in the family. Theorem 6M(4) of [Enderton] p. 151. |
| ⊢ ((∀z ∈ x z ≠ ∅ ⋀ ∀z ∈ x ∀w ∈ x (z ≠ w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)) | ||
| Theorem | ac9s 4755 | An Axiom of Choice equivalent: the infinite Cartesian product of nonempty classes is nonempty. Axiom of Choice (second form) of [Enderton] p. 55 and its converse. This is a stronger version of the axiom in Enderton, with no existence requirement for the family of classes B(x) (achieved via the Collection Principle cp 4713). |
| ⊢ A ∈ V ⇒ ⊢ (∀x ∈ A B ≠ ∅ ↔ Xx ∈ A B ≠ ∅) | ||
| Theorem | kmlem1 4756 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2. |
| Theorem | kmlem2 4757 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. |
| Theorem | kmlem3 4758 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. The right-hand side is part of the hypothesis of 4. |
| Theorem | kmlem4 4759 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. |
| Theorem | kmlem5 4760 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. |
| Theorem | kmlem6 4761 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. |
| Theorem | kmlem7 4762 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. |
| Theorem | kmlem8 4763 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. |
| Theorem | kmlem9 4764 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. |
| Theorem | kmlem10 4765 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. |
| Theorem | kmlem11 4766 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. |
| Theorem | kmlem12 4767 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. |
| Theorem | kmlem13 4768 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. |
| Theorem | kmlem14 4769 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. |
| Theorem | kmlem15 4770 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. |
| Theorem | kmlem16 4771 | Lemma for 5-quantifier AC of Kurt Maes, Th. 4 5 <=> 4. |
| Theorem | aceqkm 4772 | Equivalence of the Axiom of Choice (first form) of [Enderton] p. 49 and Maes' AC ackm 4773. The proof consists of lemmas kmlem1 4756 through kmlem16 4771 and this final theorem. AC is not used for the proof. Note: bypassing the first step (i.e. replacing aceq5 4731 with pm4.2 170) establishes the AC equivalence shown by Mae's writeup. The left-hand-side AC shown here was chosen because it is shorter to display. |
| ⊢ (∀x∃f(f ⊆ x ⋀ f Fn dom x) ↔ ∀x∃y∀z∃v∀u((y ∈ x ⋀ (z ∈ y → ((v ∈ x ⋀ ¬ y = v) ⋀ z ∈ v))) ⋁ (¬ y ∈ x ⋀ (z ∈ x → ((v ∈ z ⋀ v ∈ y) ⋀ ((u ∈ z ⋀ u ∈ y) → u = v)))))) | ||
| Theorem | ackm 4773 |
A remarkable equivalent to the Axiom of Choice that has only 5
quantifiers (when expanded to ∈, = primitives in prenex form),
discovered and proved by Kurt Maes. This establishes a new record,
reducing from 6 to 5 the largest number of quantified variables needed
by any ZFC axiom. The ZF-equivalence to AC is shown by theorem
aceqkm 4772. Maes found this version of AC in April,
2004 (replacing a
longer version, also with 5 quantifiers, that he found in November,
2003). See Kurt Maes, "A 5-quantifier (∈,=)-expression
ZF-equivalent to the Axiom of Choice"
(http://arxiv.org/PS_cache/arxiv/pdf/0705/0705.3162v1.pdf).
The original FOM posts are: http://www.cs.nyu.edu/pipermail/fom/2003-November/007631.html http://www.cs.nyu.edu/pipermail/fom/2003-November/007641.html. |
| ⊢ ∀x∃y∀z∃v∀u((y ∈ x ⋀ (z ∈ y → ((v ∈ x ⋀ ¬ y = v) ⋀ z ∈ v))) ⋁ (¬ y ∈ x ⋀ (z ∈ x → ((v ∈ z ⋀ v ∈ y) ⋀ ((u ∈ z ⋀ u ∈ y) → u = v))))) | ||
| AC equivalents: well ordering, Zorn's lemma | ||
| Theorem | numthlem 4774 | Lemma for numth 4775. |
| Theorem | numth 4775 | Numeration theorem: every set can be put into one-to-one correspondence with some ordinal (using AC). Theorem 10.3 of [TakeutiZaring] p. 84. |
| ⊢ A ∈ V ⇒ ⊢ ∃x ∈ On ∃f f:x–1-1-onto→A | ||
| Theorem | numth2 4776 | Numeration theorem: any set is equinumerous to some ordinal (using AC). Theorem 10.3 of [TakeutiZaring] p. 84. |
| ⊢ ∃x ∈ On x ≈ A | ||
| Theorem | numthcor 4777 | Any set is strictly dominated by some ordinal. |
| ⊢ (A ∈ B → ∃x ∈ On A ≺ x) | ||
| Theorem | weth 4778 | Well-ordering theorem: any set A can be well-ordered. This is an equivalent of the Axiom of Choice. Theorem 6 of [Suppes] p. 242. First proved by Ernst Zermelo (the "Z" in ZFC) in 1904. |
| ⊢ A ∈ V ⇒ ⊢ ∃x x We A | ||
| Theorem | zorn2lem1 4779 | Lemma for zorn2 4787. |
| Theorem | zorn2lem2 4780 | Lemma for zorn2 4787. |
| Theorem | zorn2lem3 4781 | Lemma for zorn2 4787. |
| Theorem | zorn2lem4 4782 | Lemma for zorn2 4787. |
| Theorem | zorn2lem5 4783 | Lemma for zorn2 4787. |
| Theorem | zorn2lem6 4784 | Lemma for zorn2 4787. |
| Theorem | zorn2lem7 4785 | Lemma for zorn2 4787. |
| Theorem | zornlem 4786 | Lemma for zorn 4788. |
| Theorem | zorn2 4787 | Zorn's Lemma of [Monk1] p. 117. This theorem is equivalent to the Axiom of Choice and states that every partially ordered set A (with an ordering relation R) in which every totally ordered subset has an upper bound, contains at least one maximal element. The main proof consists of lemmas zorn2lem1 4779 through zorn2lem7 4785; this final piece mainly changes bound variables to eliminate the hypotheses of zorn2lem7 4785. |
| ⊢ A ∈ V ⇒ ⊢ ((R Po A ⋀ ∀w((w ⊆ A ⋀ R Or w) → ∃x ∈ A ∀z ∈ w (zRx ⋁ z = x))) → ∃x ∈ A ∀y ∈ A ¬ xRy) | ||
| Theorem | zorn 4788 | Zorn's Lemma. If the union of every chain (with respect to inclusion) in a set belongs to the set, then the set contains a maximal element. This theorem is equivalent to the Axiom of Choice. Theorem 6M of [Enderton] p. 151. See zorn2 4787 for a version with general partial orderings. |
| ⊢ A ∈ V ⇒ ⊢ (∀z((z ⊆ A ⋀ ∀x ∈ z ∀y ∈ z (x ⊆ y ⋁ y ⊆ x)) → ∪z ∈ A) → ∃x ∈ A ∀y ∈ A ¬ x ⊂ y) | ||
| Theorem | fodom 4789 | An onto function implies dominance of domain over range. Lemma 10.20 of [Kunen] p. 30. This theorem uses the Axiom of Choice ac7g 4740. AC is not needed for finite sets - see fodomfi 4557. |
| ⊢ A ∈ V ⇒ ⊢ (F:A–onto→B → B ≼ A) | ||
| Theorem | fodomg 4790 | An onto function implies dominance of domain over range. |
| ⊢ (A ∈ C → (F:A–onto→B → B ≼ A)) | ||
| Theorem | fodomb 4791 | Equivalence of an onto mapping and dominance for a non-empty set. Proposition 10.35 of [TakeutiZaring] p. 93. |
| ⊢ A ∈ V ⇒ ⊢ ((A ≠ ∅ ⋀ ∃f f:A–onto→B) ↔ (∅ ≺ B ⋀ B ≼ A)) | ||
| Theorem | brdom3 4792 | Equivalence to a dominance relation. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A ≼ B ↔ ∃f(∀x∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx)) | ||
| Theorem | brdom5 4793 | An equivalence to a dominance relation. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A ≼ B ↔ ∃f(∀x ∈ B ∃*y xfy ⋀ ∀x ∈ A ∃y ∈ B yfx)) | ||
| Theorem | brdom4 4794 | An equivalence to a dominance relation. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A ≼ B ↔ ∃f(∀x ∈ B ∃*y(y ∈ A ⋀ xfy) ⋀ ∀x ∈ A ∃y ∈ B yfx)) | ||
| Theorem | brdom7disj 4795 | An equivalence to a dominance relation for disjoint sets. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ (A ∩ B) = ∅ ⇒ ⊢ (A ≼ B ↔ ∃f(∀x ∈ B ∃*y(y ∈ A ⋀ {x, y} ∈ f) ⋀ ∀x ∈ A ∃y ∈ B {y, x} ∈ f)) | ||
| Theorem | brdom6disj 4796 | An equivalence to a dominance relation for disjoint sets. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ (A ∩ B) = ∅ ⇒ ⊢ (A ≼ B ↔ ∃f(∀x ∈ B ∃*y{x, y} ∈ f ⋀ ∀x ∈ A ∃y ∈ B {y, x} ∈ f)) | ||
| Theorem | imadomg 4797 | An image of a function under a set is dominated by the set. Proposition 10.34 of [TakeutiZaring] p. 92. |
| ⊢ (A ∈ B → (Fun F → (F “ A) ≼ A)) | ||
| Theorem | fnrndomg 4798 | The range of a function is dominated by its domain. |
| ⊢ (A ∈ B → (F Fn A → ran F ≼ A)) | ||
| Theorem | unidom 4799 | An upper bound for the cardinality of a union. Theorem 10.47 of [TakeutiZaring] p. 98. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (∀x ∈ A x ≼ B → ∪A ≼ (A × B)) | ||
| Theorem | unidomg 4800 | An upper bound for the cardinality of a union. Theorem 10.47 of [TakeutiZaring] p. 98. |
| ⊢ ((A ∈ C ⋀ B ∈ D ⋀ ∀x ∈ A x ≼ B) → ∪A ≼ (A × B)) | ||
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |