No Isomorphism from Woset to Initial Segment

From ProofWiki
Jump to navigation Jump to search


Let $\struct {S, \preceq}$ be a woset.

Let $a \in S$, and let $S_a$ be the initial segment of $S$ determined by $a$.

Then there is no order isomorphism between $S$ and $S_a$.


Aiming for a contradiction, suppose $f: S \to S_a$ is an order isomorphism.

By Order Isomorphism from Woset onto Subset, $\forall x \in S: x \preceq \map f x$.

In particular, then, $a \preceq \map f a$.

But the codomain of $f$ is $S_a$, so $\map f a \in S_a$.

Thus $\map f a \prec a$, which is a contradiction.

So there can be no such order isomorphism.