[proofplan] We construct the canonical vertex map sending each nonempty face $\sigma$ of $K$ to the barycentric vertex $b_\sigma$ indexed by that face. The definition of the order complex says that its simplices are exactly finite strict chains of nonempty faces of $K$. The definition of the barycentric subdivision gives the same simplices, with the elements of the chain renamed as barycentric vertices. Therefore the canonical vertex bijection preserves and reflects simplices, which is precisely an isomorphism of abstract simplicial complexes. [/proofplan] [step:Define the canonical vertex map] Let $V(\operatorname{sd} K)$ denote the vertex set of the barycentric subdivision of $K$. By definition of the abstract barycentric subdivision, its vertices are indexed by the nonempty faces of $K$: \begin{align*} V(\operatorname{sd} K)=\{b_\sigma : \sigma \in K,\ \sigma \ne \varnothing\}. \end{align*} Define \begin{align*} \Phi: F_{\ne \varnothing}(K) \to V(\operatorname{sd} K) \end{align*} by \begin{align*} \Phi(\sigma)=b_\sigma. \end{align*} Since every vertex of $\operatorname{sd} K$ has the form $b_\sigma$ for a unique nonempty face $\sigma$ of $K$, the map $\Phi$ is a bijection on vertices. [/step] [step:Identify order-complex simplices with strict chains of nonempty faces] By definition of the order complex of a poset, a finite subset \begin{align*} \{\sigma_0,\dots,\sigma_k\}\subset F_{\ne \varnothing}(K) \end{align*} is a simplex of $\Delta(F_{\ne \varnothing}(K))$ if and only if its elements can be ordered to form a chain in $F_{\ne \varnothing}(K)$. Since the order on $F_{\ne \varnothing}(K)$ is inclusion, this means precisely that, after reindexing if necessary, the faces satisfy \begin{align*} \sigma_0 \subsetneq \sigma_1 \subsetneq \cdots \subsetneq \sigma_k. \end{align*} Thus the simplices of $\Delta(F_{\ne \varnothing}(K))$ are exactly the finite strict chains of nonempty faces of $K$. [guided] Let us unpack the definition being used. The vertices of $\Delta(F_{\ne \varnothing}(K))$ are the elements of the poset $F_{\ne \varnothing}(K)$, so a vertex is a nonempty face $\sigma$ of $K$. A simplex in the order complex is a finite set of vertices that is totally ordered by the poset relation. Here the poset relation is inclusion of faces. Therefore a finite subset \begin{align*} \{\sigma_0,\dots,\sigma_k\}\subset F_{\ne \varnothing}(K) \end{align*} is a simplex of the order complex exactly when its elements can be indexed so that each one is properly contained in the next: \begin{align*} \sigma_0 \subsetneq \sigma_1 \subsetneq \cdots \subsetneq \sigma_k. \end{align*} The containments are strict because the displayed set has distinct vertices; repeating the same face would not give a new vertex of an abstract simplex. Hence a simplex of the order complex is not extra structure beyond a chain of faces. It is exactly a finite strict chain of nonempty faces of $K$. [/guided] [/step] [step:Identify barycentric-subdivision simplices with the same chains] By definition of the abstract barycentric subdivision, a finite subset \begin{align*} \{b_{\tau_0},\dots,b_{\tau_k}\}\subset V(\operatorname{sd} K) \end{align*} is a simplex of $\operatorname{sd} K$ if and only if the corresponding nonempty faces of $K$ can be ordered into a strict inclusion chain. Equivalently, after reindexing if necessary, \begin{align*} \tau_0 \subsetneq \tau_1 \subsetneq \cdots \subsetneq \tau_k. \end{align*} Thus the simplices of $\operatorname{sd} K$ are exactly the finite sets of barycentric vertices indexed by strict chains of nonempty faces of $K$. [/step] [step:Conclude that the canonical vertex bijection is a simplicial isomorphism] Let \begin{align*} S=\{\sigma_0,\dots,\sigma_k\} \end{align*} be a finite subset of $F_{\ne \varnothing}(K)$. By the preceding two steps, $S$ is a simplex of $\Delta(F_{\ne \varnothing}(K))$ if and only if the elements of $S$ can be ordered as a strict inclusion chain, and this holds if and only if \begin{align*} \Phi(S)=\{b_{\sigma_0},\dots,b_{\sigma_k}\} \end{align*} is a simplex of $\operatorname{sd} K$. Therefore $\Phi$ preserves simplices and reflects simplices. Since $\Phi$ is also a bijection on vertices, it extends uniquely to an isomorphism of abstract simplicial complexes \begin{align*} \Delta(F_{\ne \varnothing}(K)) \cong \operatorname{sd} K. \end{align*} The construction depends only on the face $\sigma$ and sends it to its corresponding barycentric vertex $b_\sigma$, so the isomorphism is natural in the stated sense. [/step]