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

Theorem ac3 8268
Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac 8265 can be established by chaining aceq0 7925 and aceq2 7926. A standard textbook version of AC is derived from this one in dfac2a 7936, and this version of AC is derived from the textbook version in dfac2 7937.

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 7499. The key theorem for this (used in the proof of dfac2 7937) is preleq 7498. 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 8267 . 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 7926 . 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 2543   A.wral 2642   E.wrex 2643   E!wreu 2644   (/)c0 3564
This theorem is referenced by:  axac2  8272
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 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-ac 8265
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-reu 2649  df-v 2894  df-dif 3259  df-nul 3565
  Copyright terms: Public domain W3C validator