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

Theorem ac3 8331
Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac 8328 can be established by chaining aceq0 7988 and aceq2 7989. A standard textbook version of AC is derived from this one in dfac2a 7999, and this version of AC is derived from the textbook version in dfac2 8000.

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 7562. The key theorem for this (used in the proof of dfac2 8000) is preleq 7561. 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 8330 . 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 7989 . 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 200 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 359   E.wex 1550    =/= wne 2598   A.wral 2697   E.wrex 2698   E!wreu 2699   (/)c0 3620
This theorem is referenced by:  axac2  8335
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-ac 8328
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-v 2950  df-dif 3315  df-nul 3621
  Copyright terms: Public domain W3C validator