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