Prove that if $f : X \to Y$ is a function between non-empty finite sets such that $|X| \lt |Y|$, then $f$ is not a surjection. 
Theorem 11.1.6: Suppose that $f: X \to Y$ is a function between non-empty finite sets such that $|X| \lt |Y|$. Then $f$ is not a surjection, i.e. there exists an element of $Y$ which is not a value of the function.

This is a theorem from the book "Introduction to Mathematical Reasoning" by P.J.Eccles which I would like to prove. The author provides the following hints:

"This can be proved by similar methods to the pigeonhole principle. Alternatively it can be deduced from the pigeonhole principle by observing that from a surjection $X \to Y$ it is possible to construct an injection $Y \to X$."

The latter approach is given as an exercise further on the book, so I am most interested in the first. The author proved the pigeonhole principle as follows:

Theorem 11.1.2 (Pigeonhole principle): Suppose that $f: X \to Y$ is a function between non-empty finite sets such that $|X| \gt |Y|$. Then $f$ is not an injection, i.e. there exist distinct elements $x_1$ and $x_2 \in X$ such that $f(x_1) = f(x_2)$.

$Proof$ This is the contrapositive of Corollary 11.1.1 and so follows from that result.
$\tag*{$\blacksquare$}$
And the revelant corollary is

Corollary 11.1.1: Suppose that $X$ and $Y$ are non-empty finite sets. If there exists an injection $f: X \to Y$ then $|X| \le |Y|$.

For the proof of Theorem 11.1.6 I decided to make use of the following:

Ex.11.1: Suppose that ${\mathbb N_n} \to X$ is a surjection. Then $X$ is a finite set and $|X| \le n$.

$Proof\ (of\ Theorem\ 11.1.6)$ Let $X$ be non-empty finite set such that $|X| = n$. Then there exists a bijection
$$g: \mathbb{N_n} \to X$$
Suppose there exists a surjection $f : X \to Y$. We can then define 
$$ h = f \circ g : \mathbb{N_n} \to X \to Y$$
which is a surjection, given that is it a composite of surjections.
Then there exists a surjection
$$\mathbb {N_n} \to Y$$
By Ex.11.1, $n \ge |Y|$, or $|X| \ge |Y|$.
This is the contrapositive of what we wished to prove, and so we are done.
$\tag*{$\blacksquare$}$
QUESTION
Is the above proof correct? Specifically, is it really the contrapositive of the wanted? And if so, was it deduced correctly?
Thank you
 A: Best case scenario : $f$ is an injective function.
Let $X,Y$ be finite sets such that where $\mid \,X \mid \, < \, \mid Y\, \mid $ and we have an injective function $f : X \to Y$.
By injectivity, $f(x) = f(x') \iff x = x'$. Additionally, by injectivity, we know for all $f(x) \in f[X]$, there exists exactly one $x \in X$ such that $x$ maps to $f(x) \in f[X] \subseteq Y$. Moreover, there is bijection from $X$ to $f[X]$. Thus we know $|X| = |f[X]|$ and $f[X] \subseteq Y$ so we can deduce that $|f[X]| < |Y|$. Hence there exists at least one $y \in Y$ such that for no $x \in X$ it will happen that $f(x) = y$. Therefore, no surjection exists.
if $f$ is not injective then $|f[X]| < |X| < |Y|$
A: By the definition of function, every element in $X$ has one and only one image in $Y$. 
Given, $|X|<|Y|$ so we can assume $|X|=m; |Y|=m+n (n>0)$.
By the definition of function, all the $m$ elements in $|X|$ are in an association with exactly $m$ elements in $Y$(note the 'one and only one' part). 
$\therefore $ exactly $n$ elements are in $Y$ that are not present in the range of $f$, i.e., are not associated to any element in $X$. Now, if you know the definition of a surjective function, then you will know that we have proved that $f$ is not surjective. 
As for the PHP part, if $m$ pigeons are put into $m+n$ holes then at least $n$ holes will be left empty.
And yeah, I hope you know that a function is either surjective or not surjective. There is nothing in between(This is trivial. But is essential for the proof to be logically correct). 
A: This proof is correct.   
Normally people would phrase this argument in a more informal manner,
along the lines of:  "If $f: X \to Y$ is surjective, and $X$ has $n$ elements,
then $Y$ has $\leq n$ elements."
But in the context of your particular text and course, your argument looks good.    
