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	⊢ ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )