[proofplan]
We compare the Möbius recursion on the interval $[x,y]_P$ with the Möbius recursion on the reversed interval $[y,x]_{P^{\mathrm{op}}}$. Local finiteness passes to the dual because the two intervals have the same underlying finite set. We prove the equality by induction on the cardinality of $[x,y]_P$, using the upper-endpoint recursion for $\mu_P$ and the lower-endpoint recursion in the dual poset.
[/proofplan]
[step:Transfer local finiteness and identify the reversed interval]
For elements $a,b \in P$, write $a \le_{\mathrm{op}} b$ when $b \le a$ in $P$. Let $x,y \in P$ satisfy $x \le y$ in $P$. The interval of $P$ from $x$ to $y$ is
\begin{align*}
[x,y]_P=\{z\in P:x\le z\le y\}.
\end{align*}
The corresponding interval of $P^{\mathrm{op}}$ from $y$ to $x$ is
\begin{align*}
[y,x]_{P^{\mathrm{op}}}=\{z\in P:y\le_{\mathrm{op}} z\le_{\mathrm{op}} x\}.
\end{align*}
By the definition of the opposite order, the condition $y\le_{\mathrm{op}} z\le_{\mathrm{op}} x$ is equivalent to $x\le z\le y$ in $P$. Hence
\begin{align*}
[y,x]_{P^{\mathrm{op}}}=[x,y]_P
\end{align*}
as underlying sets.
Since $P$ is locally finite, $[x,y]_P$ is finite. Therefore $[y,x]_{P^{\mathrm{op}}}$ is finite. As this holds for every comparable pair in $P^{\mathrm{op}}$, the dual poset $P^{\mathrm{op}}$ is locally finite, so its Möbius function $\mu_{P^{\mathrm{op}}}$ is defined.
[/step]
[step:Prove the identity by induction on the interval size]
Let $C_P:=\{(u,v)\in P\times P:u\le v\}$ be the set of comparable ordered pairs in $P$. Define the interval-size function
\begin{align*}
N:C_P &\to \mathbb{N}
\end{align*}
by
\begin{align*}
N(u,v)=|[u,v]_P|.
\end{align*}
For the fixed pair $x\le y$ in $P$, we prove the desired identity by induction on $N(x,y)$.
If $N(x,y)=1$, then $x=y$. The diagonal normalization in the recursive definition of the Möbius function gives
\begin{align*}
\mu_{P^{\mathrm{op}}}(x,x)=1=\mu_P(x,x).
\end{align*}
Thus the result holds in the base case.
Assume now that $x<y$ in $P$, and assume the identity has been proved for every interval of cardinality strictly smaller than $N(x,y)$. Since $y<_{\mathrm{op}} x$ in $P^{\mathrm{op}}$, the lower-endpoint recursion for the Möbius function, as in [citetheorem:8101], applied in the locally finite poset $P^{\mathrm{op}}$ gives
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,x)=-\sum_{y\le_{\mathrm{op}} z<_{\mathrm{op}} x}\mu_{P^{\mathrm{op}}}(y,z).
\end{align*}
The indexing condition $y\le_{\mathrm{op}} z<_{\mathrm{op}} x$ is equivalent to $x<z\le y$ in $P$. Hence
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,x)=-\sum_{x<z\le y}\mu_{P^{\mathrm{op}}}(y,z).
\end{align*}
For each $z$ with $x<z\le y$, the interval $[z,y]_P$ is a proper subinterval of $[x,y]_P$, so $N(z,y)<N(x,y)$. By the induction hypothesis,
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,z)=\mu_P(z,y).
\end{align*}
Substituting this into the previous display yields
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,x)=-\sum_{x<z\le y}\mu_P(z,y).
\end{align*}
The upper-endpoint Möbius recursion in $P$, also supplied by [citetheorem:8101], says that, for $x<y$,
\begin{align*}
\sum_{x\le z\le y}\mu_P(z,y)=0.
\end{align*}
Separating the term $z=x$ gives
\begin{align*}
\mu_P(x,y)=-\sum_{x<z\le y}\mu_P(z,y).
\end{align*}
Therefore
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,x)=\mu_P(x,y).
\end{align*}
[guided]
We prove the identity by induction on the finite number of elements in the interval. Let $C_P:=\{(u,v)\in P\times P:u\le v\}$ be the set of comparable ordered pairs in $P$. Define the interval-size function
\begin{align*}
N:C_P &\to \{1,2,3,\dots\}
\end{align*}
by
\begin{align*}
N(u,v)=|[u,v]_P|.
\end{align*}
For every $(u,v)\in C_P$, this value is finite because $P$ is locally finite.
The smallest possible interval has $N(x,y)=1$. In that case $x=y$, and both Möbius functions are evaluated on the diagonal. The defining normalization gives
\begin{align*}
\mu_{P^{\mathrm{op}}}(x,x)=1
\end{align*}
and
\begin{align*}
\mu_P(x,x)=1.
\end{align*}
Hence the desired equality holds when the interval has one element.
Now suppose $x<y$ in $P$, and assume the equality is already known for every interval whose cardinality is smaller than $N(x,y)$. In the opposite poset, the inequality reverses, so $y<_{\mathrm{op}} x$. The lower-endpoint recursion for the Möbius function, as stated in [citetheorem:8101], applies in $P^{\mathrm{op}}$ because the preceding step proved that $P^{\mathrm{op}}$ is locally finite. It gives
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,x)=-\sum_{y\le_{\mathrm{op}} z<_{\mathrm{op}} x}\mu_{P^{\mathrm{op}}}(y,z).
\end{align*}
We now translate the indexing set back into the order of $P$. The condition $y\le_{\mathrm{op}} z$ means $z\le y$ in $P$, while the condition $z<_{\mathrm{op}} x$ means $x<z$ in $P$. Therefore the summation is over exactly those $z\in P$ satisfying $x<z\le y$. Thus
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,x)=-\sum_{x<z\le y}\mu_{P^{\mathrm{op}}}(y,z).
\end{align*}
For every such $z$, the interval $[z,y]_P$ is strictly smaller than $[x,y]_P$, because $x$ belongs to $[x,y]_P$ but not to $[z,y]_P$. Hence $N(z,y)<N(x,y)$, so the induction hypothesis applies to the pair $z\le y$. It gives
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,z)=\mu_P(z,y).
\end{align*}
Substituting this equality into the recursion in the dual poset gives
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,x)=-\sum_{x<z\le y}\mu_P(z,y).
\end{align*}
The final point is that this is exactly the upper-endpoint recursion for $\mu_P(x,y)$. By [citetheorem:8101], the Möbius function satisfies both endpoint recursions in every locally finite poset. Since $P$ is locally finite and $x<y$, we may use the upper-endpoint form
\begin{align*}
\sum_{x\le z\le y}\mu_P(z,y)=0.
\end{align*}
The term with $z=x$ is $\mu_P(x,y)$, so moving all other terms to the other side gives
\begin{align*}
\mu_P(x,y)=-\sum_{x<z\le y}\mu_P(z,y).
\end{align*}
Comparing the two formulas proves
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,x)=\mu_P(x,y).
\end{align*}
[/guided]
[/step]
[step:Conclude for all comparable pairs]
The induction establishes the identity for every pair $x,y\in P$ with $x\le y$. Therefore, for all such pairs,
\begin{align*}
\mu_{P^{\mathrm{op}}}(y,x)=\mu_P(x,y).
\end{align*}
This is precisely the asserted duality formula for Möbius functions.
[/step]
