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

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.    
