Metamath Proof Explorer

Axiom ax-ac

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 ⊢ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v

Detailed syntax breakdown

Step Hyp Ref Expression
0 vy setvar y
1 vz setvar z
2 vw setvar w
3 1 cv setvar z
4 2 cv setvar w
5 3 4 wcel wff z ∈ w
6 vx setvar x
7 6 cv setvar x
8 4 7 wcel wff w ∈ x
9 5 8 wa wff z ∈ w ∧ w ∈ x
10 vv setvar v
11 vu setvar u
12 vt setvar t
13 11 cv setvar u
14 13 4 wcel wff u ∈ w
15 12 cv setvar t
16 4 15 wcel wff w ∈ t
17 14 16 wa wff u ∈ w ∧ w ∈ t
18 13 15 wcel wff u ∈ t
19 0 cv setvar y
20 15 19 wcel wff t ∈ y
21 18 20 wa wff u ∈ t ∧ t ∈ y
22 17 21 wa wff u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y
23 22 12 wex wff ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y
24 10 cv setvar v
25 13 24 wceq wff u = v
26 23 25 wb wff ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v
27 26 11 wal wff ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v
28 27 10 wex wff ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v
29 9 28 wi wff z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v
30 29 2 wal wff ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v
31 30 1 wal wff ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v
32 31 0 wex wff ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v