A set $N$ is defined with some axioms, where $P$ and $Q$ are two of the axioms.
I am trying to prove a statement $P\rightarrow Q$ to show that $Q$ is redundant. I'm doing this by using the contrapositive. So, I assumed $\neg Q$. I defined a function $f:N \rightarrow N$ which is definitely well-defined. It can be showed that the definition of $f$ implies $\neg P$. So, $\neg Q \rightarrow \neg P$ or at least that is what I think it is.
I'm worried about making a function that contradicts an axiom of the set it's defined on. Am I doing this correctly?
EDIT: If $Q$ is also used to construct $N$, then the proof is likely invalid. The below assumes only $P$ is used to construct $N$.
I assume that you mean that you assumed axiom $P$ in the construction of the set $N$; that is, that without axiom $P$, you wouldn't be able to prove that $N$ existed in the first place.
I see that as you clarified in the comments, you are no longer assuming $P$ is an axiom (otherwise you would just prove the statement $Q$, instead of trying to prove $P \to Q$).
Your proof is correct, but you are right that it's a bit fishy. Specifically, it is not a proof by contrapositive -- it's a proof by contradiction!
Let's discuss why this is. You assumed $\lnot Q$, but you also defined the function $f: N \to N$. In order to define it, you needed to assume $P$. So you are not really just assuming $\lnot Q$. You are assuming $\boldsymbol{P}$ and $\boldsymbol{\lnot Q}$. That's the form of a proof by contradiction.
Then, when you arrive at the conclusion that the definition of $f$ implies $\lnot P$, this contradicts your earlier assumption $P$ (you assumed $P$ and not $Q$). That is, it is impossible for $P$ to hold and not $Q$, which is the same as saying that $P$ implies $Q$ ($P \to Q$).
Essentially your worry is correct -- but your proof ends up being right anyway, as long as you phrase it as a proof by contradiction instead of a proof by contrapositive.