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
|- 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 ) )

Detailed syntax breakdown

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 ) )