Let $X_1,X_2,Y_1,Y_2$ be nonempty disjoint sets, where $|X_i|<|Y_i|$. Here, we take this to mean that there is an injection $X_i\to Y_i$, but there is no bijection $X_i\to Y_i$. My question is, is the following statement true in ZF:
$\begin{align} |X_1|+|X_2|:= |X_1\coprod X_2| < |Y_1|\cdot |Y_2|:=|Y_1\times Y_2| \end{align}$
The $\leq$ part is easily seen to be true, but every proof i've found of König's Theorem in the general case fails without the axiom of choice even for the case of two sets (Even though we do not choice to claim the product is nonempty). In particular, the failure usually manifests as an assertion such as "There exists no surjection $X_i \to Y_i$" or an equivalent assertion. This claim is only equivalent to $|X_1|<|Y_1|$ in the presence of choice (Or the partition principle, but is not a priori true in ZF).
I am wondering if this claim is even provable in ZF, or maybe I am missing a very easy proof that does not depend on choice.
Surprisingly enough, it does.
It is consistent that $\Bbb R$ is the union of two sets of smaller cardinality. Since $\Bbb{|R|=|R^2|}$, this provides a counterexample.