[proofplan]
We locate the fixed point as a distinguished supremum. Consider $E := \{x \in X : x \leq f(x)\}$, the set of elements that are below their own $f$-image; completeness of $X$ gives $s := \sup E$. Order-preservation of $f$ forces $s \leq f(s)$ (because each element of $E$ sits below $f(s)$, so $f(s)$ is an upper bound of $E$) and, applying $f$ once more, $f(s) \leq s$ (because $f(s)$ is then also in $E$). The two inequalities yield $f(s) = s$.
[/proofplan]
[step:Introduce the pre-fixed set $E$ and its supremum]
Define
\begin{align*}
E := \{x \in X : x \leq f(x)\} \subseteq X.
\end{align*}
Since $(X, \leq)$ is a complete poset, every subset of $X$ — in particular $E$ — admits a supremum in $X$. Set
\begin{align*}
s := \sup E \in X.
\end{align*}
[guided]
The strategy is to find a point $s \in X$ with $f(s) = s$ by exhibiting two inequalities $s \leq f(s)$ and $f(s) \leq s$ and using antisymmetry. Both inequalities will be proved simultaneously if we pick $s$ with care.
Which candidate should we pick? The inequality $s \leq f(s)$ suggests considering the set
\begin{align*}
E := \{x \in X : x \leq f(x)\} \subseteq X,
\end{align*}
of elements sitting below their own $f$-image. Note $E$ is non-empty if the poset has a least element (since any least element $\bot$ satisfies $\bot \leq f(\bot)$), but the argument below does not require that — we only use completeness of $X$.
By completeness of $(X, \leq)$, every subset of $X$ admits a least upper bound. In particular, $\sup E$ exists in $X$; define
\begin{align*}
s := \sup E \in X.
\end{align*}
Intuitively, $s$ is the largest "approach from below" — the supremum of all points that move up under $f$. The candidate fixed point will be $s$ itself.
[/guided]
[/step]
[step:Show that $s \leq f(s)$ by proving $f(s)$ is an upper bound of $E$]
Let $x \in E$ be arbitrary. Since $s$ is an upper bound of $E$, we have $x \leq s$. Applying $f$ and using order-preservation:
\begin{align*}
f(x) \leq f(s).
\end{align*}
By the definition of $E$, $x \leq f(x)$. Chaining:
\begin{align*}
x \leq f(x) \leq f(s).
\end{align*}
Thus $f(s)$ is an upper bound of $E$. Since $s = \sup E$ is the least upper bound, $s \leq f(s)$.
[guided]
The goal of this step is to show $s \leq f(s)$. Since $s$ is the **least** upper bound of $E$, it suffices to demonstrate that $f(s)$ is **some** upper bound of $E$ — then $s \leq f(s)$ follows from the defining property of the supremum.
So fix an arbitrary $x \in E$ and aim to prove $x \leq f(s)$. We have two facts at our disposal:
1. $x \leq s$, because $s$ is an upper bound of $E$.
2. $f$ is order-preserving, so inequality (1) yields $f(x) \leq f(s)$.
We also know $x \in E$ means $x \leq f(x)$ by the very definition of $E$. Chaining the two inequalities via transitivity of $\leq$:
\begin{align*}
x \leq f(x) \leq f(s).
\end{align*}
Since $x \in E$ was arbitrary, every element of $E$ lies below $f(s)$, so $f(s)$ is an upper bound of $E$. By the least upper bound property of $s = \sup E$:
\begin{align*}
s \leq f(s).
\end{align*}
Observe where order-preservation was used: it is the **only** hypothesis on $f$ that has been consumed so far. If $f$ were not order-preserving, we could not transport $x \leq s$ to $f(x) \leq f(s)$, and the argument collapses.
[/guided]
[/step]
[step:Show that $f(s) \leq s$ by placing $f(s)$ inside $E$]
From the previous step, $s \leq f(s)$. Applying the order-preserving map $f$ to both sides:
\begin{align*}
f(s) \leq f(f(s)).
\end{align*}
This is precisely the condition that $f(s) \in E$. Since $s = \sup E$ is an upper bound of $E$, we conclude $f(s) \leq s$.
[guided]
We just established $s \leq f(s)$ — now we seek the reverse inequality $f(s) \leq s$. The direct approach would again use supremum properties: $s$ is an upper bound of $E$, so $y \leq s$ for every $y \in E$. Thus it suffices to show $f(s) \in E$.
An element $y \in X$ belongs to $E$ iff $y \leq f(y)$. So we need $f(s) \leq f(f(s))$. But this follows immediately from Step 2 and order-preservation: applying $f$ to the inequality $s \leq f(s)$ gives
\begin{align*}
f(s) \leq f(f(s)).
\end{align*}
Hence $f(s) \in E$. Since every element of $E$ is bounded above by $s = \sup E$:
\begin{align*}
f(s) \leq s.
\end{align*}
Note the circular-seeming nature of this step: we used $s \leq f(s)$ (itself coming from $s$ being the supremum of $E$) to prove $f(s) \in E$, and then used the supremum property again to get $f(s) \leq s$. This double use of the supremum is the heart of the argument.
[/guided]
[/step]
[step:Conclude $f(s) = s$ by antisymmetry]
Steps 2 and 3 give $s \leq f(s)$ and $f(s) \leq s$. By antisymmetry of the partial order,
\begin{align*}
f(s) = s,
\end{align*}
so $s$ is a fixed point of $f$. This completes the proof.
[/step]
