| Description: Axiom of Choice using
abbreviations.  The logical equivalence to ax-ac 10500
       can be established by chaining aceq0 10159 and aceq2 10160.  A standard
       textbook version of AC is derived from this one in dfac2a 10171, and this
       version of AC is derived from the textbook version in dfac2b 10172, showing
       their logical equivalence (see dfac2 10173). 
       The following sketch will help you understand this version of the axiom.
       Given any set 𝑥, the axiom says that there exists a
𝑦
that is a
       collection of unordered pairs, one pair for each nonempty member of
       𝑥.  One entry in the pair is the member
of 𝑥, and the other
       entry is some arbitrary member of that member of 𝑥.  Using the
       Axiom of Regularity, we can show that 𝑦 is really a set of
ordered
       pairs, very similar to the ordered pair construction opthreg 9659.  The
       key theorem for this (used in the proof of dfac2b 10172) is preleq 9657.
       With this modified definition of ordered pair, it can be seen that 𝑦
       is actually a choice function on the members of 𝑥.
 
       For example, suppose 𝑥 = {{1, 2}, {1, 3}, {2, 3, 4}}.
       Let us try 𝑦 = {{{1, 2}, 1}, {{1, 3}, 1},
       {{2, 3, 4}, 2}}.  For the member (of 𝑥)
       𝑧 =
{1, 2}, the only assignment to 𝑤 and 𝑣 that
       satisfies the axiom is 𝑤 = 1 and 𝑣 = {{1, 2}, 1}, so
       there is exactly one 𝑤 as required.  We verify the other two
members
       of 𝑥 similarly.  Thus, 𝑦
satisfies the axiom.  Using our
       modified ordered pair definition, we can say that 𝑦 corresponds to
       the choice function {〈{1, 2}, 1〉, 〈{1,
3}, 1〉,
       〈{2, 3, 4}, 2〉}.  Of course other
choices for 𝑦 will
       also satisfy the axiom, for example
       𝑦 =
{{{1, 2}, 2}, {{1, 3}, 1},
       {{2, 3, 4}, 4}}.  What AC tells us is that there
exists at
       least one such 𝑦, but it doesn't tell us which one.
 
       (New usage is discouraged.)  (Contributed by NM,
19-Jul-1996.) |