I am trying to formally construct the usual partial ordering LTE from Peano's 5 Axioms. Would the following construction work?
$$\forall a,b: [(a,b)\in LTE \iff(a,b)\in N^2$$
$$\land ~ \forall c\subset N^2:[\forall d\in N: [(d,d) \in c]$$
$$ \land ~ \forall d,e:[(d,e)\in c \implies(d, S(e))\in c]$$
$$\implies (a,b) \in c]]$$
where $N$ is the set of natural numbers and $S$ is the usual successor function on $N$.
Informally, for all $x,y\in N$, we can recursively define $\le$ on $N$ as the "smallest" set of ordered pairs of natural numbers that satisfies:
$$x \le x$$
$$x\le y \implies x\le S(y)$$