Let's say we're in ZF. How would we prove the following theorem?

Let $S$ be a set such that $S \neq \emptyset$. There exists some function $f$ such that $f(S) \in S$.

It seems easy if you can start with

Let $a \in S$, define $f = \{S\} \times \{a\}$.

But I'm not sure how ZF allows you to do that.

  • $\begingroup$ So each nonempty $S$ is allowed a different $f$, which needn't work for other sets, right? $\endgroup$ – J.G. Apr 19 at 19:44
  • 2
    $\begingroup$ It looks fine to me. ZF certainly proves that whenever $x$ is a set then $\{x\}$ is also a set, and it also proves that Cartesian products exist. $\endgroup$ – Nate Eldredge Apr 19 at 20:20
  • $\begingroup$ Also math.stackexchange.com/questions/1839913/… $\endgroup$ – Eric Wofsey Apr 19 at 21:14
  • 3
    $\begingroup$ This really boils down to the underlying logic (classical first-order logic) rather than ZF itself, specifically existential instantiation. Our ability to "for free" pick an object satisfying a given property is given to us even before we write down the ZF axioms. $\endgroup$ – Noah Schweber Apr 19 at 21:54
  • $\begingroup$ Just a minor comment about interpretation, though I am sure that interpretation you've already given it is intended: Since $S$ is a set, $f(S)$ could also mean the set $\{f(s)\mid s \in S\}$. In that case, such an $f$ would only be possible if there is a set $A \in S$ whose cardinality is $\le$ the cardinality of $S$. $\endgroup$ – Paul Sinclair Apr 20 at 3:28

Browse other questions tagged or ask your own question.