The need for the axiom of choice is to choose arbitrary elements. Injectivity eliminates this need.
Assume that $A$ is not empty, if $f\colon A\to B$ is injective this means that if $b\in B$ is in the range of $f$ then there is a unique $a\in A$ such that $f(a)=b$.
This means that we can define (from $f$) what is the $a$ to which we send $b$.
So if $f$ is not onto $B$ we have two options:
- $b\in B$ in the range of $f$, then we have exactly one option to send $b$ to.
- $b\in B$ not in the range of $f$. Since $A$ is not empty fix in advance some $a_0\in A$ and send $b$ to $a_0$.
Another way to see this is let $B=B'\cup Rng(f)$, where $B'\cap Rng(f)=\varnothing$. Fix $a_0\in A$ and define $g|_{B'}(x)=a_0$. For every $b\in Rng(f)$ we have that $f^{-1}[\{b\}]=\{a\in A\mid f(a)=b\}$ is a singleton, so there is only one function which we can define in: $$\prod_{b\in Rng(f)}f^{-1}[\{b\}]$$
Now let the unique function in the product be $g|_{Rng(f)}$ and define $g$ to be the union of these two.
Your intuition about the need for the axiom of choice is true for surjections, if $f$ was surjective then we only know that $f^{-1}[\{b\}]$ is non-empty for every $b\in B$, and we need the full power of the axiom of choice to ensure that an arbitrary surjection has an inverse function.
To the edited question:
The axiom of choice is needed because we have models in which the axiom of choice does not hold, where there exists an infinite family of pairs whose product is empty.
There are weaker forms from which follow choice principles for finite sets. However these are still not provable from ZF on its own.
As indicated by Chris Eagle in the comments, and as I remark above, in a product of singletons there is no need for the axiom of choice since there is only one way to choose from a singleton.
Further reading:
- Finite choice without AC
- axiom of choice: cardinality of general disjoint union
Your proof is not a proof, but rather an intuition why the AC should be true.
Recall the precise(!) definition of the product of a family of sets: $\prod_{i \in I} X_i$ consists of functions $f : I \to \bigcup_{i \in I} X_i$ such that $f(i) \in X_i$ for all $i \in I$. Also recall the definition of a function $A \to B$ as a special subset of $A \times B$.
Now, given non-empty sets $X_i$, how do you define such a function, using the other ZF axioms? You say, for every $i \in I$ we choose some element $x_i \in X_i$. This works for every single $i$ at a time, but this doesn't define a function $i \mapsto x_i$.
Example: Let $I$ be the set of all non-empty subsets of $\mathbb{R}$, and $X_i = i$. Then an element $f$ in $\prod_{i \in I} X_i$ is a function which picks an element $f(T) \in T$ for every non-empty $T \subseteq \mathbb{R}$. How do you define such an $f$? If we would have $\mathbb{N}$ instead of $\mathbb{R}$, we could take $f(T)=\min(T)$, but this doesn't work for $\mathbb{R}$. Apparently, there is no canonical choice of an element in a non-empty set of real numbers. But the AC tells us that we don't have to worry about this, it gives us such a function, even if we cannot "write it down" (which means: construct it from the other ZF axioms).
By the way, if we let $I$ be to be the set of all non-empty open subsets of $\mathbb{R}$, then there is a choice function (provably in ZF): Choose any bijection $\tau : \mathbb{N} \to \mathbb{Q}$, and then assign to each open subset $\emptyset \neq U \subseteq \mathbb{R}$ the element $\tau(\min \{n \in \mathbb{N} : \tau(n) \in U\})$. This works since $U \cap \mathbb{Q} \neq \emptyset$.
Best Answer
No. You may simply pick $x_i=42$ for all $i\in I$.