Theorem ac3 4809

Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac 4806 can be established by chaining aceq0 4792 and aceq2 4793. A standard textbook version of AC is derived from this one in aceq6a 4803, and this version of AC is derived from the textbook version in aceq6b 4804.

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 4666. The key theorem for this (used in the proof of aceq6b 4804) is preleq 4665. 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 4808	. 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 4793	. 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 196	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 230   e. wcel 999  E.wex 1021   =/= wne 1632  A.wral 1692  E.wrex 1693  E!wreu 1694  (/)c0 2331

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-ac 4806

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-reu 1698  df-v 1859  df-dif 2100  df-nul 2332

Copyright terms: Public domain