How axiom of substitution implies unique function for ordinals in Halmos book?

Question

I'm studying set theory using Halmos's book. I'm stopping at the chapter 19 about ordinal numbers.

I have 2 questions please:

1. Is the axiom of substitution necessary in the definition of ordinal number ? (provided that Halmos introduced axiom of substitution before giving definition of ordinal number)
2. How to use the axiom of substitution to prove that there exists a unique function $F$ on $\omega$ such that $F(0) = \omega$ and $F(n^+) = (F(n))^+$ for each natural number $n$.

Thank you very much for your help!

-------------- Below is the context in the book --------------

In his exposition, at first, the author starts with definition of $\omega$-successor function:

Let us say that a function $f$ whose domain is the set of strict predecessors of some natural number $n$ (in other words, dom$f$ = $n$) is an $\omega$-successor function iff(0) = $\omega$ (provided that $n \neq 0$, so that $0 \lt n$), and $f(m^+) = (f(m))^+$ whenever $m^+ < n$. Here $\omega$ is the set of all natural numbers.

Then he states the axiom of substitution:

Axiom of substitution: If $S(a, b)$ is a sentence such that for each $a$ in a set $A$ the set {$b:S(a, b)$} can be formed, then there exists a function $F$ with domain $A$ such that $F(a) =$ {$b: S(a, b)$} for each $a \in A$

Then he gives the definition of ordinal number:

An ordinal number is defined as a well ordered set $\alpha$ such that $s(t) = t$ for all $t \in \alpha$. Note that here $s(t)$ is the initial segment {$ x \in \alpha: x \lt t$}.

Finally, he said that:

The axiom of substitution implies easily that there exists a unique function $F$ on $\omega$ such that $F(0) = \omega$ and $F(n^+) = (F(n))^+$ for each natural number $n$.

Answer 1

Q.1: you may want to have a look at the Wikipedia entry

Q.2: you may want to reread the second paragraph of the section, where Halmos says explicitly:

Let $S(n, x)$ be the sentence that says "$n$ is a natural number and $x$ belongs to the range of the $\omega$ -successor function with domain $n$."

So the sentence can be formed for $\omega$, the hypothesis of axiom of substitution is satisfied, so by the axiom there exists a unique function $F$ on $\omega$ etc., no further proof is needed.

To the comment:

I don’t think your problem is with the application of axiom of substitution, since a short comparison will ensure you that the axiom’s hypothesis is indeed satisfied:

Axiom of substitution: $S(a, b)$ is a sentence...

The definition of $F$: $S(n, x)$ is a sentence...

Axiom of substitution: ...such that for each $a$ in a set $A$ the set {$b:S(a, b)$} can be formed.

The definition of $F$: The author himself says «[w]e know that for each natural number $n$ we are permitted to form the set ».