[proofplan] Fix an interval isomorphism $\varphi:[x,y]_P\to [u,v]_Q$. Since an isomorphism preserves the unique minimum and maximum elements of an interval, it sends $x$ to $u$ and $y$ to $v$. We prove the stronger statement that $\mu_P(x,z)=\mu_Q(u,\varphi(z))$ for every $z\in [x,y]_P$, using induction on the finite size of the subinterval $[x,z]_P$. The recursive definition of the Möbius function then transports across $\varphi$, because $\varphi$ gives a bijection from the elements below $z$ to the elements below $\varphi(z)$. [/proofplan]

[step:Fix the interval isomorphism and record how it acts on subintervals]Let $\varphi:[x,y]_P\to [u,v]_Q$ be a poset isomorphism. Since $x$ is the unique minimum element of $[x,y]_P$ and $u$ is the unique minimum element of $[u,v]_Q$, order preservation and surjectivity imply $\varphi(x)=u$. Similarly, since $y$ and $v$ are the unique maximum elements of the two intervals, $\varphi(y)=v$. For each $z\in [x,y]_P$, define the finite subinterval $[x,z]_P=\{t\in P:x\le t\le z\}$. Local finiteness of $P$ guarantees that $[x,z]_P$ is finite. We claim that $\varphi$ restricts to a poset isomorphism $\varphi|_{[x,z]_P}:[x,z]_P\to [u,\varphi(z)]_Q$. Indeed, if $t\in [x,z]_P$, then $x\le t\le z$, so order preservation gives $u=\varphi(x)\le \varphi(t)\le \varphi(z)$. Conversely, if $w\in [u,\varphi(z)]_Q$, let $t=\varphi^{-1}(w)$. Since $u\le w\le \varphi(z)$ and $\varphi^{-1}$ is order-preserving, we obtain $x=\varphi^{-1}(u)\le t\le z$. Hence $t\in [x,z]_P$ and $\varphi(t)=w$.[/step]

[guided]We first isolate exactly what the interval isomorphism gives us. Let $\varphi:[x,y]_P\to [u,v]_Q$ be a bijection that preserves and reflects order. The element $x$ is characterized inside $[x,y]_P$ by the property that $x\le t$ for every $t\in [x,y]_P$. Because $\varphi$ preserves order and is surjective, $\varphi(x)$ has the corresponding property in $[u,v]_Q$: for every $w\in [u,v]_Q$, choosing $t=\varphi^{-1}(w)$ gives $\varphi(x)\le w$. The unique such element is $u$, so $\varphi(x)=u$. The same argument applied to maximum elements gives $\varphi(y)=v$. Now fix $z\in [x,y]_P$ and define $[x,z]_P=\{t\in P:x\le t\le z\}$. Because $P$ is locally finite, this interval is finite. We need more than endpoint preservation: the recurrence for the Möbius function sums over all elements below the upper endpoint, so we must know that $\varphi$ carries the whole subinterval below $z$ onto the whole subinterval below $\varphi(z)$. If $t\in [x,z]_P$, then $x\le t\le z$. Applying the order-preserving map $\varphi$ gives \begin{align*}u=\varphi(x)\le \varphi(t)\le \varphi(z).\end{align*} Thus $\varphi(t)\in [u,\varphi(z)]_Q$. Conversely, take $w\in [u,\varphi(z)]_Q$ and define $t=\varphi^{-1}(w)$. Since $\varphi^{-1}$ is also order-preserving, the inequalities $u\le w\le \varphi(z)$ imply \begin{align*}x=\varphi^{-1}(u)\le t\le z.\end{align*} Therefore $t\in [x,z]_P$ and $\varphi(t)=w$. This proves that $\varphi|_{[x,z]_P}$ is a poset isomorphism from $[x,z]_P$ to $[u,\varphi(z)]_Q$.[/guided]

[step:Prove equality of the transported Möbius values by induction on subinterval size] Define the auxiliary size map $N:[x,y]_P\to \mathbb N$ by letting $N(z)=|[x,z]_P|$ for each $z\in [x,y]_P$. This is well-defined because each interval $[x,z]_P$ is finite by local finiteness of $P$. We prove by strong induction on $N(z)$ that \begin{align*}\mu_P(x,z)=\mu_Q(u,\varphi(z)).\end{align*} If $N(z)=1$, then $[x,z]_P=\{x\}$, so $z=x$. Since the Möbius function has diagonal value $1$ in every locally finite poset, \begin{align*}\mu_P(x,x)=1=\mu_Q(u,u)=\mu_Q(u,\varphi(x)).\end{align*} Now let $z\in [x,y]_P$ satisfy $N(z)>1$, and assume the equality has already been proved for every $t\in [x,y]_P$ with $N(t)<N(z)$. Since $N(z)>1$, we have $x<z$. By the [recursive formula for the Möbius function](/theorems/8093) [citetheorem:8093] applied in the locally finite poset $P$ to the comparable pair $x<z$, we have \begin{align*}\mu_P(x,z)=-\sum_{x\le t<z}\mu_P(x,t).\end{align*} For every $t$ with $x\le t<z$, the inclusion $[x,t]_P\subsetneq [x,z]_P$ is proper because $z\notin [x,t]_P$, so $N(t)<N(z)$. The induction hypothesis therefore gives \begin{align*}\mu_P(x,t)=\mu_Q(u,\varphi(t)).\end{align*} Substituting this into the recurrence yields \begin{align*}\mu_P(x,z)=-\sum_{x\le t<z}\mu_Q(u,\varphi(t)).\end{align*} By the previous step, $\varphi$ gives a bijection from $[x,z]_P$ to $[u,\varphi(z)]_Q$. It restricts to a bijection from $\{t\in P:x\le t<z\}$ to $\{w\in Q:u\le w<\varphi(z)\}$: if $t<z$, then $\varphi(t)\le \varphi(z)$ and equality would imply $t=z$ by injectivity of $\varphi$, so $\varphi(t)<\varphi(z)$; the same argument applied to $\varphi^{-1}$ proves the converse. Reindexing the finite sum along this bijection gives \begin{align*}\mu_P(x,z)=-\sum_{u\le w<\varphi(z)}\mu_Q(u,w).\end{align*} Applying the recursive formula for the Möbius function [citetheorem:8093] in the locally finite poset $Q$ to the comparable pair $u<\varphi(z)$ gives \begin{align*}-\sum_{u\le w<\varphi(z)}\mu_Q(u,w)=\mu_Q(u,\varphi(z)).\end{align*} Thus $\mu_P(x,z)=\mu_Q(u,\varphi(z))$, completing the induction. [/step]

[step:Apply the transported equality to the upper endpoint] Taking $z=y$ in the result of the induction gives \begin{align*}\mu_P(x,y)=\mu_Q(u,\varphi(y)).\end{align*} Since $\varphi(y)=v$, this becomes \begin{align*}\mu_P(x,y)=\mu_Q(u,v).\end{align*} This proves that the Möbius value depends only on the isomorphism type of the interval. [/step]