How to prove $\forall k \exists y \forall x (x < y \Leftrightarrow \forall n (n < x \Rightarrow n < k))$?

It's helpful to simplify things a bit by figuring out what the analogue of "$\subseteq$" is in this context.

• This is a useful principle in general. Suppose I have a sentence $\varphi$ which is well-understood and true in some structure $\mathcal{A}$, and I want to figure out if $\varphi$ is also true in some other structure $\mathcal{B}$. The sentence $\varphi$ itself may be sufficiently complicated that I can't immediately tell what it means in the context of $\mathcal{B}$, but this can be mitigated by approaching $\varphi$ as something built out of simpler concepts whose "translation to $\mathcal{B}$" is easier to figure out. In the present case, "set of all subsets of" is easier to parse than "set of all sets whose elements are all elements of."

Remember that $\subseteq$ is the relation defined by $$x\subseteq y\quad\iff\quad\forall z(z\in x\implies z\in y).$$ If we replace "$\in$" with "$<$," the corresponding "arithmetic subset" notion - which I'll denote "$\sqsubseteq$" - is defined by $$x\sqsubseteq y\quad\iff\quad \forall z(z<x\implies z<y).$$ That right hand side is something we can simplify quite well: "every number $<x$ is also $<y$" is just a complicated way of saying $\color{red}{x\le y}$.

---

So now let's look back at the powerset axiom. In somewhat abbreviated form, it says

For every $x$, there is some $y$ such that for all $z$ we have $$z\in y\quad\iff\quad z\subseteq x.$$

Replacing "$\in$" with "$<$" and using our characterization of "$\sqsubseteq$" above, the "arithmetic powerset principle" is the statement

For every natural number $a$, there is some natural number $b$ such that for all natural numbers $c$ we have $$c<b\quad\iff\quad c\le a.$$

Does every $a$ in fact have such a $b$? (HINT: there's a crucial difference here between this question and the analogous question with $\mathbb{N}$ replaced with $\mathbb{R}_{\ge 0}$ ...)