Do we need Axiom of Choice to prove $|\prod_{i\in J}A_i| \le |\prod_{i\in I}A_i|$ for all $J \subseteq I$ where $I \setminus J$ is infinite? To prove the theorem, I try to define a injection $G:\prod\limits_{i\in J}A_i \to \prod\limits_{i\in I}A_i$. I'm able to define $G(\phi)$ for all $i \in J$ by $G(\phi)(i) = \phi(i)$. I feel that to define $G(\phi)$ for $i \in I \setminus J$ is impossible without AC in case $I \setminus J$ is infinite.

The Cartesian product of a family $(A_i\mid i\in I)$ is defined as $$\prod\limits_{i\in I}A_i=\{f:I\to\bigcup_{i \in I} A_i\mid f(i)\in A_i \text{ for all } i \in I\}$$

Theorem : Let $J \subseteq I$, then $|\prod\limits_{i\in J}A_i| \le |\prod\limits_{i\in I}A_i|$.


Consider
$$\begin
{array}{l|rcl}
G : & \prod\limits_{i\in J}A_i
 & \longrightarrow & \prod\limits_{i\in I}A_i \\
    & \phi & \longmapsto & G(\phi) \end{array}$$
where $\phi:J \to \bigcup_{i\in J}A_i$ such that $\phi(i) \in A_i$ for all $i \in J$.
$G(\phi)$ is defined by $G(\phi)(i) = \phi(i)$ for all $i \in J$.
 A: Of course. It might just be that $\prod_{i\in I\setminus J} A_i$ is empty.
For example, take any $I'$ whose product is empty, and add $J$ as a family with a nonempty product, and $I=I'\cup J$.
If course, once you know that $\prod_{i\in I} A_i$ is nonempty, then the statement is true. Simply fix one choice function, and look at the modifications on $J$ given by the choice functions from $\prod_{i\in J} A_i$. 
A: On the basis of @Asaf Karagila's answer and @Andrés E. Caicedo's comments, I present a solution in my own words here so that I can truly understand their ideas. All credits are given to @Asaf Karagila and @Andrés E. Caicedo.


Suppose $J \subseteq I$. Find the necessary and sufficient conditions that the below inequality holds.  $$|\prod\limits_{i\in J}A_i| \le |\prod\limits_{i\in I}A_i|$$

There are only two possible cases


*

*$\prod\limits_{i\in J}A_i = \emptyset$


$I \subseteq J$ and $\prod\limits_{i\in J}A_i = \emptyset \implies \prod\limits_{i\in I}A_i = \emptyset$. Then $|\prod\limits_{i\in J}A_i| = |\prod\limits_{i\in I}A_i| = 0$. Hence the inequality holds.


*$\prod\limits_{i\in J}A_i \neq \emptyset$


Then $|\prod\limits_{i\in J}A_i| \ge 1$. In order for the inequality to hold, $|\prod\limits_{i\in I}A_i| \ge 1$, and consequently $\prod\limits_{i\in I}A_i \neq \emptyset$.
For $\prod\limits_{i\in I}A_i \neq \emptyset$, there exists a mapping $f:I \to \bigcup_{i \in I} A_i$ such that $f(i)\in A_i \text{ for all } i \in I$. Consider
$$\begin
{array}{l|rcl}
G : & \prod\limits_{i\in J}A_i
 & \longrightarrow & \prod\limits_{i\in I}A_i \\
    & \phi & \longmapsto & G(\phi) \end{array}$$
where $G(\phi)$ is defined by
$$G(\phi)(i)=\begin{cases}\phi(i) & \text{ for all } i \in J\\
f(i) & \text{ for all } i \in I \setminus J
\end {cases}$$
$G$ is injective
For $\phi_1,\phi_2 \in \prod\limits_{i\in J}A_i$ and $G(\phi_1)=G(\phi_2)$. Then $G(\phi_1)(i)=G(\phi_2)(i)$ for all $i \in I$. Then $\phi_1(i)=\phi_2(i)$ for all $i \in J$ and $f(i) = f(i)$ for all $i \in I \setminus J$. Thus $\phi_1 = \phi_2$. Hence $G$ is injective.
Since $G$ is injective, $|\prod\limits_{i\in J}A_i| \le |\prod\limits_{i\in I}A_i|$, or equivalently the inequality holds.
To sum up the two cases:
The inequality holds $\iff$ $\prod\limits_{i\in J}A_i = \emptyset$ or $\begin{cases} \prod\limits_{i\in J}A_i \neq \emptyset & \\
\prod\limits_{i\in I}A_i \neq \emptyset & 
\end {cases} \iff \prod\limits_{i\in J}A_i = \emptyset$ or $\prod\limits_{i\in I}A_i \neq \emptyset$
