Theorem ac3 3568

Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac 1080 can be established by chaining aceq0 3553 and aceq2 3554. A standard textbook version of AC is derived from this one in aceq6a 3564, and this version of AC is derived from the textbook version in aceq6b 3565.

The following sketch will help you understand this version of the axiom. Given any set x, the axiom says that there exists a y that is a collection of unordered pairs, one pair for each non-empty 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. Using the Axiom of Regularity, we can show that y is really a set of ordered pairs, very similar to the ordered pair construction opthreg 3455. The key theorem for this (used in the proof of aceq6b 3565) is preleq 3454. With this modified definition of ordered pair, it can be seen that y is actually a choice function on the members of x.

For example, suppose x = {{1, 2}, {1, 3}, {2, 3}}. Take y = {{{1, 2}, 1}, {{1, 3}, 1}, {{2, 3}, 2}}. For the member (of x) z = {1, 2}, the only assignment to w and v that satisfies the axiom is w = 1 and v = {{1, 2}, 1}, so there is exactly one w as required. We verify the other two members of x similarly. Thus y satisfies the axiom. Using our modified ordered pair definition, it is easy to see that y is the choice function {<.{1, 2}, 1>., <.{1, 3}, 1>., <.{2, 3}, 2>.}. Of course other choices for y will also satisfy the axiom, for example y = {{{1, 2}, 2}, {{1, 3}, 1}, {{2, 3}, 3}}. What AC tells us is that there exists at least one such y, but it doesn't tell us which one.

Assertion

Ref	Expression
ac3	|- E.yA.z e. x (-. z = (/) -> E!w e. z E.v e. y (z e. v /\ w e. v))

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

Proof of Theorem ac3

Step	Hyp	Ref	Expression
1		ac2 3567	. 2 |- E.yA.z e. x A.w e. z E!v e. z E.u e. y (z e. u /\ v e. u)
2		aceq2 3554	. 2 |- (E.yA.z e. x A.w e. z E!v e. z E.u e. y (z e. u /\ v e. u) <-> E.yA.z e. x (-. z = (/) -> E!w e. z E.v e. y (z e. v /\ w e. v)))
3	1, 2	mpbi 164	1 |- E.yA.z e. x (-. z = (/) -> E!w e. z E.v e. y (z e. v /\ w e. v))

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196  E.wex 678   e. wel 803   = wceq 1091  A.wral 1201  E.wrex 1202  E!wreu 1203  (/)c0 1707

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-ac 1080

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-reu 1207  df-v 1349  df-dif 1489  df-nul 1708

metamath.org