[proofplan] We produce a $K$-isomorphism $\bar{K} \xrightarrow{\sim} \bar{K}'$ via Zorn's lemma. Consider the poset $\mathcal{S}$ of all $K$-homomorphisms $\sigma \colon F \to \bar{K}'$ where $F$ ranges over intermediate fields $K \subseteq F \subseteq \bar{K}$, ordered by extension. After verifying that every chain has an upper bound (by taking the union of domains), Zorn's lemma yields a maximal element $\phi \colon F_0 \to \bar{K}'$. We show $F_0 = \bar{K}$: if not, any $\alpha \in \bar{K} \setminus F_0$ has a minimal polynomial over $F_0$ whose image under $\phi$ is irreducible over $\phi(F_0)$ and splits in $\bar{K}'$, allowing an extension of $\phi$ to $F_0(\alpha)$ and contradicting maximality. Finally, surjectivity follows because $\phi(\bar{K})$ is algebraically closed (as an isomorphic copy of $\bar{K}$) and $\bar{K}'$ is algebraic over $K \subseteq \phi(\bar{K})$, forcing $\bar{K}' \subseteq \phi(\bar{K})$. [/proofplan]

[step:Construct the poset of $K$-homomorphisms into $\bar{K}'$]Define the set \begin{align*} \mathcal{S} := \bigl\{(\sigma, F) \;\big|\; K \subseteq F \subseteq \bar{K} \text{ is an intermediate field and } \sigma \colon F \to \bar{K}' \text{ is a } K\text{-homomorphism}\bigr\}. \end{align*} Here a $K$-homomorphism means a field homomorphism $\sigma \colon F \to \bar{K}'$ satisfying $\sigma(a) = a$ for all $a \in K$. The set $\mathcal{S}$ is non-empty since the inclusion $\iota \colon K \hookrightarrow \bar{K}'$ is a $K$-homomorphism, so $(\iota, K) \in \mathcal{S}$. We equip $\mathcal{S}$ with a partial order: declare $(\sigma_1, F_1) \leq (\sigma_2, F_2)$ if and only if $F_1 \subseteq F_2$ and $\sigma_2|_{F_1} = \sigma_1$, i.e., $\sigma_2$ extends $\sigma_1$.[/step]

[guided]The idea is to build a $K$-isomorphism $\bar{K} \to \bar{K}'$ by starting from the identity on $K$ and extending one element at a time. Rather than performing a transfinite induction explicitly, we encode all possible partial extensions into a single poset and invoke Zorn's lemma. Each element of $\mathcal{S}$ is a "partial isomorphism" -- a $K$-homomorphism defined on some intermediate field $F$ between $K$ and $\bar{K}$. The partial order captures the notion that one such map extends another. Since every field homomorphism is injective (the kernel is an ideal in a field, hence $\{0\}$ or the whole field, and the latter is excluded because $\sigma(1) = 1$), each $\sigma \in \mathcal{S}$ is automatically an isomorphism onto its image $\sigma(F) \subseteq \bar{K}'$. The pair $(\iota, K)$ ensures $\mathcal{S} \neq \varnothing$, which is a prerequisite for applying Zorn's lemma.[/guided]

[step:Verify that every chain in $\mathcal{S}$ has an upper bound]Let $\mathcal{C} = \{(\sigma_i, F_i)\}_{i \in I}$ be a totally ordered chain in $\mathcal{S}$. Define \begin{align*} F_{\infty} := \bigcup_{i \in I} F_i. \end{align*} We verify that $F_{\infty}$ is a field. Let $a, b \in F_{\infty}$. Then $a \in F_i$ and $b \in F_j$ for some $i, j \in I$. Since $\mathcal{C}$ is totally ordered, either $F_i \subseteq F_j$ or $F_j \subseteq F_i$; without loss of generality $F_i \subseteq F_j$. Then $a, b \in F_j$, so $a + b$, $a - b$, $ab \in F_j \subseteq F_{\infty}$, and if $b \neq 0$ then $a/b \in F_j \subseteq F_{\infty}$. Since $1 \in K \subseteq F_{\infty}$, the set $F_{\infty}$ is a subfield of $\bar{K}$ containing $K$. Define the map \begin{align*} \sigma_{\infty} \colon F_{\infty} &\to \bar{K}' \\ a &\mapsto \sigma_i(a) \quad \text{for any } i \in I \text{ with } a \in F_i. \end{align*} This is well-defined: if $a \in F_i \cap F_j$ with $(\sigma_i, F_i) \leq (\sigma_j, F_j)$, then $\sigma_j|_{F_i} = \sigma_i$, so $\sigma_j(a) = \sigma_i(a)$. The same compatibility along the total order handles the general case. Since each $\sigma_i$ is a $K$-homomorphism, $\sigma_{\infty}$ preserves addition, multiplication, and fixes $K$ pointwise. Hence $(\sigma_{\infty}, F_{\infty}) \in \mathcal{S}$, and by construction $(\sigma_i, F_i) \leq (\sigma_{\infty}, F_{\infty})$ for all $i \in I$.[/step]

[guided]This is the standard verification for applying Zorn's lemma to a poset of "partial maps ordered by extension." The key point is that the union of a chain of fields is again a field, and the pasting of compatible homomorphisms along a chain yields a well-defined homomorphism on the union. Why does well-definedness hold? Given $a \in F_{\infty}$, the element $a$ may belong to many fields $F_i$ in the chain. But for any two indices $i, j \in I$, the total ordering of $\mathcal{C}$ guarantees (say) $(\sigma_i, F_i) \leq (\sigma_j, F_j)$, which means $\sigma_j$ extends $\sigma_i$. In particular $\sigma_j(a) = \sigma_i(a)$, so the value $\sigma_{\infty}(a)$ does not depend on the choice of index. The fact that $\sigma_{\infty}$ is a field homomorphism (i.e., preserves $+$ and $\cdot$) follows because for any two elements $a, b \in F_{\infty}$, we can find a single $F_j$ containing both $a$ and $b$ (using the total order), and then $\sigma_{\infty}(a + b) = \sigma_j(a + b) = \sigma_j(a) + \sigma_j(b) = \sigma_{\infty}(a) + \sigma_{\infty}(b)$, and similarly for products. Since each $\sigma_i$ fixes $K$, so does $\sigma_{\infty}$.[/guided]

[step:Apply Zorn's lemma to obtain a maximal $K$-homomorphism] The poset $(\mathcal{S}, \leq)$ is non-empty (it contains $(\iota, K)$) and every chain has an upper bound (constructed in the previous step). By Zorn's lemma, $\mathcal{S}$ contains a maximal element $(\phi, F_0)$. That is, $\phi \colon F_0 \to \bar{K}'$ is a $K$-homomorphism with $K \subseteq F_0 \subseteq \bar{K}$, and no proper extension of $\phi$ to a strictly larger intermediate field exists in $\mathcal{S}$. [/step]

[step:Show $F_0 = \bar{K}$ by deriving a contradiction from any element outside $F_0$]Suppose for contradiction that $F_0 \subsetneq \bar{K}$. Choose $\alpha \in \bar{K} \setminus F_0$. Since $\bar{K}$ is algebraic over $K$ and $K \subseteq F_0$, the element $\alpha$ is algebraic over $F_0$. Let \begin{align*} P_{\alpha} \in F_0[x] \end{align*} denote the minimal polynomial of $\alpha$ over $F_0$. By definition, $P_{\alpha}$ is monic, irreducible in $F_0[x]$, and $P_{\alpha}(\alpha) = 0$. Since $\phi \colon F_0 \to \bar{K}'$ is a field isomorphism onto its image $\phi(F_0)$, the map $\phi$ induces a ring isomorphism \begin{align*} \tilde{\phi} \colon F_0[x] &\to \phi(F_0)[x] \end{align*} that applies $\phi$ to each coefficient. The image $\tilde{\phi}(P_{\alpha}) \in \phi(F_0)[x]$ is irreducible over $\phi(F_0)$, because $\tilde{\phi}$ is a ring isomorphism and irreducibility is preserved under ring isomorphisms of polynomial rings. Since $\bar{K}'$ is algebraically closed and $\tilde{\phi}(P_{\alpha}) \in \phi(F_0)[x] \subseteq \bar{K}'[x]$ is a non-constant polynomial, there exists $\beta \in \bar{K}'$ with $\tilde{\phi}(P_{\alpha})(\beta) = 0$. Now consider the simple algebraic extension $F_0(\alpha) \subseteq \bar{K}$. Since $P_{\alpha}$ is the minimal polynomial of $\alpha$ over $F_0$, every element of $F_0(\alpha)$ can be written uniquely as \begin{align*} c_0 + c_1 \alpha + \cdots + c_{d-1} \alpha^{d-1} \end{align*} where $d = \deg P_{\alpha}$ and $c_0, \ldots, c_{d-1} \in F_0$. Similarly, since $\tilde{\phi}(P_{\alpha})$ is irreducible over $\phi(F_0)$ and $\beta$ is a root, the minimal polynomial of $\beta$ over $\phi(F_0)$ divides $\tilde{\phi}(P_{\alpha})$. As $\tilde{\phi}(P_{\alpha})$ is irreducible, the minimal polynomial of $\beta$ over $\phi(F_0)$ equals $\tilde{\phi}(P_{\alpha})$, so $[\phi(F_0)(\beta) : \phi(F_0)] = d$. Define the map \begin{align*} \Phi \colon F_0(\alpha) &\to \bar{K}' \\ c_0 + c_1 \alpha + \cdots + c_{d-1} \alpha^{d-1} &\mapsto \phi(c_0) + \phi(c_1)\beta + \cdots + \phi(c_{d-1})\beta^{d-1}. \end{align*} This is a well-defined field homomorphism. Indeed, the universal property of the quotient $F_0[x]/(P_{\alpha}) \cong F_0(\alpha)$ guarantees that specifying the image of $\alpha$ as $\beta$ -- a root of $\tilde{\phi}(P_{\alpha})$ -- and the action on $F_0$ as $\phi$ uniquely determines a field homomorphism. Since $\Phi$ restricts to $\phi$ on $F_0$ and fixes $K$ pointwise (because $\phi$ does), $\Phi$ is a $K$-homomorphism extending $\phi$ to the strictly larger field $F_0(\alpha) \supsetneq F_0$. This means $(\Phi, F_0(\alpha)) \in \mathcal{S}$ with $(\phi, F_0) < (\Phi, F_0(\alpha))$, contradicting the maximality of $(\phi, F_0)$. Therefore $F_0 = \bar{K}$, and $\phi \colon \bar{K} \to \bar{K}'$ is an injective $K$-homomorphism.[/step]

[guided]The argument here is the heart of the proof: we show that any maximal element of $\mathcal{S}$ must have domain equal to all of $\bar{K}$. Suppose $F_0 \subsetneq \bar{K}$ and pick $\alpha \in \bar{K} \setminus F_0$. Why is $\alpha$ algebraic over $F_0$? Because $\alpha \in \bar{K}$ and $\bar{K}$ is algebraic over $K$, there is a polynomial $Q \in K[x] \subseteq F_0[x]$ with $Q(\alpha) = 0$. Hence $\alpha$ is algebraic over $F_0$ (its minimal polynomial over $F_0$ divides $Q$). Let $P_{\alpha} \in F_0[x]$ be the minimal polynomial of $\alpha$ over $F_0$, which is monic, irreducible, and of some degree $d \geq 1$. We want to "push" this polynomial through $\phi$ and find a root on the other side. The isomorphism $\phi \colon F_0 \xrightarrow{\sim} \phi(F_0)$ extends to a ring isomorphism $\tilde{\phi} \colon F_0[x] \xrightarrow{\sim} \phi(F_0)[x]$ by acting on coefficients. Ring isomorphisms preserve irreducibility: if $\tilde{\phi}(P_{\alpha}) = g \cdot h$ were a non-trivial factorisation in $\phi(F_0)[x]$, then $P_{\alpha} = \tilde{\phi}^{-1}(g) \cdot \tilde{\phi}^{-1}(h)$ would be a non-trivial factorisation in $F_0[x]$, contradicting irreducibility of $P_{\alpha}$. So $\tilde{\phi}(P_{\alpha})$ is irreducible over $\phi(F_0)$. Now we use that $\bar{K}'$ is algebraically closed: the polynomial $\tilde{\phi}(P_{\alpha}) \in \phi(F_0)[x] \subseteq \bar{K}'[x]$ is non-constant (its degree is $d \geq 1$), so it has a root $\beta \in \bar{K}'$. Since $\tilde{\phi}(P_{\alpha})$ is irreducible over $\phi(F_0)$ and $\beta$ is one of its roots, $\tilde{\phi}(P_{\alpha})$ is the minimal polynomial of $\beta$ over $\phi(F_0)$, so $[\phi(F_0)(\beta) : \phi(F_0)] = d = [F_0(\alpha) : F_0]$. The extension map $\Phi \colon F_0(\alpha) \to \bar{K}'$ is defined by sending $\alpha \mapsto \beta$ and acting as $\phi$ on $F_0$. More precisely, every element of $F_0(\alpha)$ has a unique representation $c_0 + c_1\alpha + \cdots + c_{d-1}\alpha^{d-1}$ with $c_i \in F_0$, and we set \begin{align*} \Phi(c_0 + c_1\alpha + \cdots + c_{d-1}\alpha^{d-1}) = \phi(c_0) + \phi(c_1)\beta + \cdots + \phi(c_{d-1})\beta^{d-1}. \end{align*} Why is $\Phi$ a field homomorphism? The isomorphism $F_0(\alpha) \cong F_0[x]/(P_{\alpha})$ identifies $\alpha$ with the coset $x + (P_{\alpha})$. The composite \begin{align*} F_0[x] \xrightarrow{\tilde{\phi}} \phi(F_0)[x] \xrightarrow{\operatorname{ev}_{\beta}} \bar{K}' \end{align*} sends $P_{\alpha}$ to $\tilde{\phi}(P_{\alpha})(\beta) = 0$, so the kernel contains $(P_{\alpha})$. By the universal property of quotient rings, this composite factors through $F_0[x]/(P_{\alpha}) \cong F_0(\alpha)$, yielding the field homomorphism $\Phi$. Since $(P_{\alpha})$ is a maximal ideal (as $P_{\alpha}$ is irreducible and $F_0[x]$ is a PID), the quotient is a field, so the induced map is either zero or injective. It is non-zero because $\Phi(1) = \phi(1) = 1$, hence injective. By construction $\Phi|_{F_0} = \phi$ and $\Phi$ fixes $K$ pointwise, so $(\Phi, F_0(\alpha)) \in \mathcal{S}$. Since $\alpha \in F_0(\alpha) \setminus F_0$, the field $F_0(\alpha)$ strictly contains $F_0$, so $(\phi, F_0) < (\Phi, F_0(\alpha))$. This contradicts the maximality of $(\phi, F_0)$. The contradiction forces $F_0 = \bar{K}$, so $\phi$ is defined on all of $\bar{K}$. Since every field homomorphism is injective ($\ker \phi$ is an ideal of the field $\bar{K}$, hence $\{0\}$ or $\bar{K}$; the latter is excluded by $\phi(1) = 1$), the map $\phi \colon \bar{K} \to \bar{K}'$ is an injective $K$-homomorphism.[/guided]

[step:Show $\phi$ is surjective by proving its image is algebraically closed and contains $K$]It remains to show that $\phi \colon \bar{K} \to \bar{K}'$ is surjective, i.e., $\phi(\bar{K}) = \bar{K}'$. Since $\phi$ is an injective field homomorphism, $\phi(\bar{K})$ is a subfield of $\bar{K}'$ isomorphic to $\bar{K}$. Because $\bar{K}$ is algebraically closed and the property of being algebraically closed is preserved under field isomorphisms, $\phi(\bar{K})$ is algebraically closed. We now show $\bar{K}' \subseteq \phi(\bar{K})$. Let $\gamma \in \bar{K}'$ be arbitrary. Since $\bar{K}'$ is algebraic over $K$ (by the definition of algebraic closure) and $K = \phi(K) \subseteq \phi(\bar{K})$, the element $\gamma$ is algebraic over $\phi(\bar{K})$. That is, $\gamma$ is a root of some non-constant polynomial with coefficients in $\phi(\bar{K})$. But $\phi(\bar{K})$ is algebraically closed, so every non-constant polynomial over $\phi(\bar{K})$ already splits completely in $\phi(\bar{K})$. In particular, $\gamma \in \phi(\bar{K})$. Since $\gamma \in \bar{K}'$ was arbitrary, $\bar{K}' \subseteq \phi(\bar{K})$. Combined with $\phi(\bar{K}) \subseteq \bar{K}'$, this gives $\phi(\bar{K}) = \bar{K}'$. Therefore $\phi \colon \bar{K} \xrightarrow{\sim} \bar{K}'$ is a $K$-isomorphism.[/step]

[guided]We have established that $\phi \colon \bar{K} \to \bar{K}'$ is an injective $K$-homomorphism. To conclude that it is a $K$-isomorphism, we need surjectivity. The argument relies on a key interplay between two properties: (a) $\phi(\bar{K})$ is algebraically closed, and (b) $\bar{K}'$ is algebraic over $\phi(\bar{K})$. For (a): the field $\bar{K}$ is algebraically closed by hypothesis (it is an algebraic closure of $K$). The image $\phi(\bar{K})$ is a field isomorphic to $\bar{K}$ via $\phi$. We claim that algebraic closure is preserved under isomorphism. Let $Q \in \phi(\bar{K})[x]$ be a non-constant polynomial. Pulling back the coefficients through $\phi^{-1} \colon \phi(\bar{K}) \xrightarrow{\sim} \bar{K}$, we obtain a non-constant polynomial $\phi^{-1}(Q) \in \bar{K}[x]$. Since $\bar{K}$ is algebraically closed, $\phi^{-1}(Q)$ has a root $r \in \bar{K}$. Then $\phi(r) \in \phi(\bar{K})$ is a root of $Q$, because applying $\phi$ to the equation $\phi^{-1}(Q)(r) = 0$ gives $Q(\phi(r)) = 0$. So every non-constant polynomial over $\phi(\bar{K})$ has a root in $\phi(\bar{K})$, confirming that $\phi(\bar{K})$ is algebraically closed. For (b): take any $\gamma \in \bar{K}'$. Since $\bar{K}'$ is an algebraic closure of $K$, the element $\gamma$ is algebraic over $K$. In particular, there exists a non-constant polynomial $Q \in K[x]$ with $Q(\gamma) = 0$. Since $K = \phi(K) \subseteq \phi(\bar{K})$, this same polynomial $Q$ has coefficients in $\phi(\bar{K})$, so $\gamma$ is algebraic over $\phi(\bar{K})$. Combining (a) and (b): the element $\gamma$ satisfies a non-constant polynomial over $\phi(\bar{K})$, and $\phi(\bar{K})$ is algebraically closed, so $\gamma \in \phi(\bar{K})$. Since $\gamma \in \bar{K}'$ was arbitrary, $\bar{K}' \subseteq \phi(\bar{K})$. The reverse inclusion $\phi(\bar{K}) \subseteq \bar{K}'$ holds because $\phi$ maps into $\bar{K}'$. Hence $\phi(\bar{K}) = \bar{K}'$, and $\phi$ is a $K$-isomorphism. Note what this argument does NOT show: it does not establish that the isomorphism is unique. Indeed, the isomorphism $\phi$ depends on the choices made by Zorn's lemma, and in general there are many distinct $K$-isomorphisms $\bar{K} \xrightarrow{\sim} \bar{K}'$. Uniqueness up to $K$-automorphism is a separate (and more subtle) question connected to the structure of the absolute Galois group $\operatorname{Gal}(\bar{K}/K)$.[/guided]