Theorem ac3 4727

Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac 4724 can be established by chaining aceq0 4710 and aceq2 4711. A standard textbook version of AC is derived from this one in aceq6a 4721, and this version of AC is derived from the textbook version in aceq6b 4722.

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 4584. The key theorem for this (used in the proof of aceq6b 4722) is preleq 4583. 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 4726	. 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 4711	. 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 956  E.wex 978   =/= wne 1582  A.wral 1642  E.wrex 1643  E!wreu 1644  (/)c0 2276

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-ac 4724

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-reu 1648  df-v 1808  df-dif 2045  df-nul 2277

Copyright terms: Public domain