Prove that for any infinite poset there is an infinite subset which is either linearly ordered or antichain.

If we also require that the infinite chain or anti-chain will be maximal, then we do need the axiom of choice. Indeed Zorn's lemma is a useful tool when finding maximal chains and anti-chains.

There is a choice principle called Hausdorff's maximality principle stating that in every partially ordered set there exists a maximal chain. It too is equivalent to the axiom of choice, so when you negate the axiom of choice you add a partially ordered set without a maximal chain.

For anti-chains there exists a similar principle, which too implies the axiom of choice.

If you just want to find an infinite anti-chain or chain, some axiom of choice may be needed. Indeed there are trees that every branch can be extended, but there is no infinite branch (thus no infinite chain).

On the other hand, there exists a model of ZF assuming some amount of finite choice, in which there exists a partially ordered set which is infinite but has no infinite chains or anti-chains.

The proof is quite complicated, but appears on Jech, The Axiom of Choice as the model given in Theorem 7.11 (p. 107) and in exercise 7.14 (p. 115)

Your proof is fine for the most, assuming the axiom of choice (or at least The Principle of Dependent Choice). However if we only remove a finite number of comparable elements we don't have to have an anti-chain left.

Dichotomy proofs should show that if condition I failed then condition II holds. And indeed, suppose that $X$ is infinite, but every chain is finite. We define a sequence of elements $x_n\in X$ by induction:

Let $x_0\in X$ be an element such that $X_0=\{x\in X\mid x\nleq x_0\land x_0\nleq x\}$ is infinite. If no element has this property, we can use the same induction to define an infinite chain (taking all the elements comparable with $x_0$ instead).

Suppose $x_n$ and $X_n$ were defined, let $x_{n+1}\in X_n$ be such that $X_{n+1}=\{x\in X_n\mid x\nleq x_{n+1}\land x_{n+1}\nleq x\}$ is infinite. If we got stuck at the $n$-th stage (that is $X_{n+1}$ is finite for every $x\in X_n$) then we can define an infinite chain *within $X_n$* by the same induction as in the first step.

I claim that $\{x_n\mid n\in\mathbb N\}$ is an infinite anti-chain. First note that $\ldots\subsetneq X_n\subsetneq X_{n-1}\subsetneq\ldots\subsetneq X$, and $x_n\in X_{n-1}$ and $x_0\in X$. Each $x_n$ defined $X_n$ and those are unique so $x_n\neq x_k$ for $n\neq k$.

Secondly, since $x_k\in X_{k-1}$ if $x_k$ and $x_n$ are comparable and $n<k$ then $x_k\in X_n$ which was defined as a set of elements incomparable with $x_n$ to begin with, therefore we have an infinite anti-chain.

The fact that every infinite partial order has either an infinite chain or an infinite antichain has a quick proof as a consequence of the infinite Ramsey theorem, which asserts that every coloring of pairs from an infinite set admits an infinite monochromatic subset. Namely, for any partial order, consider the coloring of pairs either as "comparable" or "incomparable," as the case may be for that pair. By Ramsey's theorem, there is an infinite monochromatic subset, meaning that all pairs from the subset are assigned the same color, and this subset therefore is either an infinite chain or an infinite antichain.

Meanwhile, Ramsey's theorem can apparantly be proved using only the principle of dependent choices---a weak choice principle, allowing one to make countably many choices in succession---for the proof of Ramsey's theorem given on the linked wikipedia page is an inductive argument, in each stage of which one makes countably many choices in succession.

One can use a free ultrafilter to get a reasonably slick argument that minimizes the amount of detail that has to be kept track of at the cost of using a different consequence of AC $-$ the Boolean prime ideal theorem, which is strictly weaker than AC and independent of Dependent Choice, which also suffices.

Let $\mathscr{U}$ be a free ultrafilter on $X$. For each $x\in X$ let $C(x)=\{y\in X:x\le y\lor y\le x\}$, and let $A(x)=X\setminus C(x)=\{y\in X:x\not\le y \land y\not\le x\}$; exactly one of $C(x)$ and $A(x)$ belongs to $\mathscr{U}$. Let $C=\{x\in X:C(x)\in\mathscr{U}\,\}$, and let $A=X\setminus C=\{x\in X:A(x)\in\mathscr{U}\,\}$. Exactly one of $A$ and $C$ belongs to $\mathscr{U}$; without loss of generality assume that $C\in\mathscr{U}$.

Fix $x_0\in C$, and let $C_0=C\cap C(x_0)\setminus\{x_0\}\in\mathscr{U}$. Given $C_n\in\mathscr{U}\,$ for some $n\in\omega$, choose $x_{n+1}\in C_n$ and let $C_{n+1}=C_n\cap C(x_{n+1})\setminus\{x_{n+1}\}\in\mathscr{U}\,$; clearly the construction goes through to $\omega$ to produce a set $\{x_n:n\in\omega\}$ of distinct elements of $X$. Moreover, for any $k<n<\omega$ we have $x_n\in C_k\subseteq C(x_k)$, so $\{x_n:n\in\omega\}$ is an infinite chain in $X$. (Had $A$ been a member of $\mathscr{U}\,$ instead of $C$, the set $\{x_n:n\in\omega\}$ would of course have been an infinite antichain.)

As JDH has already noted, this is essentially just the two-color case of the infinite Ramsey theorem, $\kappa\to(\omega)_2^2$. If one wanted to use a really big stick, one could beat the problem over the head with the Erdős-Dushnik-Miller theorem, $\kappa\to(\kappa,\omega)^2$, and conclude that either $X$ has a chain of cardinality $|X|$, or $X$ has an infinite antichain. (Here the rôles of chain and antichain can of course be reversed.)