My proof of Dilworth's theorem

Dilworth's theorem: Given a finite poset $P$ its width $w(P)$, minimum number of chains that cover $P$, is equal to $a(P)$, the size of its maximum antichain.

My proof isn't as elegant as textbook's, but they share a key construction in the induction step.

Proof:
Clearly $a(P)\le w(P)$, so it suffices to show that $w(P)\le a(P)$.

Induct on $|P|$. Add an element $x$ to $P$ to obain $P'$. Without loss of generality we can assume $x\in \max(P')$.

If $a(P')=a(P)+1$ then we are done, because by inductive hypothesis $$w(P')\le w(P)+1=a(P)+1=a(P').$$

Suppose that $a(P')=a(P)$, and let $$C_1,\ldots,C_{w(P)}$$ be a smallest chain decomposition of $P$. If $x\gt\max(C_i)$ for some $i$ then we can add $x$ to $C_i$ and get $$w(P')=w(P)=a(P)=a(P').$$ Hence for each $i$ let $d_i$ be the minimal element in $C_i$ such that $x\ngeq d_i$.

Consider $$Q=\cup_i\{y|y\in C_i\wedge y\geq d_i\}.$$ Element $x$ is not comparable with $Q$, so $$a(Q)+1=a(Q+x)\leq a(P')=a(P).$$ Let $c_i=C_i-Q$, the remains of $C_i$ smaller than $x$. Note that $x$ is greater than $c_i$ for every $i$.

By inductive hypothesis, consider a smallest chain decomposition of Q $$C'_1,C'_2,\dots,C'_{w(Q)}.$$ We make all individual smallest element of $\{C'_i\}$ from distinct $C_i$ as follows. Whenever consecutive smallest elements of both $C'_i$ and $C'_j$ are from $C_k$, we merge them. By argument of infinite descent, the merging has to terminate without any empty $C'_i$.

Then, we glue every $c_i$ to an appropriate $C'_j$ such that exactly $w(P)-w(Q)$ $c_i$s remain. Finally we add $x$ to one of them, resulting in a chain decomposition of $P'$ of size $w(P)$.