Here's Dedekind's definition:
A set $S$ is said to be infinite if there is an injection from $S$ to one of its proper subsets.
There is a hidden other half implied by this definition, namely that a finite set is one that is not infinite. One might imagine that it also says:
A set $S$ is said to be finite if there is no injection from $S$ to any of its proper subsets.
Or equivalently:
There is no injection from a finite set $S$ to one of its proper subsets.
Or equivalently:
If $f$ is a mapping from a finite set $S$ to one of its proper subsets, then $f$ is not an injection
Replacing "injection" with its definition:
If $f$ is a mapping from a finite set $S$ to one of its proper subsets, there are distinct $x$ and $y$ in $S$ with $f(x) = f(y)$
Now comes what I think is the only leap: imagine that the elements of $S$ are the pigeons, and that the pigeonholes are also labeled by elements of $S$. But not every possible element of $S$ is a label, so that the set of labels is a proper subset of $S$. Then the function $f$ says, for each pigeon, which hole it goes into:
If $f$ is a mapping from a finite set of pigeons $S$ to a set of pigeonholes labeled with elements of a proper subset of $S$,there are distinct pigeons $x$ and $y$ with $f(x) = f(y)$
Or equivalently:
If $f$ sends pigeons from a finite set $S$ to a set of pigeonholes labeled with elements of a proper subset of $S$, there are distinct pigeons $x$ and $y$ sent to the same hole
I think this is the version of the pigeonhole principle that Kanamori was thinking of.
There's still a piece missing before we get to your version of the pigeonhole principle, which is that finite sets have sizes, which are numbers. To do this properly is a little bit technical.
We define a number to be one of the sets $0=\varnothing, 1=\{0\}, 2=\{0, 1\}, 3=\{0, 1, 2\}, \ldots$. We can define $<$ to be the same as $\in$, or perhaps the restriction of $\in$ to the set of numbers. For example, $1<3$ because $1\in 3 = \{0,1,2\}$.
Then we can show that for any finite set $S$ there is exactly one number $n$ for which there is a bijection $c:S\to n$, and we can say that this unique number is the size $|S|$ of set $S$. Then we can show that if $S$ and $S'$ are finite sets with $S'\subsetneq S$, then $|S'|<|S|$.
Once this "size" machinery is in place, we can transform the statement of the pigeonhole principle above from one about a set and its proper subset to one about the sizes of the two sets:
If $f$ sends pigeons from a set of size $s$ to a set of pigeonholes of size $s'$, with $s'<s$, there are distinct pigeons $x$ and $y$ sent to the same hole
Or, leaving $f$ implicit:
If pigeons are sent from a set of size $s$ to a set of pigeonholes of size $s'$, with $s'<s$, there are distinct pigeons $x$ and $y$ sent to the same hole
Which is pretty much what you said:
If $s$ items are put into $s'$ pigeonholes with $s > s'$, then at least one pigeonhole must contain more than one item.
I hope this is some help.
Best Answer
The theorem is false. It becomes true if you change "XOR" to "OR" and your proof becomes correct if you replace $\Leftarrow\Rightarrow$ with $\wedge$.