Theorem ac3 4719

Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac 4716 can be established by chaining aceq0 4702 and aceq2 4703. A standard textbook version of AC is derived from this one in aceq6a 4713, and this version of AC is derived from the textbook version in aceq6b 4714.

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 4576. The key theorem for this (used in the proof of aceq6b 4714) is preleq 4575. 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:   x,y,z,w,v

Proof of Theorem ac3

Step	Hyp	Ref	Expression
1		ac2 4718	. 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 4703	. 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 189	1 |- E.yA.z e. x (z =/= (/) -> E!w e. z E.v e. y (z e. v /\ w e. v))

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 955  E.wex 977   =/= wne 1577  A.wral 1637  E.wrex 1638  E!wreu 1639  (/)c0 2270

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-ac 4716

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-reu 1643  df-v 1803  df-dif 2039  df-nul 2271

Copyright terms: Public domain