equivalence of two definitions of cardinality

Question

The following is an attempt to verify the agreement of two definitions. My concerns are in blockquotes.

Definition 1
Let $n\geq1$ be a natural number, and $X$ be a set. We define the cardinality $|X|$ of $X$ to be $n$ if there is a bijection from $X$ to the set $\{1,2,\ldots,n\}$. The cardinality of the empty set is defined to be $0$.

Definition 2
We can define the cardinality $|X|$ of a finite set $X$ recursively as follows:

• The cardinality of the empty set is $0$.
• The cardinality of a set $X$ is $n+1$ if there exists $x\in X$ such that $|X\setminus\{x\}|=n$

Proof

Let $|X|_1$ and $|X|_2$ denote the cardinality of a finite set $X$ according to definitions 1 and 2, respectively. We need to prove using induction that $|X|_1=|X|_2$ for all $n\geq0$.

1. For $n=0$, we have $|X|_1=0\Leftrightarrow X=\emptyset\Leftrightarrow |X|_2=0$ by definition. Hence, the definitions agree.

Definitions 1 and 2 only say that $X=\emptyset \Rightarrow |X|=0$, so the converse may be false. Non-empty sets with cardinality $0$ are permissible, according to these definitions. How can I establish the $n=0$ case without the opposite? I avoided the converse for the inductive step below.

2. Assume the result for $|X|_1=n\Leftrightarrow|X|_2=n$.

3. For $b\notin X$ let $X\cup\{b\}=B\Leftrightarrow X=B\setminus\{b\}$.

4. Therefore, there exists $b\in B$ such that $|B\setminus\{b\}|_2=|X|_2=n$. Hence, we can infer that $|B|_2=n+1$.

Here I avoided beginning with $|B|_2=n+1$ to get $|B\backslash\{b\}|_2=n$ because that assumes the converse. Definition 2 allows sets $C$ such that $|C|_2=n+1$ but $|C\setminus\{c\}|_2\neq n$ for $c\in C$.

5. From (2) we have that there exists a bijection $f$ from $X$ to $\{1,2,\ldots,n\}$.
6. Define $g$ from $X\cup\{b\}$ to $\{1,2,\ldots,n,n+1\}$ as:
   • for $u\in X$ let $g(u)=f(u)$
   • for $u\in\{b\}$ let $g(u)=n+1$
7. As defined, $g$ has an inverse:
   • for $1\leq m\leq n$ let $g^{-1}(m)=f^{-1}(m)$
   • for $m=n+1$ let $g^{-1}(m)=b$
8. Therefore, there is a bijection $g$ from $B$ to $\{1,2,\ldots,n+1\}$. Hence, we can infer that $|B|_1=n+1$.

Again, I did not begin with $|B|_1=n+1$ to get a bijection $g$ from $B$ to $\{1,2,\ldots,n+1\}$. Definition 1 allows sets $C$ such that $|C|_1=n$ without any bijection from $C$ to $\{1,2,\ldots,n\}$.

9. Hence, we have $|B|_1=n+1\Leftrightarrow|B|_2=n+1$ from $|X|_1=n\Leftrightarrow|X|_2=n$.

From (1) and (9), we conclude that the definitions are equivalent for all $n\in \mathbb{N}$.

I avoided the converse for the inductive step, but how should I prove the first case? Also, please let me know if there are other problems.