Can you prove this without axiom of choice?

Question

Let $\{ X_i\} (i\in I)$ be a family such that $X_i\neq\varnothing$ for all $i\in I$.
Let $J\subset I$.
Let $\prod_{i\in J} X_i=\{ x\in (\bigcup_{i\in J} X_i)^{J} : \forall i(i\in J\to x_i\in X_i\}$

Prove, without axiom of choice (if possible), that $$\prod_{i\in J} X_i=\{ x|J : x\in\prod_{i\in I} X_i\}$$

---

Note:

1. $\prod_{i\in I} X_i$ denotes the Cartesian product of the family $\{ X_i\} (i\in I)$.
2. $Y^{X}$ is the set set of all functions from $X$ to $Y$.
3. If $f:Y\to Z$ and $X\subset Y$, then $f|X$ denotes $f$ restricted to $X$.

Answer 1

You can prove without choice that the restriction map $x \mapsto x|J$ is given by the following composite $$\prod_{i \in I} X_i \xrightarrow{\cong} \left( \prod_{i \in I \setminus J} X_i \right) \times \left( \prod_{i \in J} X_i \right) \xrightarrow{\pi_2} \prod_{i \in J} X_i$$ where the first map is the bijection defined by $(x_i)_{i \in I} \mapsto ((x_i)_{i \in I \setminus J}, (x_i)_{i \in J})$, and the second map is the projection onto the second coordinate.

To say that each $x \in \prod_{i \in J} X_i$ is the restriction of some element of $\prod_{i \in I} X_i$ is therefore equivalent to saying that this projection map is surjective. This, in turn is equivalent to saying that $\prod_{i \in I \setminus J} X_i$ is inhabited.

...but saying that $\prod_{i \in I \setminus J} X_i$ is inhabited for all indexing sets $I$ and $J \subseteq I$ and all inhabited $X_i$ is equivalent to the axiom of choice. (To see why, consider the case when $J = \varnothing$.)

Answer 2

No, in fact the assertion that this equality holds in all instances is equivalent to the axiom of choice. Here is the problem:

The axiom of choice is equivalent to "for all $I$ and sequences $\langle X_i\mid i\in I\rangle$ of nonempty sets, $\prod_{i\in I} X_i\neq\emptyset$", maybe this is even the variant of choice you are used to.

So if the axiom of choice fails, this means that there is some $I$ and a sequence $\langle X_i\mid i\in I\rangle$ of nonempty sets so that in fact $\prod_{i\in I} X_i=\emptyset$. It is now clear that for any $J\subseteq I$ the righthand side $\{x\vert J\mid x\in\prod_{i\in I} X_i\}$ is empty. However, finite choice is true just in ZF, so that for any finite $J\subseteq I$, $\prod_{i\in J} X_i\neq\emptyset$. If you haven't seen this, it is a good exercise to prove this. In our case, we can take $J$ to be a singleton, in which case it is trivial that $\prod_{i\in J} X_i\neq\emptyset$, so the equiality fails.