Using induction to prove a natural number property Suppose that the natural numbers are defined as:
$\mathrm{P} 1)$ $1 \in \mathbb{N}$
$\mathrm{P} 2) \forall n \in \mathbb{N}, f(n) \neq 1 ;$
$\mathrm{P} 3)$ $f$ is injective
$\mathrm{P} 4)$ A subset $A \subset \mathbb{N}$ satisfies:
a) $1 \in A$
b) $\forall n \in \mathbb{N}, n \in A \text { implies } f(n) \in A$
And now $f$ is defined as $f(1) =2 , f(f(1))=3 , f(f(f(1)))=4, ...$
And I want to prove that For any $n ∈ \mathbb{N}, n \neq 1$, show that there exists a unique $n' ∈ \mathbb{N}$, such that $n = f(n')$.
My attempt:
Let $P(n)$ denote that there exists a unique $n' ∈ \mathbb{N}$, such that $n = f(n')$ for any $n ∈ \mathbb{N}, n \neq 1$
Base case: suppose $n=2$, then there exists a unique $n'=1 ∈ \mathbb{N}$, such that $2 = f(1)$. by $P2)$, $1$ is unique.
Inductive: assume $P(n)$ true, show $P(n+1)$ true:
Denote $n+1$ as applying the successor function $f$, From $n = f(n')$, apply the successor function to both sides, that is: $f(n) = f(f(n'))$ $(*)$, using the induction hypothesis, the right side $f(f(n'))=f(n)$, so by $(*)$,$f(n)=f(n)$, since $f$ is injective, $P(n+1)$ is true.
So by induction, $P(n)$ is true.
Did I do this proof correctly? I feel like for the inductive step, not mentioning uniqueness is wrong. Any help is appreciated.
 A: Well, uniqueness comes from injectivity of the successor function (axiom 3). So once you've found some $n'$ with $f(n')=n$, you know this $n'$ is unique.
You do need to include this for a fully rigorous proof, but it's literally just a single extra line.

There is a subtlety you've missed with the induction step. Not one that invalidates the logic, but it does contribute to your proof looking and feeling somewhat confused, and also demonstrates some lack of understanding.
This subtlety is that you never really need to use the $n'$ that is the unique number with $f(n')=n$. The statement you are trying to prove - $P(n)$ - just says that there is some number $m$ with $f(m)= n+1$... and that number is $n$. Starting by looking at the $n'$ and then applying $f$ to it like you did just takes you around the back alley before bringing you right back to where you should have started.

(Given that you've started with the axiomatic definition of the naturals, you may also want to have a lemma that let's you start the induction at $2$, since the induction axiom P4 you've written (and omitted an important part of: check it again) only allows induction starting at $1$.)
