Axiom ax-ac 1080

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. AC (in a common version given in textbooks) asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. Stated another way, there exists a "choice function" on any set that maps each (non-empty) member of the set to an arbitrary member of that member.

The unpublished version shown here was specifically crafted to be short when expanded to primitives and may be the shortest possible (although Kurt Maes' 5-quantifier formula ackm 3597 is the same length when the biconditional of ax-ac 1080 is expanded). In order to understand ax-ac 1080, you should look at the rewritten version ac3 3568, which is accompanied by an informal explanation.

Standard textbook versions of AC are derived as ac4 3571 and ac5 3573 (which is Axiom AC of [BellMachover] p. 488). The Axiom of Regularity ax-reg 1078 (among others) is used to derive our version from the standard ones; this reverse derivation is shown as theorem aceq6b 3565. Equivalents to AC are the well-ordering theorem weth 3602 and Zorn's lemma zorn2 3612.

Assertion

Ref	Expression
ax-ac	|- E.yA.zA.w((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v))

Distinct variable group(s):   x,y,z,w,v,u,t

Detailed syntax breakdown of Axiom ax-ac

Step	Hyp	Ref	Expression
1		vz	. . . . . . 7 set z
2		vw	. . . . . . 7 set w
3	1, 2	wel 803	. . . . . 6 wff z e. w
4		vx	. . . . . . 7 set x
5	2, 4	wel 803	. . . . . 6 wff w e. x
6	3, 5	wa 196	. . . . 5 wff (z e. w /\ w e. x)
7		vu	. . . . . . . . . . . 12 set u
8	7, 2	wel 803	. . . . . . . . . . 11 wff u e. w
9		vt	. . . . . . . . . . . 12 set t
10	2, 9	wel 803	. . . . . . . . . . 11 wff w e. t
11	8, 10	wa 196	. . . . . . . . . 10 wff (u e. w /\ w e. t)
12	7, 9	wel 803	. . . . . . . . . . 11 wff u e. t
13		vy	. . . . . . . . . . . 12 set y
14	9, 13	wel 803	. . . . . . . . . . 11 wff t e. y
15	12, 14	wa 196	. . . . . . . . . 10 wff (u e. t /\ t e. y)
16	11, 15	wa 196	. . . . . . . . 9 wff ((u e. w /\ w e. t) /\ (u e. t /\ t e. y))
17	16, 9	wex 678	. . . . . . . 8 wff E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y))
18		vv	. . . . . . . . 9 set v
19	7, 18	weq 797	. . . . . . . 8 wff u = v
20	17, 19	wb 127	. . . . . . 7 wff (E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v)
21	20, 7	wal 672	. . . . . 6 wff A.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v)
22	21, 18	wex 678	. . . . 5 wff E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v)
23	6, 22	wi 2	. . . 4 wff ((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v))
24	23, 2	wal 672	. . 3 wff A.w((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v))
25	24, 1	wal 672	. 2 wff A.zA.w((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v))
26	25, 13	wex 678	1 wff E.yA.zA.w((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v))

This axiom is referenced by:  axac 1085  ac2 3567

metamath.org