avewright/proofwiki-math huggingface dataset:
Theorem: Cantor-Bernstein-Schröder Theorem

If a subset of one set is equivalent to the other, and a subset of the other is equivalent to the first, then the two sets are themselves equivalent:
:$\forall S, T: T \sim S_1 \subseteq S \land S \sim T_1 \subseteq T \implies S \sim T$

Proof:
Let $\powerset A$ be the power set of $A$.
Define a mapping $E: \powerset A \to \powerset A$ thus:
:$\map E S = A \setminus g \sqbrk {B \setminus f \sqbrk S}$
=== $E$ is increasing ===
Let $S, T \in \powerset A$ such that $S \subseteq T$.
Then:
{{begin-eqn}}
{{eqn | l = f \sqbrk S
      | o = \subseteq
      | r = f \sqbrk T
      | c = Image of Subset is Subset of Image
}}
{{eqn | ll= \leadsto
      | l = B \setminus f \sqbrk T
      | o = \subseteq
      | r = B \setminus f \sqbrk S
      | c = Set Difference with Subset is Superset of Set Difference
}}
{{eqn | ll= \leadsto
      | l = g \sqbrk {B \setminus f \sqbrk T}
      | o = \subseteq
      | r = g \sqbrk {B \setminus f \sqbrk S}
      | c = Image of Subset is Subset of Image
}}
{{eqn | ll= \leadsto
      | l = A \setminus g \sqbrk {B \setminus f \sqbrk S}
      | o = \subseteq
      | r = A \setminus g \sqbrk {B \setminus f \sqbrk T}
      | c = Set Difference with Subset is Superset of Set Difference
}}
{{end-eqn}}
That is, $\map E S \subseteq \map E T$.
{{qed|lemma}}
By the Knaster-Tarski Lemma, $E$ has a fixed point $X$.
By the definition of fixed point:
:$\map E X = X$
Thus by the definition of $E$:
:$A \setminus g \sqbrk {B \setminus f \sqbrk X} = X$
Therefore:
:$(1): \quad A \setminus \paren {A \setminus g \sqbrk {B \setminus f \sqbrk X} } = A \setminus X$
Since $g$ is a mapping into $A$:
:$g \sqbrk {B \setminus f \sqbrk X} \subseteq A$
Thus by Relative Complement of Relative Complement:
:$A \setminus \paren {A \setminus g \sqbrk {B \setminus f \sqbrk X} } = g \sqbrk {B \setminus f \sqbrk X}$
Thus by $(1)$:
:$g \sqbrk {B \setminus f \sqbrk X} = A \setminus X$
Let $f' = f \restriction_{X \times f \sqbrk X}$ be the restriction of $f$ to $X \times f \sqbrk X$.
Similarly, let $g' = g \restriction_{\paren {B \setminus f \sqbrk X} \times \paren {A \setminus X} } = g \restriction_{\paren {B \setminus f \sqbrk X} \times g \sqbrk {B \setminus f \sqbrk X} }$.
By Injection to Image is Bijection, $f'$ and $g'$ are both bijections.
Define a relation $h: A \to B$ by $h = f' \cup {g'}^{-1}$.
We will show that $h$ is a bijection from $A$ onto $B$.
The domain of $f'$ is $X$, which is disjoint from the codomain, $A \setminus X$, of $g'$.
The domain of $g'$ is $B \setminus f \sqbrk X$, which is disjoint from the codomain, $f \sqbrk X$, of $f'$.
Let $h = f' \cup {g'}^{-1}$.
By {{Corollary|Union of Bijections with Disjoint Domains and Codomains is Bijection}}:
: $h$ is a bijection from $X \cup \paren {A \setminus X}$ onto $f \sqbrk X \cup \paren {B \setminus f \sqbrk X}$.
By Union with Relative Complement, $h$ is a bijection from $A$ onto $B$.
Since $f' \subseteq f$ and $g' \subseteq g$, each element of $h$ is an element of $f$ or of $g^{-1}$.
That is, if $y = \map h x$ then either $y = \map f x$ or $x = \map g y$.
{{Qed}}
Theorem: Trivial Ordering is Universally Compatible

Let $S$ be a set.
Let $\RR$ be the trivial ordering on $S$.
Then $\RR$ is universally compatible.

Proof:
To prove that the trivial ordering is in fact an ordering, we need to checking each of the criteria for an ordering:
Theorem: Identity Mapping is Order Isomorphism

Let $\struct {S, \preceq}$ be an ordered set.
The identity mapping $I_S$ is an order isomorphism from $\struct {S, \preceq}$ to itself.

Proof:
By definition:
:$\forall x \in S: \map {I_S} x = x$
So:
:$x \preceq y \implies \map {I_S} x \preceq \map {I_S} y$
As $I_S$ is a bijection, we also have:
:$\map {I_S^{-1} } x = x$
So:
:$x \preceq y \implies \map {I_S^{-1} } x \preceq \map {I_S^{-1} } y$
{{qed}}
Theorem: Identity Mapping is Order Isomorphism

Let $\struct {S, \preceq}$ be an ordered set.
The identity mapping $I_S$ is an order isomorphism from $\struct {S, \preceq}$ to itself.

Proof:
An ordered set is a relational structure where order isomorphism is a special case of relation isomorphism.
The result follows directly from Identity Mapping is Relation Isomorphism.
{{Qed}}
Theorem: Inverse of Order Isomorphism is Order Isomorphism

Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $\phi$ be a bijection from $\struct {S, \preceq_1}$ to $\struct {T, \preceq_2}$.
Then:
:$\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$
is an order isomorphism {{iff}}:
:$\phi^{-1}: \struct {T, \preceq_2} \to \struct {S, \preceq_1}$
is also an order isomorphism.

Proof:
Follows directly from the definition of order isomorphism.
Let $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$ be an order isomorphism.
Then:
:$\forall x, y, \in S: x \preceq_1 y \implies \map \phi x \preceq_2 \map \phi y$
and:
:$\forall \map \phi x, \map \phi y \in T: \map \phi x \preceq_2 \map \phi y \implies \map {\phi^{-1} } {\map \phi x} \preceq_1 \map {\phi^{-1} } {\map \phi y}$
That is:
:$\forall \map \phi x, \map \phi y \in T: \map \phi x \preceq_2 \map \phi y \implies x \preceq_1 y$
Hence the result.
{{Qed}}
Theorem: Composite of Order Isomorphisms is Order Isomorphism

Let $\struct {S_1, \preceq_1}$, $\struct {S_2, \preceq_2}$ and $\struct {S_3, \preceq_3}$ be ordered sets.
Let:
:$\phi: \struct {S_1, \preceq_1} \to \struct {S_2, \preceq_2}$
and:
:$\psi: \struct {S_2, \preceq_2} \to \struct {S_3, \preceq_3}$
be order isomorphisms.
Then $\psi \circ \phi: \struct {S_1, \preceq_1} \to \struct {S_3, \preceq_3}$ is also an order isomorphism.

Proof:
From Composite of Bijections is Bijection, $\psi \circ \phi$ is a bijection, as, by definition, an order isomorphism is also a bijection.
From Inverse of Composite Bijection, the inverse of $\psi \circ \phi$ is given by:
:$\paren {\psi \circ \phi}^{-1} = \phi^{-1} \circ \psi^{-1}$
By definition of composition of mappings:
:$\map {\psi \circ \phi} x = \map \psi {\map \phi x}$
By definition of order isomorphism, we have:
:$\phi: \struct {S_1, \preceq_1} \to \struct {S_2, \preceq_2}$ is an increasing mapping
and:
:$\psi: \struct {S_2, \preceq_2} \to \struct {S_3, \preceq_3}$ is an increasing mapping.
Hence from Composite of Increasing Mappings is Increasing:
:$\psi \circ \phi: \struct {S_1, \preceq_1} \to \struct {S_3, \preceq_3}$ is an increasing mapping.
Similarly by definition of order isomorphism:
:$\phi^{-1}: \struct {S_2, \preceq_2} \to \struct {S_1, \preceq_1}$ is an increasing mapping
and:
:$\psi^{-1}: \struct {S_3, \preceq_3} \to \struct {S_2, \preceq_2}$ is an increasing mapping.
Hence from Composite of Increasing Mappings is Increasing:
:$\phi^{-1} \circ \psi^{-1}: \struct {S_3, \preceq_3} \to \struct {S_1, \preceq_1}$ is an increasing mapping.
Hence we have that:
:$\psi \circ \phi: \struct {S_1, \preceq_1} \to \struct {S_3, \preceq_3}$ is an increasing mapping
and:
:$\paren {\psi \circ \phi}^{-1}: \struct {S_3, \preceq_3} \to \struct {S_1, \preceq_1}$ is an increasing mapping
and it follows by definition that $\psi \circ \phi$ is an order isomorphism.
{{qed}}
Theorem: Order Isomorphism is Equivalence Relation

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:
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 ===
{{:Order Isomorphism is Reflexive}}
Thus $\cong$ is seen to be reflexive.
{{qed|lemma}}
=== Symmetric ===
{{:Order Isomorphism is Symmetric}}
Thus $\cong$ is seen to be symmetric.
{{qed|lemma}}
=== Transitive ===
{{:Order Isomorphism is Transitive}}
Thus $\cong$ is seen to be transitive.
{{qed|lemma}}
$\cong$ has been shown to be reflexive, symmetric and transitive.
Hence the result.
{{qed}}
Theorem: Order Isomorphism is Equivalence Relation

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:
An ordered set is a relational structure where order isomorphism is a special case of relation isomorphism.
The result follows directly from Relation Isomorphism is Equivalence Relation.
{{qed}}
Theorem: Dual Ordering is Ordering

Let $\struct {S, \preceq}$ be an ordered set.
Let $\succeq$ denote the dual ordering of $\preceq$.
Then $\succeq$ is an ordering on $S$.

Proof:
By definition of ordering, $\preceq$ is reflexive, transitive and antisymmetric.
By definition, $\succeq$ is the inverse relation to $\preceq$.
By Inverse of Reflexive Relation is Reflexive, $\succeq$ is reflexive.
By Inverse of Antisymmetric Relation is Antisymmetric, $\succeq$ is antisymmetric.
By Inverse of Transitive Relation is Transitive, $\succeq$ is transitive.
Thus by definition $\succeq$ is an ordering on $S$.
{{qed}}
Theorem: Power Set is Complete Lattice

Let $S$ be a set.
Let $\struct {\powerset S, \subseteq}$ be the relational structure defined on the power set $\powerset S$ of $S$ by the relation $\subseteq$.
Then:
:$\struct {\powerset S, \subseteq}$ is a complete lattice
where for every subset $\mathbb S$ of $\powerset S$:
:the infimum of $\mathbb S$ necessarily admitted by $\mathbb S$ is $\bigcap \mathbb S$.

Proof:
From Set is Subset of Itself:
:$S \in \powerset S$
Let $\mathbb S$ be a non-empty subset of $\powerset S$.
From Intersection is Subset:
:$\bigcap \mathbb S \in \powerset S$
Hence, from Set of Subsets which contains Set and Intersection of Subsets is Complete Lattice:
:$\struct {\powerset S, \subseteq}$ is a complete lattice
where $\bigcap \mathbb S$ is the infimum of $\mathbb S$.
{{qed}}
Theorem: Totally Ordered Set is Lattice

Every totally ordered set is a lattice.

Proof:
Let $\struct {S, \preceq}$ be a totally ordered set.
Then we have:
:$\forall x, y \in S: x \preceq y \lor y \preceq x$
:$\forall x, y \in S: x \preceq y \implies \sup \set {x, y} = y \land \inf \set {x, y} = x$
:$\forall x, y \in S: y \preceq x \implies \sup \set {x, y} = x \land \inf \set {x, y} = y$
Thus the conditions for $\struct {S, \preceq}$ to be a lattice are fulfilled.
{{qed}}
Theorem: Trichotomy Law (Ordering)

Let $\struct {S, \preceq}$ be an ordered set.
Then $\preceq$ is a total ordering {{iff}}:
:$\forall a, b \in S: \paren {a \prec b} \lor \paren {a = b} \lor \paren {a \succ b}$
That is, every element either strictly precedes, is the same as, or strictly succeeds, every other element.
In other words, {{iff}} $\prec$ is a trichotomy.

Proof:
{{begin-eqn}}
{{eqn | q = \forall a, b \in S
      | o =
      | r = a \preceq b \lor b \preceq a
      | c = {{Defof|Total Ordering}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall a, b \in S
      | o =
      | r = a \preceq b \lor a \succeq b
      | c = {{Defof|Dual Ordering}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall a, b \in S
      | o =
      | r = \paren {a = b \lor a \prec b} \lor \paren {a = b \lor a \succ b}
      | c = Strictly Precedes is Strict Ordering
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall a, b \in S
      | o =
      | r = a \prec b \lor a = b \lor a \succ b
      | c = Rules of Commutation, Association and Idempotence
}}
{{end-eqn}}
{{qed}}
Theorem: Complement of Reflexive Relation

Let $\RR \subseteq S \times S$ be a relation.
Then $\RR$ is reflexive {{iff}} its complement $\relcomp {S \times S} \RR \subseteq S \times S$ is antireflexive.
Likewise, $\RR$ is antireflexive {{iff}} its complement $\relcomp {S \times S} \RR \subseteq S \times S$ is reflexive.

Proof:
Let $\RR \subseteq S \times T$ be reflexive.
Then:
:$\forall x \in S: \tuple {x, x} \in \RR$
By the definition of complement of $\RR$:
:$\tuple {x, y} \in \RR \implies \tuple {x, y} \notin \relcomp {S \times S} \RR$
The same applies to $\tuple {x, x}$, and thus:
:$\forall x \in S: \tuple {x, x} \notin \relcomp {S \times S} \RR$
Thus $\relcomp {S \times S} \RR$ is antireflexive.
Similarly, by definition:
:$\forall x \in S: \tuple {x, x} \notin \RR \implies \neg \tuple {x, x} \notin \relcomp {S \times S} \RR$
By Double Negation it follows that:
:$\tuple {x, x} \in \relcomp {S \times S} \RR$
The converses of these results follow from the fact that:
:$\relcomp {S \times S} {\relcomp {S \times S} \RR} = \RR$
by Relative Complement of Relative Complement.
{{Qed}}
Category:Reflexive Relations
Category:Relative Complement
iqnuxo8bs5jeattlg5gkrvi05m9rgsj
Theorem: Complement of Symmetric Relation

Let $\RR \subseteq S \times S$ be a relation.
Then $\RR$ is symmetric {{iff}} its complement $\relcomp {S \times S} \RR \subseteq S \times S$ is also symmetric.

Proof:
Let $\RR \subseteq S \times S$ be symmetric.
Then from Symmetry of Relations is Symmetric:
:$\tuple {x, y} \in \RR \iff \tuple {y, x} \in \RR$
{{AimForCont}} $\relcomp {S \times S} \RR \subseteq S \times S$ is not symmetric.
Then:
:$\exists \tuple {x, y} \in \relcomp {S \times S} \RR: \tuple {y, x} \notin \relcomp {S \times S} \RR$
But then by definition of complement of $\RR$:
:$\tuple {y, x} \in \RR$
As $\RR$ is symmetric it follows that:
:$\tuple {x, y} \in \RR$
This contradicts the premise that $\tuple {x, y} \in \relcomp {S \times S} \RR$.
Hence by Proof by Contradiction it follows that $\relcomp {S \times S} \RR$ is symmetric.
{{qed}}
The converse follows similarly.
Category:Symmetric Relations
Category:Relative Complement
cb7wsmff1zssoah1h4mh7zrao25yces
Theorem: Strictly Increasing Mapping is Increasing

A mapping that is strictly increasing is an increasing mapping.

Proof:
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$ be strictly increasing.
From Strictly Precedes is Strict Ordering:
:$x \preceq_1 y \implies x = y \lor x \prec_1 y$
So:
{{begin-eqn}}
{{eqn | l = x
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \phi x
      | r = \map \phi y
      | c = {{Defof|Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \map \phi x
      | o = \preceq_2
      | r = \map \phi y
      | c = as $\preceq_2$, being an ordering, is reflexive
}}
{{end-eqn}}
This leaves us with:
{{begin-eqn}}
{{eqn | l = x
      | o = \prec_1
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \phi x
      | o = \prec_2
      | r = \map \phi y
      | c = {{Defof|Strictly Increasing Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \map \phi x
      | o = \preceq_2
      | r = \map \phi y
      | c = Strictly Precedes is Strict Ordering
}}
{{end-eqn}}
{{Qed}}
Theorem: Strictly Decreasing Mapping is Decreasing

A mapping that is strictly decreasing is a decreasing mapping.

Proof:
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$ be strictly decreasing.
From Strictly Precedes is Strict Ordering:
:$x \preceq_1 y \iff x = y \lor x \prec_1 y$
So:
{{begin-eqn}}
{{eqn | l = x
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \phi y
      | r = \map \phi x
      | c = {{Defof|Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \map \phi y
      | o = \preceq_2
      | r = \map \phi x
      | c = as $\preceq_2$, being an ordering, is reflexive
}}
{{end-eqn}}
This leaves us with:
{{begin-eqn}}
{{eqn | l = x
      | o = \prec_1
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \phi y
      | o = \prec_2
      | r = \map \phi x
      | c = {{Defof|Strictly Decreasing Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \map \phi y
      | o = \preceq_2
      | r = \map \phi x
      | c = Strictly Precedes is Strict Ordering
}}
{{end-eqn}}
{{Qed}}
Theorem: Strictly Monotone Mapping is Monotone

A mapping that is strictly monotone is a monotone mapping.

Proof:
If $\phi$ is strictly monotone, then it is either strictly increasing or strictly decreasing.
If $\phi$ is strictly increasing, then by Strictly Increasing Mapping is Increasing, $\phi$ is increasing.
If $\phi$ is strictly decreasing, then by Strictly Decreasing Mapping is Decreasing, $\phi$ is decreasing.
Thus $\phi$ is monotone by definition.
{{qed}}
Theorem: Order Embedding into Image is Isomorphism

Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $S'$ be the image of a mapping $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$.
Then:
:$\phi$ is an order embedding from $\struct {S, \preceq_1}$ into $\struct {T, \preceq_2}$
{{iff}}:
:$\phi$ is an order isomorphism from $\struct {S, \preceq_1}$ into $\struct {S', \preceq_2 \restriction_{S'} }$.

Proof:
Let $\phi$ be an order embedding from $\struct {S, \preceq_1}$ into $\struct {T, \preceq_2}$.
Then $\phi$ is an injection into $\struct {T, \preceq_2}$ by definition.
From Restriction of Mapping to Image is Surjection, a mapping from a set to the image of that mapping is a surjection.
Thus the surjective restriction of $\phi$ onto $S'$ is an order embedding which is also a surjection.
Hence the result from Order Isomorphism is Surjective Order Embedding.
{{qed}}
Theorem: Strictly Monotone Mapping with Totally Ordered Domain is Injective

Let $\struct {S, \preceq_1}$ be a totally ordered set.
Let $\struct {T, \preceq_2}$ be an ordered set.
Let $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$ be a strictly monotone mapping.
Then $\phi$ is injective.

Proof:
{{begin-eqn}}
{{eqn | l = x, y
      | o = \in
      | r = S
      | c = 
}}
{{eqn | lo= \land
      | l = x
      | o = \ne
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \prec_1
      | r = y
}}
{{eqn | lo= \lor
      | l = y
      | o = \prec_1
      | r = x
      | c = Trichotomy Law
}}
{{eqn | ll= \leadsto
      | l = \map \phi x
      | o = \prec_2
      | r = \map \phi y
}}
{{eqn | lo= \lor
      | l = \map \phi y
      | o = \prec_2
      | r = \map \phi x
      | c = $\phi$ is strictly monotone
}}
{{eqn | ll= \leadsto
      | l = \map \phi x
      | o = \ne
      | r = \map \phi y
      | c = Definition of $\prec_2$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Mapping from Totally Ordered Set is Order Embedding iff Strictly Increasing

Let $\struct {S, \preceq_1}$ be a totally ordered set.
Let $\struct {T, \preceq_2}$ be an ordered set.
Let $\phi: S \to T$ be a mapping.
Then $\phi$ is an order embedding {{iff}} $\phi$ is strictly increasing.
That is:
:$\forall x, y \in S: x \preceq_1 y \iff \map \phi x \preceq_2 \map \phi y$
{{iff}}:
:$\forall x, y \in S: x \prec_1 y \implies \map \phi x \prec_2 \map \phi y$

Proof:
=== Forward Implication ===
Let $\phi$ be an order embedding.
Let $x, y \in S$ with $x \prec_1 y$, where $\prec_1$ is the strict predecessor relation.
Then:
{{begin-eqn}}
{{eqn | o =
      | r = x \prec_1 y \land x \ne y
      | c = {{Defof|Strictly Precedes|index = 2}}
}}
{{eqn | o = \leadsto
      | r = \map \phi x \preceq_2 \map \phi y
      | c = {{Defof|Order Embedding}}
}}
{{eqn | o = \leadsto
      | r = \map \phi x \prec_2 \map \phi y
      | c = $\phi$ is injective
}} 
{{end-eqn}}
So by definition, $\phi$ is strictly increasing.
{{qed|lemma}}
{{transclude:Mapping from Totally Ordered Set is Order Embedding iff Strictly Increasing/Reverse Implication
  |section  = proofs
  |title    = Reverse Implication
  |header   = 3
  |increase = 2
  |link     = true
}}
Theorem: Mapping from Totally Ordered Set is Order Embedding iff Strictly Increasing

Let $\struct {S, \preceq_1}$ be a totally ordered set.
Let $\struct {T, \preceq_2}$ be an ordered set.
Let $\phi: S \to T$ be a mapping.
Then $\phi$ is an order embedding {{iff}} $\phi$ is strictly increasing.
That is:
:$\forall x, y \in S: x \preceq_1 y \iff \map \phi x \preceq_2 \map \phi y$
{{iff}}:
:$\forall x, y \in S: x \prec_1 y \implies \map \phi x \prec_2 \map \phi y$

Proof:
Let $x \preceq_1 y$.
Then $x = y$ or $x \prec_1 y$.
Let $x = y$.
Then
:$\map \phi x = \map \phi y$
so:
:$\map \phi x \preceq_2 \map \phi y$
Let $x \prec_1 y$.
Then by the definition of strictly increasing mapping:
:$\map \phi x \prec_2 \map \phi y$
so by the definition of $\prec_2$:
:$\map \phi x \preceq_2 \map \phi y$
Thus:
:$x \preceq_1 y \implies \map \phi x \preceq_2 \map \phi y$
It remains to be shown that:
:$\map \phi x \preceq_2 \map \phi y \implies x \preceq_1 y$
Suppose that $x \npreceq_1 y$.
Since $\preceq_1$ is a total ordering:
:$y \prec_1 x$
Thus since $\phi$ is strictly increasing:
:$\map \phi y \prec_1 \map \phi x$
Thus:
:$\map \phi x \npreceq_1 \map \phi y$
Therefore:
:$x \npreceq_1 y \implies \map \phi x \npreceq_2 \map \phi y$
By the Rule of Transposition:
:$\map \phi x \preceq_2 \map \phi y \implies x \preceq y$
{{qed}}
Theorem: Mapping from Totally Ordered Set is Order Embedding iff Strictly Increasing

Let $\struct {S, \preceq_1}$ be a totally ordered set.
Let $\struct {T, \preceq_2}$ be an ordered set.
Let $\phi: S \to T$ be a mapping.
Then $\phi$ is an order embedding {{iff}} $\phi$ is strictly increasing.
That is:
:$\forall x, y \in S: x \preceq_1 y \iff \map \phi x \preceq_2 \map \phi y$
{{iff}}:
:$\forall x, y \in S: x \prec_1 y \implies \map \phi x \prec_2 \map \phi y$

Proof:
Let $\phi$ be strictly increasing.
Let $\map \phi x \preceq_2 \map \phi y$.
As $\struct {S, \prec_1}$ is a strictly totally ordered set:
:Either $y \prec_1 x$, $y = x$, or $x \prec_1 y$.
{{AimForCont}} that $y \prec_1 x$.
By the definition of a strictly increasing mapping:
:$\map \phi y \prec_2 \map \phi x$
which contradicts the fact that $\map \phi x \preceq_2 \map \phi y$.
Therefore $y \nprec_1 x$.
Thus $y = x$, or $x \prec_1 y$, so $x \preceq_1 y$.
Hence:
:$\map \phi x \preceq_2 \map \phi y \iff x \preceq_1 y$
and $\phi$ has been proved to be an order embedding.
{{qed}}
Theorem: Finite Totally Ordered Set is Well-Ordered

Every finite totally ordered set is well-ordered.

Proof:
Let $\struct {S, \preceq}$ be a finite totally ordered set.
{{AimForCont}} $\preceq$ is not a well-founded relation.
From Infinite Sequence Property of Well-Founded Relation, $\struct {S, \preceq}$ is well-founded {{iff}} there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that $\forall n \in \N: a_{n + 1} \prec a_n$.
Let us construct such an infinite sequence.
Then at least some of the terms would be repeated in that sequence.
So there would be, for example:
:$s_i \preceq s_j \preceq s_k \preceq s_i$
But then we have:
:$s_i \preceq s_j$ and $s_j \preceq s_k$
and as $\preceq$ is transitive, we have:
:$s_i \preceq s_k$
But as we also have $s_k \preceq s_i$
we have $s_i \preceq s_k$ and $s_k \preceq s_i$ where $s_i \ne s_k$.
That is, $\preceq$ is not antisymmetric.
That is, $\preceq$ is therefore not a totally ordered set.
From this contradiction it follows that $\preceq$ is well-founded.
The result follows from the definition of well-ordered set.
{{qed}}
Theorem: Subset of Well-Ordered Set is Well-Ordered

Let $\struct {S, \preceq}$ be a well-ordered set.
Let $T \subseteq S$ be a subset of $S$.
Let $\preceq'$ be the restriction of $\preceq$ to $T$.
Then the relational structure $\struct {T, \preceq'}$ is a well-ordered set.

Proof:
First suppose that $T = \O$.
From Empty Set is Subset of All Sets, $T$ is a subset of $S$.
By Empty Set is Well-Ordered, $\struct {\O, \preceq'}$ is a well-ordered set. 
Otherwise, let $T$ be non-empty.
Let $X \subseteq T$ such that $X \ne \O$ be arbitrary.
Such a subset exists, as from Set is Subset of Itself, $T$ itself is a subset of $T$.
By Subset Relation is Transitive, $X \subseteq S$.
By the definition of a well-ordered set, $X$ has a smallest element under $\preceq$.
That is:
:$\forall y \in S: x \preceq y$
Hence as $T \subseteq S$:
:$\forall y \in T: x \preceq y$
Because $\preceq'$ is the restriction of $\preceq$ to $T$:
:$\forall y \in T: x \preceq' y$
and so $x$ is the smallest element of $X$ under $\preceq'$.
It follows by definition that $\struct {T, \preceq'}$ is a well-ordered set.
{{qed}}