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

Theorem ac3 8306
Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac 8303 can be established by chaining aceq0 7963 and aceq2 7964. A standard textbook version of AC is derived from this one in dfac2a 7974, and this version of AC is derived from the textbook version in dfac2 7975.

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 7537. The key theorem for this (used in the proof of dfac2 7975) is preleq 7536. 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 8305 . 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 7964 . 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 1547    =/= wne 2575   A.wral 2674   E.wrex 2675   E!wreu 2676   (/)c0 3596
This theorem is referenced by:  axac2  8310
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-ac 8303
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-v 2926  df-dif 3291  df-nul 3597
  Copyright terms: Public domain W3C validator