Prove there exists a strictly increasing function from the natural numbers to a partially strictly ordered set

Question

Let $P$ be a non-empty partially strictly ordered set and assume no element of $P$ is maximal (i.e. for every $x \in P$ there exists $y\in P$ with $x < y$). Show there exists a function $f\colon\omega\to P$ with $f(n) < f(n+1)$ for all $n\in\omega$.

My thought process so far is to combine recursion with the axiom of choice to set up the function $f$ with $f(0) = x$, where $x$ is any element in $P$ and have a recursive function $f(n + 1) = g(f(n))$ where I'd use the axiom of choice for $g$ to choose a next greater element. However, I'm not sure if I'm allowed to infinitely use the axiom of choice like I think I would be here?

Answer 1

Yes, it's fine.

Note that the use of the axiom of choice is only in proving that a choice function $g$ exists, and we fix this choice function before starting the recursion. Afterwards it's just recursion.

Also note that you don't choose from $f(n)$, but rather from $\{y\mid f(n)<y\}$, which is nonempty since $f(n)$ is not maximal.

Answer 2

Yes, this is fine. In fact you don't even need the full strength of the axiom of choice: the axiom of dependent choice is all that you're really using.