Description: 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 nonempty 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 for a more detailed explanation. Theorem ac2 shows an equivalent written compactly with restricted quantifiers.
This version was specifically crafted to be short when expanded to primitives. Kurt Maes' 5-quantifier version ackm is slightly shorter when the biconditional of ax-ac is expanded into implication and negation. In axac3 we allow the constant CHOICE to represent the Axiom of Choice; this simplifies the representation of theorems like gchac (the Generalized Continuum Hypothesis implies the Axiom of Choice).
Standard textbook versions of AC are derived as ac8 , ac5 , and ac7 . The Axiom of Regularity ax-reg (among others) is used to derive our version from the standard ones; this reverse derivation is shown as Theorem dfac2b . Equivalents to AC are the well-ordering theorem weth and Zorn's lemma zorn . See ac4 for comments about stronger versions of AC.
In order to avoid uses of ax-reg for derivation of AC equivalents, we provide ax-ac2 (due to Kurt Maes), which is equivalent to the standard AC of textbooks. The derivation of ax-ac2 from ax-ac is shown by Theorem axac2 , and the reverse derivation by axac . Therefore, new proofs should normally use ax-ac2 instead. (New usage is discouraged.) (Contributed by NM, 18-Jul-1996)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-ac | |- E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vy | |- y |
|
| 1 | vz | |- z |
|
| 2 | vw | |- w |
|
| 3 | 1 | cv | |- z |
| 4 | 2 | cv | |- w |
| 5 | 3 4 | wcel | |- z e. w |
| 6 | vx | |- x |
|
| 7 | 6 | cv | |- x |
| 8 | 4 7 | wcel | |- w e. x |
| 9 | 5 8 | wa | |- ( z e. w /\ w e. x ) |
| 10 | vv | |- v |
|
| 11 | vu | |- u |
|
| 12 | vt | |- t |
|
| 13 | 11 | cv | |- u |
| 14 | 13 4 | wcel | |- u e. w |
| 15 | 12 | cv | |- t |
| 16 | 4 15 | wcel | |- w e. t |
| 17 | 14 16 | wa | |- ( u e. w /\ w e. t ) |
| 18 | 13 15 | wcel | |- u e. t |
| 19 | 0 | cv | |- y |
| 20 | 15 19 | wcel | |- t e. y |
| 21 | 18 20 | wa | |- ( u e. t /\ t e. y ) |
| 22 | 17 21 | wa | |- ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) |
| 23 | 22 12 | wex | |- E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) |
| 24 | 10 | cv | |- v |
| 25 | 13 24 | wceq | |- u = v |
| 26 | 23 25 | wb | |- ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) |
| 27 | 26 11 | wal | |- A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) |
| 28 | 27 10 | wex | |- E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) |
| 29 | 9 28 | wi | |- ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) |
| 30 | 29 2 | wal | |- A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) |
| 31 | 30 1 | wal | |- A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) |
| 32 | 31 0 | wex | |- E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) |