Suppose $A=B=\mathbb{Z_+}\times\mathbb{Z_+}$ where $\mathbb{Z_+}$ is the positive integers; let $<$ be the "usual order relation." Let $<_A$ be the dictionary order relation and let $<_B$ be the order relation defined by the following rule: $(x_0,y_0)<_B(x_1,y_1)$ if either $x_0+y_0<x_1+y_1$, or $x_0+y_0=x_1+y_1$ and $y_0<y_1.$
As the title states, I'm trying to show $\mathbb{Z_+}\times\mathbb{Z_+}$ in the dictionary order relation $<_A$ has a different order type than $\mathbb{Z_+}\times\mathbb{Z_+}$ in the order relation just defined above, $<_B$.
My proof seems a bit easier than I would have thought and I'm unsure I'm allowed set theoretically to do what I'm doing.
$$$$
I argued that we assume for a contradiction that $A$ and $B$ indeed have the same order type, so that there exists a bijection $f:A\to B$ such that $a_0<_Aa_1\implies f(a_0)<_Bf(a_1)$. Then let $a_0=(1,1)$ and $a_1=(2,1)$, which have no immediate predecessors, so that $a_0<_Aa_1\implies f(a_0)<_Bf(a_1)$.
However, every element in $(B,<_B)$ has an immediate successor (and predecessor, except the least element of $B$ ) so there is a finite number of elements $f(z)$ such that $f(a_0)<_Bf(z)<_Bf(a_1)$ for $z\in A,$ but an infinite number of $z$ such that $a_0<_Az<_Aa_1$. Thus there exists $z_\epsilon\in A$ such that $a_0<_Az_\epsilon<_Aa_1$ and $f(a_0)\not<_Bf(z_\epsilon)\not<_Bf(a_1)\therefore$ contradiction.
Thus $A$ and $B$ don't have the same order type since no such bijection can exist. QED.
$$$$ I'm concerned with the highlighted piece and the deduction via cardinality. Any check would be appreciated. Thanks!