MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ac3 Unicode version

Theorem ac3 8235
Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac 8232 can be established by chaining aceq0 7892 and aceq2 7893. A standard textbook version of AC is derived from this one in dfac2a 7903, and this version of AC is derived from the textbook version in dfac2 7904.

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 7466. The key theorem for this (used in the proof of dfac2 7904) is preleq 7465. 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.
StepHypRef Expression
1 ac2 8234 . 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 7893 . 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 )
) )
31, 2mpbi 199 1  |-  E. y A. z  e.  x  ( z  =/=  (/)  ->  E! w  e.  z  E. v  e.  y  (
z  e.  v  /\  w  e.  v )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1546    e. wcel 1715    =/= wne 2529   A.wral 2628   E.wrex 2629   E!wreu 2630   (/)c0 3543
This theorem is referenced by:  axac3OLD  8238  axac2  8240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-ac 8232
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-reu 2635  df-v 2875  df-dif 3241  df-nul 3544
  Copyright terms: Public domain W3C validator