I am currently self-studying "The Real Numbers and Real Analysis" by Bloch, and I am having a hard time understanding a particular part of the proof for the following Theorem (my question is at the bottom).
Theorem 1: There is a unique binary operation +: $\mathbb{N}\rightarrow\mathbb{N}$ that satisfies the following two properties for all n,m $\in\mathbb{N}$
1) $n+1=s(n)$
2) $n+s(m)=s(n+m)$
The following, definitions, axiom, lemma, and theorem can be used to prove this theorem as they came before the theorem.
Definition: Let S be a set. A binary operation on S is a function S$\times$S$\rightarrow$S
Axiom:There exists a set $\mathbb{N}$ with an element 1 $\in\mathbb{N}$ and a function $s: \mathbb{N}\rightarrow\mathbb{N}$ that satisfy the following three properties.
1) There is no n $\in\mathbb{N}$ such that $s(n)=1$
2)The function $s$ is injective
3)Let $G\subseteq\mathbb{N}$ be a set. Suppose 1 $\in G$, and that if g $\in G$ then $s(g)\in G$. Then $G=\mathbb{N}$
Lemma: suppose $a\in\mathbb{N}$. Suppose $a\neq1$, then there is a unique $b\in\mathbb{N}$ such that $a=s(b)$
Theorem 2 (Definition by Recursion): Let $H$ be a set, let $e\in H$ and let $k: H\rightarrow H$ be a function . Then there is a unique function $f:\mathbb{N}\rightarrow H$ such that $f(1)=e$ and $f(s(n))=k(f(n))$
The following is the beginning of the proof for existence of Theorem 1 given in the book. I have only shown up to where I have problems. I have indicated with quotation marks the part I am having trouble with ( I am not use to mathjax).
Proof: Suppose $p\in\mathbb{N}$. We can apply the Definition by Recursion to the set $\mathbb{N}$,"the element $s(p)\in\mathbb{N}$", and the function $s:\mathbb{N}\rightarrow\mathbb{N}$ to deduce that there is a unique function $f_p:\mathbb{N}\rightarrow\mathbb{N}$ such that $f_p(1)=s(p)$ and $f_p(s(n))=s(f_p(n))$...
Why is $s(p)\in\mathbb{N}$? I do realize the function $s$ is defined as $s:\mathbb{N}\rightarrow\mathbb{N}$, so the output of the function $s$ must be in $\mathbb{N}$, but how do we know $s(p)$ is defined from the above info. The only reason I can think of is we can assume that for any $p$ , $s(p)$ is defined, but I am not convinced because the axiom says that function is only injective, not bijective, and I do not know how to prove its bijective. I do not think I need to prove its bijective because the text doesn't.
This has nothing to do with bijectivity. It is simply that $p \in \mathbb{N}$ (by assumption). That is, $p$ is in the domain of $s$. Look at your axiom defining $s$. It states that $s$ is a function whose domain is $\mathbb{N}$ and whose codomain is $\mathbb{N}$. That means for each $p \in \mathbb{N}$, $s(p) \in \mathbb{N}$.