Why does the Well Ordering Theorem imply decreasing ordinals go to zero? The Well Ordering Theorem states that any set can be well ordered. But in this PBS Infinite Series video, Kelsey states the theorem as, "Any decreasing sequence of ordinals eventually goes to zero." This isn't an obvious equivalence to me. Does deeper work need to be done to prove it, or is it a one-liner?
It may be hard for me to see the connection because I don't know the rigorous definition of ordinals, just the intuitive idea from the above-linked episode.

Let $(E,<)$ be a well ordered set.
Suppose for contradiction that there is an infinite decreasing sequence $(x_n)_{n\in\mathbb{N}}$ of elements of $E$.
Since $E$ is well ordered, the set $X:=\{x_n \big| \ n \in \mathbb{N}\}$ has a minimum, say $m$.
For every $x\in X$, the set $\{y\in X \big| \ x<y\}$ has a minimum, we hence have a function $S : X \mapsto X, \ x \mapsto \min\big(\{y\in X \big| \ x<y\}\big)$. $S$ behaves like a successor function : there is no $y\in X$ such that $x<y<S(x)$.
The function $\sigma : \mathbb{N} \mapsto X, \ n \mapsto S^n(m)$ is an order-isomorphism.
The sequence $(\sigma^{-1}(x_n))_{n\in \mathbb{N}}$ is a strictly decreasing sequence of elements of $\mathbb{N}$, an absurdity!
