Theorem ac3 4757

Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac 4754 can be established by chaining aceq0 4740 and aceq2 4741. A standard textbook version of AC is derived from this one in aceq6a 4751, and this version of AC is derived from the textbook version in aceq6b 4752.

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 4613. The key theorem for this (used in the proof of aceq6b 4752) is preleq 4612. 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 4756	. 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 4741	. 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 960  E.wex 982   =/= wne 1588  A.wral 1648  E.wrex 1649  E!wreu 1650  (/)c0 2283

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-ac 4754

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-reu 1654  df-v 1815  df-dif 2052  df-nul 2284

Copyright terms: Public domain