Theorem ac3 9284

Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac 9281 can be established by chaining aceq0 8941 and aceq2 8942. A standard textbook version of AC is derived from this one in dfac2a 8952, and this version of AC is derived from the textbook version in dfac2 8953.

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 nonempty 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 8515. The key theorem for this (used in the proof of dfac2 8953) is preleq 8514. 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 , 4 } }. Let us try y = { { { 1 , 2 } , 1 } , { { 1 , 3 } , 1 } , { { 2 , 3 , 4 } , 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, we can say that y corresponds to the choice function { <. { 1 , 2 } , 1 >. , <. { 1 , 3 } , 1 >. , <. { 2 , 3 , 4 } , 2 >. }. Of course other choices for y will also satisfy the axiom, for example y = { { { 1 , 2 } , 2 } , { { 1 , 3 } , 1 } , { { 2 , 3 , 4 } , 4 } }. What AC tells us is that there exists at least one such y, but it doesn't tell us which one.

(New usage is discouraged.) (Contributed by NM, 19-Jul-1996.)

Assertion

Ref	Expression
ac3	|- E. y A. 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

Dummy variable u is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ac2 9283	. 2 |- E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u )
2		aceq2 8942	. 2 |- ( E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
3	1, 2	mpbi 220	1 |- E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) )

Syntax hints:   -> wi 4   /\ wa 384   E.wex 1704   =/= wne 2794   A.wral 2912   E.wrex 2913   E!wreu 2914   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-ac 9281

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  axac2  9288