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	$$⊢\exists y\forall z\in x\left(z\ne \varnothing \to \exists !w\in z\exists v\in y\left(z\in v\wedge w\in v\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ac2	$$⊢\exists y\forall z\in x\forall w\in z\exists !v\in z\exists u\in y\left(z\in u\wedge v\in u\right)$$
2		aceq2	$$⊢\exists y\forall z\in x\forall w\in z\exists !v\in z\exists u\in y\left(z\in u\wedge v\in u\right)\leftrightarrow \exists y\forall z\in x\left(z\ne \varnothing \to \exists !w\in z\exists v\in y\left(z\in v\wedge w\in v\right)\right)$$
3	1 2	mpbi	$$⊢\exists y\forall z\in x\left(z\ne \varnothing \to \exists !w\in z\exists v\in y\left(z\in v\wedge w\in v\right)\right)$$