nyuuzyou/wikis huggingface dataset:
Order Generating iff Every Superset Closed on Infima is Whole Space

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $X$ be a subset of $S$.
Then
:$X$ is order generating
:$\forall Y \subseteq S: Y \supseteq X \land \paren {\forall Z \subseteq Y: \inf Z \in Y} \implies Y = S$
== Proof ==
=== Sufficient Condition ===
Let $X$ be order generating.
Let $Y \subseteq S$ such that
:$Y \supseteq X \land \paren {\forall Z \subseteq Y: \inf Z \in Y}$
We will prove that
:$S \subseteq Y$
Let $s \in S$.
By Order Generating iff Every Element is Infimum:
:$\exists Z \subseteq X: s = \inf Z$
By Subset Relation is Transitive:
:$Z \subseteq Y$
Thus by assumption:
:$s \in Y$
By definition of set equality:
:$Y = S$
=== Necessary Condition ===
Assume that:
:$\forall Y \subseteq S: Y \supseteq X \land \paren {\forall Z \subseteq Y: \inf Z \in Y} \implies Y = S$
Define $Y := \set {\inf Z: Z \subseteq X}$
By definition of subset:
:$Y \subseteq S$
We will prove that
:$X \subseteq Y$
Let $x \in X$.
By definitions of singleton and subset:
:$\set x \subseteq X$
By Infimum of Singleton:
:$\inf \set x = x$
Thus by definition of $Y$:
:$x \in Y$
We will prove that:
:$\forall x \in S: \exists Z \subseteq X: x = \inf Z$
Let $x \in S$.
We will prove that:
:$\forall Z \subseteq Y: \inf Z \in Y$
Let $Z \subseteq Y$.
Define:
:$T := \bigcup \set {A \subseteq X: \inf A \in Z}$
By Union of Subsets is Subset:
:$T \subseteq X \subseteq S$
Define:
:$N := \set {\inf A: A \subseteq X \land \inf A \in Z}$
We will prove that:
:$Z \subseteq N$
Let $y \in Z$.
By definition of subset:
:$y \in Y$
By definition of $Y$:
:$\exists Z \subseteq X: y = \inf Z$
Thus by definition of $N$:
:$y \in N$
By definition of subset:
:$N \subseteq Z$
By definition of set equality:
:$Z = N$
By Infimum of Infima:
:$\inf Z = \inf T$
Thus
:$\inf Z \in Y$
By assumption:
:$Y = S$
Then
:$x \in Y$
Thus by definition of $Y$:
:$\exists Z \subseteq X: x = \inf Z$
Hence $X$ is order generating by Order Generating iff Every Element is Infimum.
== Sources ==
* 
* 
Category:Complete Lattices
Category:Order Generating Subsets
Order Generating iff Not Preceding implies There Exists Element Preceding and Not Preceding

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $X$ be a subset of $S$.
Then
:$X$ is order generating
:$\forall x, y \in S: \paren {y \npreceq x \implies \exists p \in X: x \preceq p \land y \npreceq p}$
== Proof ==
=== Sufficient Condition ===
Let $X$ be order generating.
Let $x, y \in S$ such that:
:$y \npreceq x$
By Order Generating iff Every Element is Infimum:
:$\exists P \subseteq X: x = \inf P$
By definition of infimum:
:$y$ is lower bound for $P \implies y \preceq x$
By definition of lower bound:
:$\exists p \in P: y \npreceq p$
Thus by definition of subset:
:$p \in X$
By definition of infimum:
:$x$ is lower bound for $P$.
Thus by definition of lower bound:
:$x \preceq p$
Thus
:$y \npreceq p$
=== Necessary Condition ===
Suppose that
:$\forall x, y \in S: \paren {y \npreceq x \implies \exists p \in X: x \preceq p \land y \npreceq p}$
Let $x \in S$.
Thus by definition of complete lattice:
:$x^\succeq \cap X$ admits an infimum.
Define $y := \map \inf {x^\succeq \cap X}$
By definition of infimum:
:$y$ is lower bound for $x^\succeq \cap X$
We will prove that:
:$x$ is lower bound for $x^\succeq \cap X$
Let $a \in x^\succeq \cap X$.
By definition of intersection:
:$a \in x^\succeq$
Thus by definition of upper closure of element:
:$x \preceq a$
By definition of infimum:
:$x \preceq y$
By definition of antisymmetry:
:$y \nprec x$
It remains to prove that
:$y = x$
:$y \ne x$
By definition of $\prec$:
:$y \npreceq x$ or $y = x$
;Case $y \npreceq x$
By assumption:
:$\exists p \in X: x \preceq p \land y \npreceq p$
By definition of upper closure of element:
:$p \in x^\succeq$
By definition of intersection:
:$p \in x^\succeq \cap X$
By definition of lower bound:
:$y \preceq p$
Thus this contradicts $y \npreceq p$.
;Case $y = x$
This contradicts $y \ne x$.
== Sources ==
* 
* 
Category:Complete Lattices
Category:Order Generating Subsets
Order Isomorphic Sets are Equivalent

== Theorem ==
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be order isomorphic.
Then $S$ and $T$ are equivalent.
== Proof ==
By definition, an order isomorphism is a bijection $\phi$ such that:
:$\phi: S \to T$ is order-preserving
:$\phi^{-1}: T \to S$ is order-preserving.
So, by definition, there exists a bijection between $S$ and $T$.
The result follows by definition of set equivalence.
== Sources ==
* : $\S 3.3$: Ordered sets. Order types
Category:Examples of Equivalence Relations
Category:Order Isomorphisms
Order Isomorphism/Examples/Real Arctangent Function

== Example of Order Isomorphism ==
The real arctangent function $\arctan$ is an order isomorphism between the set of real numbers $\R$ and the open real interval $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$ under the usual ordering.
== Proof ==
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations
Category:Examples of Order Isomorphisms
Order Isomorphism Preserves Infima and Suprema

== Theorem ==
Let $L = \left({S, \preceq}\right)$, $L' = \left({S', \preceq'}\right)$ be ordered sets.
Let $f:S \to S'$ be an order isomorphism between $L$ and $L'$.
Then $f$ preserves infima and suprema.
== Proof ==
=== $f$ preserves infima ===
Let $X$ be a subset of $S$ such that
:$X$ admits an infimum in $L$.
By definition of infimum:
:$\inf X$ is lower bound for $X$.
Thus by Order Isomorphism Preserves Lower Bounds:
:$f\left({\inf X}\right)$ is lower bound for $f\left[{X}\right]$.
We will prove that
:$\forall x \in S': x$ is lower bound for $f\left[{X}\right] \implies x \preceq' f\left({\inf X}\right)$
Let $x \in S'$ such that
:$x$ is lower bound for $f\left[{X}\right]$.
By definitions of order isomorphism and bijection:
:$f$ is a surjection.
By definition of surjection:
:$S' = f\left[{S}\right]$
By definition of image of set:
:$\exists y \in S: x = f\left({y}\right)$
By Order Isomorphism Preserves Lower Bounds:
:$y$ is lower bound for $X$.
By definition of infimum:
:$y \preceq \inf X$
Thus by definition of order isomorphism:
:$x \preceq' f\left({\inf X}\right)$
Thus by definition of infimum:
:$f\left[{X}\right]$ admits an infimum in $L'$ and $\inf\left({f\left[{X}\right]}\right) = f\left( {\inf X}\right)$
=== $f$ preserves suprema ===
This fallows by mutatis mutandis.
== Sources ==
* 
Category:Order Isomorphisms
Order Isomorphism Preserves Initial Segments

== Theorem ==
Let $A_1$ and $A_2$ be classes.
Let $\prec_1$ and $\prec_2$ be strict orderings.
Let $\phi: A_1 \to A_2$ create an order isomorphism between $\struct {A_1, \prec_1}$ and $\struct {A_2, \prec_2}$.
Suppose $x \in A_1$.
Then $\phi$ maps the $\prec_1$-initial segment of $x$ to the $\prec_2$-initial segment of $\map \phi x$.
== Proof ==
$\phi$ maps the $\prec_1$-initial segment of $x$ to:
This is the $\prec_2$-initial segment of $\map \phi x$.
== Sources ==
* : $\S 6.31$
Category:Order Isomorphisms
Order Isomorphism Preserves Lower Bounds

== Theorem ==
Let $L = \struct {S, \preceq}$, $L' = \struct {S', \preceq'}$ be ordered sets.
Let $f: S \to S'$ be an order isomorphism between $L$ and $L'$.
Let $x \in S$, $X \subseteq S$.
Then $x$ is lower bound for $X$ $\map f x$ is lower bound for $f \sqbrk X$.
== Proof ==
By definition of order isomorphism:
:$f$ is an order embedding.
=== Sufficient Condition ===
Assume that
:$x$ is lower bound for $X$.
By Order Embedding is Increasing Mapping:
:$f$ is an increasing mapping.
Thus by Increasing Mapping Preserves Lower Bounds:
:$\map f x$ is lower bound for $f \sqbrk X$.
=== Necessary Condition ===
Assume that
:$\map f x$ is lower bound for $f \sqbrk X$.
Let $y \in X$.
By definition of image of set:
:$\map f y \in f \sqbrk X$
By definition of lower bound:
:$\map f y \preceq' \map f x$
Thus by definition of order embedding:
:$y \preceq x$
== Sources ==
* 
Category:Order Isomorphisms
Order Isomorphism Preserves Strictly Minimal Elements

== Theorem ==
Let $A_1$ and $A_2$ be classes.
Let $\prec_1$ and $\prec_2$ be relations.
Let $\phi : A_1 \to A_2$ create an order isomorphism between $\struct {A_1, \prec_1}$ and $\struct {A_1, \prec_2}$.
Let $B \subseteq A_1$.
Then $\phi$ maps the strictly minimal elements under $\prec_1$ of $B$ to the strictly minimal elements under $\prec_2$ of $\phi \sqbrk B$.
== Proof ==
Suppose $x$ is a strictly minimal element of $B$. That is:
:$\neg \exists y \in B: x \prec_1 y$
This is equivalent to the statement:
:$\neg \exists z \in \phi \sqbrk B: \map \phi x \prec_2 z$ since $z$ is of the form $\map \phi y$ by the definition of order isomorphism.
Thus, this statement is true $\map \phi x$ is a strictly minimal element of $B$.
== Sources ==
* : $\S 6.31$
Category:Order Isomorphisms
Order Isomorphism Preserves Upper Bounds

== Theorem ==
Let $L = \struct {S, \preceq}$, $L' = \struct {S', \preceq'}$ be ordered sets.
Let $f: S \to S'$ be an order isomorphism between $L$ and $L'$.
Let $x \in S$, $X \subseteq S$.
Then:
:$x$ is an upper bound for $X$
:
:$\map f x$ is an upper bound for $f \sqbrk X$.
== Proof ==
By definition of order isomorphism:
:$f$ is an order embedding.
=== Sufficient Condition ===
Assume that
:$x$ is upper bound for $X$.
By Order Embedding is Increasing Mapping:
:$f$ is an increasing mapping.
Thus by Increasing Mapping Preserves Upper Bounds:
:$\map f x$ is an upper bound for $f \sqbrk X$.
=== Necessary Condition ===
Assume that:
:$\map f x$ is upper bound for $f \sqbrk X$.
Let $y \in X$.
By definition of image of set:
:$\map f y \in f \sqbrk X$
By definition of upper bound:
:$\map f x \preceq' \map f y$
Thus by definition of order embedding:
:$x \preceq y$
== Sources ==
* 
Category:Order Isomorphisms
Order Isomorphism between Linearly Ordered Spaces is Homeomorphism

== Theorem ==
Let $\struct {S_1, \le_1, \tau_1}$ and $\struct {S_2, \le_2, \tau_2}$ be linearly ordered spaces.
Let $\phi: S_1 \to S_2$ be an order isomorphism from $\struct {S_1, \le_1}$ to $\struct {S_2, \le_2}$.
Then $\phi$ is a homeomorphism from $\struct {S_1, \tau_1}$ to $\struct {S_2, \tau_2}$.
== Proof ==
By the definition of order isomorphism, $\phi$ is a bijection.
Thus to show $\phi$ is a homeomorphism it remains to be shown that:
:$\phi$ is continuous
and:
:$\phi^{-1}$ is continuous.
First it is shown that $\phi^{-1}$ is continuous.
By Order Isomorphism Preserves Initial Segments and its dual, $\phi$ maps open rays in $\struct {S_1, \le_1}$ to open rays in $\struct {S_2, \le_2}$.
By Continuity Test using Sub-Basis, $\phi^{-1}$ is continuous.
Next it is shown that $\phi^{-1}$ is continuous.
By Inverse of Order Isomorphism is Order Isomorphism, $\phi^{-1}$ is an order isomorphism.
Applying the above shows that $\phi = \paren {\phi^{-1} }^{-1}$ is continuous.
Both $\phi$ and $\phi^{-1}$ have been shown to be continuous.
Thus, by definition, $\phi$ is a homeomorphism.
Category:Linearly Ordered Spaces
Order Isomorphism between Ordinals and Proper Class

== Theorem ==
Let $\struct {A, \prec}$ be a strict well-ordering.
Let $A$ be a proper class.
Let the initial segment of $x$ be a set for every $x \in A$.
Then we may make the following definitions:
Set $G$ equal to the collection of ordered pairs $\tuple {x, y}$ such that:
:$y \in A \setminus \Img x$
:$\paren {A \setminus \Img x} \cap A_y = \O$
Use the First Principle of Transfinite Recursion to construct a mapping $F$ such that:
:The domain of $F$ is the class of all ordinals $\On$
:For all ordinals $x$, $\map F x = \map G {F {\restriction_x} }$
Then $F: \On \to A$ is an order isomorphism between $\struct {\On, \in}$ and $\struct {A, \prec}$.
=== Corollary ===
== Proof ==
=== Lemma ===
Assume that:
:$\exists x: A \setminus \Img x = \O$
Then:
:$A \subseteq \Img x$
Therefore, $A$ is a set.
This contradicts the fact that $A$ is a proper class.
Therefore by Axiom of Subsets Equivalents and De Morgan's Laws (Predicate Logic):
:$\forall x: A \setminus \Img x \ne \O$
Then:
where $\rightarrowtail$ denotes an injection.
Now to prove that $F$ is surjective:
But if $\Img F = A \cap A_x$, then it is equal to some initial segment of $A$.
This would imply that $\Img F$ is a set, which is a contradiction.
Therefore $A = \Img F$ and the function is bijective.
Conversely, assume $\map F x \prec \map F y$.
Then $y \in x$ and $x = y$ lead to contradictory conclusions.
By Ordinal Membership is Trichotomy, we may conclude that $x \in y$.
== Also see ==
* Transfinite Recursion Theorem
* Condition for Injective Mapping on Ordinals
* Maximal Injective Mapping from Ordinals to a Set
== Sources ==
* : $\S 7.49$
Category:Class of All Ordinals
Category:Class Mappings
Order Isomorphism between Ordinals and Proper Class/Corollary

== Corollary to Order Isomorphism between Ordinals and Proper Class ==
Let $A$ be a proper class of ordinals.
We will take ordering on $A$ to be $\in$.
Set $G$ equal to the class of all ordered pairs $\tuple {x, y}$ such that:
:$y \in A \setminus \Img x$
:$\paren {A \setminus \Img x} \cap A_y = \O$
Define $F$ by the First Principle of Transfinite Recursion to construct a mapping $F$ such that:
:The domain of $F$ is $\On$.
:For all ordinals $x$, $\map F x = \map G {F \restriction x}$.
Then $F: \On \to A$ is an order isomorphism between $\struct {\On, \in}$ and $\struct {A, \in}$.
== Proof ==
$A$ is a proper class of ordinals.
It is strictly well-ordered by $\in$.
Moreover, every initial segment of $A$ is a set, since the initial segment of the ordinal is simply the ordinal itself.
Therefore, we may apply Order Isomorphism between Ordinals and Proper Class to achieve the desired isomorphism.
== Remark ==
This theorem shows that every proper class of ordinals can be put in a unique order-isomorphism with the set of all ordinals.
== Sources ==
* : $\S 7.50$
Category:Order Isomorphisms
Category:Ordinals
Category:Class Mappings
Order Isomorphism between Ordinals and Proper Class/Lemma

== Lemma for Order Isomorphism between Ordinals and Proper Class ==
Suppose the following conditions are met:
Let $A$ be a class.
We allow $A$ to be a proper class or a set.
Let $\struct {A, \prec}$ be a strict well-ordering.
Let every $\prec$-initial segment be a set, not a proper class.
Let $\Img x$ denote the image of a subclass $x$.
Let $G$ equal the class of all ordered pairs $\tuple {x, y}$ satisfying:
::$y \in A \setminus \Img x$
::The initial segment $A_y$ of $\struct {A, \prec}$ is a subset of $\Img x$
Let $F$ be a mapping with a domain of $\On$.
Let $F$ also satisfy:
:$\map F x = \map G {F \restriction x}$
Then:
: $G$ is a mapping
: $\map G x \in A \setminus \Img x \iff A \setminus \Img x \ne \O$
Note that only the first four conditions need hold: we may construct classes $F$ and $G$ satisfying the other conditions using the First Principle of Transfinite Recursion.
== Proof ==
Therefore, we may conclude, that $G$ is a single-valued relation and therefore a mapping.
For the second part:
Furthermore:
:$\map G x \in A \setminus \Img x \implies A \setminus \Img x \ne \O$ by the definition of non-empty.
== Also see ==
* Transfinite Recursion Theorem
* Condition for Injective Mapping on Ordinals
* Maximal Injective Mapping from Ordinals to a Set
== Sources ==
* : $\S 7.48$
Category:Ordinals
Category:Order Theory
Order Isomorphism between Tosets is not necessarily Unique

== Theorem ==
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be tosets.
Let $\struct {S_1, \preccurlyeq_1} \cong \struct {S_2, \preccurlyeq_2}$, that is, let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be order isomorphic.
Then it is not necessarily the case that there is exactly one mapping $f: S_1 \to S_2$ such that $f$ is an order isomorphism.
== Proof ==
Proof by Counterexample:
Let $\Z$ denote the set of integers.
We have that Integers under Usual Ordering form Totally Ordered Set.
Let $m \in \Z$ be an arbitrary integer.
Let $f_m: \Z \to \Z$ be the order isomorphism defined as:
:$\forall a \in \Z: \map {f_m} a = a + m$
It follows that there are at least as many order isomorphisms of from $\Z$ to $\Z$ as there are integers.
Hence the result
== Sources ==
* : $\S 1$: Naive Set Theory: $\S 1.7$: Well-Orderings and Ordinals
Category:Order Isomorphisms
Category:Total Orderings
Order Isomorphism between Wosets is Unique

== Theorem ==
Let $\struct {S_1, \preceq_1}$ and $\struct {S_2, \preceq_2}$ be wosets.
Let $\struct {S_1, \preceq_1} \cong \struct {S_2, \preceq_2}$, that is, let $\struct {S_1, \preceq_1}$ and $\struct {S_2, \preceq_2}$ be order isomorphic.
Then there is exactly one mapping $f: S_1 \to S_2$ such that $f$ is an order isomorphism.
== Proof ==
Let $f: S_1 \to S_2$ and $g: S_1 \to S_2$ both be order isomorphisms.
By Inverse of Order Isomorphism is Order Isomorphism, the inverse $f^{-1}$ is also an order isomorphism.
Let $h = f^{-1} \circ g$ be the composition of $f^{-1}$ and $g$, which, by Composite of Order Isomorphisms is Order Isomorphism, is itself an order isomorphism.
So, by Order Isomorphism from Woset onto Subset:
:$\forall x \in S_1: x \preceq_1 \map h x$
Now we apply $f$ to $S_1$ and see that:
:$\forall x \in S_1: \map f x \preceq_2 \map f {\map h x} = \map g x$
In a similar way we can show that:
:$\forall x \in S_1: \map g x \preceq_2 \map f x$
Hence $f = g$ and the proof is complete.
== Sources ==
* : $\S 1$: Naive Set Theory: $\S 1.7$: Well-Orderings and Ordinals: Theorem $1.7.3$
Category:Order Isomorphisms
Category:Well-Orderings
Order Isomorphism forms Galois Connection

== Theorem ==
Let $L_1 = \struct {S_1, \preceq_1}$, $L_2 = \struct {S_2, \preceq_2}$ be ordered sets.
Let $f:S_1 \to S_2$ be an order isomorphism between $L_1$ and $L_2$.
Then $\struct {f, f^{-1} }$ is a Galois connection.
== Proof ==
Let $t \in S_2$, $s \in S_1$.
We will prove that:
:$t \preceq_2 \map f s \implies \map {f^{-1} } t \preceq_1 s$
Assume that:
:$t \preceq_2 \map f s$
By Inverse of Order Isomorphism is Order Isomorphism:
:$f^{-1}$ is an order isomorphism.
By definition of order isomorphism:
:$f^{-1}$ is an order embedding.
By definition of order embedding:
:$\map {f^{-1} } t \preceq_1 \map {f^{-1} } {\map f s}$
Thus by definition of bijection:
:$\map {f^{-1} } t \preceq_1 s$
We will prove that:
:$\map {f^{-1} } t \preceq_1 s \implies t \preceq_2 \map f s$
Assume that:
:$\map {f^{-1} } t \preceq_1 s$
By definition of order embedding:
:$\map f {\map {f^{-1} } t} \preceq_2 \map f s$
Thus by definition of bijection:
:$t \preceq_2 \map f s$
== Sources ==
* 
Category:Galois Connections
Category:Order Isomorphisms
Order Isomorphism from Woset onto Subset

== Theorem ==
Let $\struct {S, \preceq}$ be a woset.
Let $T \subseteq S$.
Let $f: S \to T$ be an order isomorphism.
Then $\forall x \in S: x \preceq \map f x$.
== Proof ==
Let $T = \set {x \in S: \map f x \prec x}$.
We are to show that $T = \O$.
 that $T \ne \O$.
Then as $\struct {S, \preceq}$ is a woset, by definition $T$ has a minimal element: call it $x_0$.
Since $x_0 \in T$, we have $\map f {x_0} \prec x_0$.
So, let $x_1 = \map f {x_0}$.
$f$ is an order isomorphism, so since $x_1 \prec x_0$, it follows that $\map f {x_1} \prec \map f {x_0} = x_1$.
So as $\map f {x_1} \prec x_1$ it follows that $x_1 \in T$.
But $x_0$ was chosen to be the minimal element of $T$.
From this contradiction, it follows that it can not be the case that $T \ne \O$.
So $T = \O$ and so $\forall x \in S: x \preceq \map f x$.
== Sources ==
* : $\S 1$: Naive Set Theory: $\S 1.7$: Well-Orderings and Ordinals: Theorem $1.7.2$
Category:Well-Orderings
Category:Order Isomorphisms
Order Isomorphism iff Strictly Increasing Surjection

== Theorem ==
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be totally ordered sets.
A mapping $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$ is an order isomorphism :
:$(1): \quad \phi$ is a surjection
:$(2): \quad \forall x, y \in S: x \mathop {\prec_1} y \implies \map \phi x \mathop {\prec_2} \map \phi y$
== Proof ==
=== Necessary Condition ===
Let $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$ be an order isomorphism.
Then by definition $\phi$ is a bijection and so a surjection.
Suppose $x \mathop {\prec_1} y$.
That is:
:$x \mathop {\preceq_1} y$
:$x \ne y$
Then:
:$x \mathop {\prec_1} y \implies \map \phi x \mathop {\preceq_2} \map \phi y$
as $\phi$ is an order isomorphism.
But as $\phi$ is a bijection it is also an injection.
Thus:
:$\map \phi x = \map \phi y \implies x = y$
and so it follows that:
:$x \mathop {\prec_1} y \implies \map \phi x \mathop {\prec_2} \map \phi y$
=== Sufficient Condition ===
Suppose $\phi$ is a mapping which satisfies the conditions:
:$(1): \quad \phi$ is a surjection
:$(2): \quad \forall x, y \in S: x \mathop {\prec_1} y \implies \map \phi x \mathop {\prec_2} \map \phi y$
From $(2)$ and Strictly Increasing Mapping is Increasing we have:
:$x \mathop {\preceq_1} y \implies \map \phi x \mathop {\preceq_2} \map \phi y$
Now suppose $\map \phi x \mathop {\preceq_2} \map \phi y$.
Suppose $y \mathop {\prec_1} x$.
Then from $(2)$ it would follow that $\map \phi y \mathop {\prec_2} \map \phi x$.
So it is not the case that $y \mathop {\prec_1} x$.
So from the Trichotomy Law:
:$x \mathop {\preceq_1} y$
Thus it follows that:
:$x \mathop {\preceq_1} y \iff \map \phi x \mathop {\preceq_2} \map \phi y$
It follows from Order Isomorphism is Surjective Order Embedding that $\phi$ is an order isomorphism.
== Sources ==
* : $\S 7$: Theorem $7.2$
Category:Order Isomorphisms
Category:Surjections
Order Isomorphism is Equivalence Relation

== Theorem ==
Order isomorphism between ordered sets is an equivalence relation.
So any given family of ordered sets can be partitioned into disjoint classes of isomorphic sets.
== Proof 1 ==
== Proof 2 ==
== Also see ==
* Order Isomorphic Sets are Equivalent
Category:Order Isomorphisms
Category:Examples of Equivalence Relations
Category:Order Isomorphism is Equivalence Relation
Order Isomorphism is Equivalence Relation/Proof 1

== Theorem ==
== Proof ==
Let $\struct {S_1, \preccurlyeq_1} \cong \struct {S_2, \preccurlyeq_2}$ denote that $\struct {S_1, \preccurlyeq_1}$ is isomorphic to $\struct {S_2, \preccurlyeq_2}$.
Checking in turn each of the criteria for equivalence:
=== Reflexivity ===
Thus $\cong$ is seen to be reflexive.
=== Symmetric ===
Thus $\cong$ is seen to be symmetric.
=== Transitive ===
Thus $\cong$ is seen to be transitive.
$\cong$ has been shown to be reflexive, symmetric and transitive.
Hence the result.
== Sources ==
* : $\S 3.2$: Order-preserving mappings. Isomorphisms
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $24$
Category:Order Isomorphism is Equivalence Relation
Order Isomorphism is Preserved by Antilexicographic Order

== Theorem ==
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\struct {T_1, \preccurlyeq_{1'} }$ and $\struct {T_2, \preccurlyeq_{2'} }$ be ordered sets such that:
:$\struct {S_1, \preccurlyeq_1}$ is isomorphic to $\struct {T_1, \preccurlyeq_{1'} }$
:$\struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {T_2, \preccurlyeq_{2'} }$
Then the antilexicographic order $\struct {S_1, \preccurlyeq_1} \otimes^a \struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {T_2, \preccurlyeq_{2'} } \otimes^a \struct {T_2, \preccurlyeq_{2'} }$.
== Proof ==
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $33$
Category:Antilexicographic Order
Category:Order Isomorphisms
Order Isomorphism is Preserved by Order Sum

== Theorem ==
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\struct {T_1, \preccurlyeq_{1'} }$ and $\struct {T_2, \preccurlyeq_{2'} }$ be ordered sets such that:
:$\struct {S_1, \preccurlyeq_1}$ is isomorphic to $\struct {T_1, \preccurlyeq_{1'} }$
:$\struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {T_2, \preccurlyeq_{2'} }$
Then the order sum $\struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {T_2, \preccurlyeq_{2'} } \oplus \struct {T_2, \preccurlyeq_{2'} }$.
== Proof ==
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $26 \ \text {(c)}$
Category:Order Sums
Category:Order Isomorphisms