[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*}[/step]

[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: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]