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 | ⊢ ∃ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑣 ∀ 𝑢 ( ∃ 𝑡 ( ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) ∧ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) ) ↔ 𝑢 = 𝑣 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vy | ⊢ 𝑦 | |
| 1 | vz | ⊢ 𝑧 | |
| 2 | vw | ⊢ 𝑤 | |
| 3 | 1 | cv | ⊢ 𝑧 |
| 4 | 2 | cv | ⊢ 𝑤 |
| 5 | 3 4 | wcel | ⊢ 𝑧 ∈ 𝑤 |
| 6 | vx | ⊢ 𝑥 | |
| 7 | 6 | cv | ⊢ 𝑥 |
| 8 | 4 7 | wcel | ⊢ 𝑤 ∈ 𝑥 |
| 9 | 5 8 | wa | ⊢ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) |
| 10 | vv | ⊢ 𝑣 | |
| 11 | vu | ⊢ 𝑢 | |
| 12 | vt | ⊢ 𝑡 | |
| 13 | 11 | cv | ⊢ 𝑢 |
| 14 | 13 4 | wcel | ⊢ 𝑢 ∈ 𝑤 |
| 15 | 12 | cv | ⊢ 𝑡 |
| 16 | 4 15 | wcel | ⊢ 𝑤 ∈ 𝑡 |
| 17 | 14 16 | wa | ⊢ ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) |
| 18 | 13 15 | wcel | ⊢ 𝑢 ∈ 𝑡 |
| 19 | 0 | cv | ⊢ 𝑦 |
| 20 | 15 19 | wcel | ⊢ 𝑡 ∈ 𝑦 |
| 21 | 18 20 | wa | ⊢ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) |
| 22 | 17 21 | wa | ⊢ ( ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) ∧ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) ) |
| 23 | 22 12 | wex | ⊢ ∃ 𝑡 ( ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) ∧ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) ) |
| 24 | 10 | cv | ⊢ 𝑣 |
| 25 | 13 24 | wceq | ⊢ 𝑢 = 𝑣 |
| 26 | 23 25 | wb | ⊢ ( ∃ 𝑡 ( ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) ∧ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) ) ↔ 𝑢 = 𝑣 ) |
| 27 | 26 11 | wal | ⊢ ∀ 𝑢 ( ∃ 𝑡 ( ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) ∧ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) ) ↔ 𝑢 = 𝑣 ) |
| 28 | 27 10 | wex | ⊢ ∃ 𝑣 ∀ 𝑢 ( ∃ 𝑡 ( ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) ∧ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) ) ↔ 𝑢 = 𝑣 ) |
| 29 | 9 28 | wi | ⊢ ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑣 ∀ 𝑢 ( ∃ 𝑡 ( ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) ∧ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) ) ↔ 𝑢 = 𝑣 ) ) |
| 30 | 29 2 | wal | ⊢ ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑣 ∀ 𝑢 ( ∃ 𝑡 ( ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) ∧ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) ) ↔ 𝑢 = 𝑣 ) ) |
| 31 | 30 1 | wal | ⊢ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑣 ∀ 𝑢 ( ∃ 𝑡 ( ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) ∧ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) ) ↔ 𝑢 = 𝑣 ) ) |
| 32 | 31 0 | wex | ⊢ ∃ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑣 ∀ 𝑢 ( ∃ 𝑡 ( ( 𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡 ) ∧ ( 𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦 ) ) ↔ 𝑢 = 𝑣 ) ) |