Theorem ac4

Description: Equivalent of Axiom of Choice. We do not insist that f be a function. However, Theorem ac5 , derived from this one, shows that this form of the axiom does imply that at least one such set f whose existence we assert is in fact a function. Axiom of Choice of TakeutiZaring p. 83.

Takeuti and Zaring call this "weak choice" in contrast to "strong choice" E. F A. z ( z =/= (/) -> ( Fz ) e. z ) , which asserts the existence of a universal choice function but requires second-order quantification on (proper) class variable F and thus cannot be expressed in our first-order formalization. However, it has been shown that ZF plus strong choice is a conservative extension of ZF plus weak choice. See Ulrich Felgner, "Comparison of the axioms of local and universal choice",Fundamenta Mathematica, 71, 43-62 (1971).

Weak choice can be strengthened in a different direction to choose from a collection of proper classes; see ac6s5 . (Contributed by NM, 21-Jul-1996)

	Ref	Expression
Assertion	ac4	⊢ ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		dfac3	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
2	1	axaci	⊢ ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 )