Metamath Proof Explorer


Theorem ac3

Description: Axiom of Choice using abbreviations. The logical equivalence to ax-ac can be established by chaining aceq0 and aceq2 . A standard textbook version of AC is derived from this one in dfac2a , and this version of AC is derived from the textbook version in dfac2b , showing their logical equivalence (see dfac2 ).

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 ofordered pairs, very similar to the ordered pair construction opthreg . The key theorem for this (used in the proof of dfac2b ) is preleq . 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)

Ref Expression
Assertion ac3 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) )

Proof

Step Hyp Ref Expression
1 ac2 𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 )
2 aceq2 ( ∃ 𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∃ 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
3 1 2 mpbi 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) )