Proof that order-isomorphisms are bijective I'm reading the Davey and Priestley's Introduction to Lattices and Order. On page 3, it is said that order-isomorphism is necessarily bijective. I thought we could easily prove the claim given the definition of order-isomorphism. However the book gave the following proof (the function $\phi$ is a function from set $P$ onto set $Q$ such that $x \le $y iff $\phi(x) \le \phi(y)$: 
\begin{align*}
 \phi(x) = \phi(y) &\Leftrightarrow \phi(x) \le \phi(y) \;\&\; \phi(y) \le \phi(x) \\
                   &\Leftrightarrow x \le y \;\&\; y \le x \\
                   &\Leftrightarrow x = y
\end{align*}
Could anyone please help me understand why this proves that order-isomorphism is bijective? Is it because in a set, any element is equal to itself, which implies the function $\phi$ is injective? 
Thanks, 
 A: Almost by definition (use (i) and (ii) of Davey and Priestley's definition), if $(P,\leq)$ is a partial order then for all $p,q\in P$ we have $p\leq q ~\&~ q\leq p$ if and only if $p=q$.
In Davey and Priestley's Introduction to Lattices and Orders they define an order isomorphism from a partial order $(P,\leq_P)$ to a partial order $(Q,\leq_Q)$ to be a surjective (onto) map $\phi:P\to Q$ such that for all $p,p'\in P$  $p\leq_P p'$ iff $\phi(p)\leq_Q \phi(p')$. 
Now recall that a map $\phi:P\to Q$ between sets $P$ and $Q$ is injective if for all $p,p'\in P$ $\phi(p)=\phi(p')$ implies $p=p'$.
To show that any order isomoprhism $\phi:(P,\leq_P)\to (Q,\leq_Q)$ is bijective, it is enough to show that it is injective (since it is surjective by definition). So let $p,p'\in P$ and suppose that $\phi(p)=\phi(p')$. By our first remark, this is equivalent to $\phi(p)\leq_Q \phi(p')~ \&~\phi(p')\leq_Q \phi(p)$. By definition of an order isomorphism, this implies (is in fact equivalent) to $p\leq_P p'~\&~p'\leq_P p$. This again by our first remark implies (is equivalent to) $p=p'$.
