Proof Verification that Every Finite Set has a Unique Cardinality Is my proof correct for proving that every finite set has a unique cardinality? My part of the proof is as follows:
"Let $A = \{a_1, a_2, ..., a_n\}$ be an arbitrary set with $n$ elements, and let $f:A \rightarrow \{1, 2, ..., n\}$ be a function defined by $f(a_i)=i$ for all $1 \leq i \leq n$. Then this function is bijective, so it follows that $|A| = n$." 
However, I'm still having trouble showing that the cardinality of $A$ is unique. I tried supposing that $|A|=m$ for $m \neq n$, in which I ended up having two possibilities: either $m \leq n$ or $m \geq n$. Suppose that $m \leq n$.  Then there exists a bijective function $f: A \rightarrow \{1, 2, ..., m\}$. My question is, in order to show it cannot be bijective, how would you show it is not one-to-one? 
Now suppose that $m \geq n$. Then again, there exists a bijective function $f: A \rightarrow \{1, 2, ..., m\}$. In this case, my question is, how would you show that it is onto?
I kind of understand it intuitively, but in a formal proof writing, how do you show that these two functions are not one-to-one and not onto?
Thanks in advance. 
 A: I'll assume you know that there is no bijection between two different finite cardinals.  You prove this by showing by induction that if $m$ and $n$ are different finite cardinals, there is always a bijection between one of them and a proper initial segment of the other.  Since there is no bijection between a finite set and one of its proper subsets, that proves there can be no bijection between different finite cardinals.
Now assume $f:A \to n$ and $g:A \to m$ are bijections.  Then because $f$ is a bijection, the function $f^{-1}$ is also a bijection, and $g \circ f^{-1}:n \to m$ is a bijection between two different finite cardinals.
A: Here is an outline:
Definition. Let $X$ and $Y$ be sets.


*

*Say $X$ injects into $Y$, denoted $X\lesssim Y$, if there exists an injection from $X$ to $Y$.

*Say $X$ and $Y$ have the same cardinality, denoted $X\sim Y$, if there exists a bijection from $X$ to $Y$.


Primitive Notion. We take the natural numbers $\mathbb{N}$ as a primitive notion. In particular, we assume the well-ordering principle.
Definition. Let $X$ be a set.


*

*Say $X$ is finite if there exists $n\in\mathbb{N}$ such that $X\lesssim\{1,\ldots,n\}$.

*If $X$ is finite, then the cardinality of $X$, denoted $\#X$, is $\min\{n\in\mathbb{N}:X\lesssim\{1,\ldots,n\}\}$. That is to say, the cardinality of $X$ is the least natural number $n$ satisfying $X\lesssim\{1,\ldots,n\}$.


Lemma. The following can be proven by induction.


*

*$\mathbb{N}=\{n\in\mathbb{N}:(\forall S)[S\subseteq \{1,\ldots,n\}\lesssim S\:\Rightarrow\:S=\{1,\ldots,n\}]\}$

*$\mathbb{N}=\{n\in\mathbb{N}:(\forall S)[S\lesssim\{1,\ldots,n\}\:\Rightarrow\:(\exists m\le n)[S\sim \{1,\ldots,m\}]]\}$
Theorem. Let $X$ be a finite set. Then $\{n\in\mathbb{N}:X\sim \{1,\ldots,n\}\}=\{\#X\}$. That is to say, every finite set has a unique cardinality, namely, $\# X$.
Proof Outline. Use the first lemma to show the $\subseteq$ direction of the theorem. Use the second lemma to show the $\supseteq$ direction of the theorem.
