Order Theory/Preordered classes and poclasses

Definition (preordered class):

A preordered class is a set $S$ together with a binary relation $\leq \subset S\times S$ satisfying the following axioms:

1. $\forall s\in S:s\leq s$ (reflexivity)
2. $\forall r,s,t\in S:(s\leq r\wedge r\leq t\Rightarrow s\leq t)$ (transitivity)

Definition (poclass):

A poclass (shorthand for partially ordered class) is a preordered class $(S,\leq )$ such that the following additional axiom is satisfied:

3. $\forall s,t\in S:s\leq t\wedge t\leq s\Rightarrow s=t$ (antisymmetry)

Example (subsets of the power set are ordered by inclusion):

Let $S$ be any set, and let $\sigma \subset {\mathcal {P}}(X)$. Then the relation on $\sigma$ defined by

$S\leq T:\Leftrightarrow S\subseteq T$

is an order on $\sigma$.

Definition (order homomorphism):

Let $(S,\leq )$ and $(T,\preceq )$ be preordered classes. An order homomorphism from $(S,\leq )$ to $(T,\preceq )$ is a class function $f:S\to T$ so that $x\leq y\Rightarrow f(x)\preceq f(y)$ for all $x,y\in S$.

Definition (isotonic class function):

Let $S,T$ be sets, and let $\leq _{S}$ be a preorder on $S$, and $\leq _{T}$ a preorder on $T$. A class function $f:S\to T$ is said to be isotonic with respect to $\leq _{S}$ and $\leq _{T}$ iff $f$ is an order homomorphism from $(S,\leq _{S})$ to $(T,\leq _{T})$.

Definition (antitonic class function):

Let $S,T$ be sets with preorders $\leq _{S},\leq _{T}$ respectively. Then an antitonic class function from $S$ to $T$ with respect to the partial orders $\leq _{S}$ and $\leq _{T}$ is a class function $f:S\to T$ such that

$x\leq _{S}y\Rightarrow f(y)\leq _{T}f(x)$.

Definition (product order):

Let $(S_{\alpha },\leq _{\alpha })_{\alpha \in A}$ be a family of preordered classes. The product order on the cartesian product $\prod _{\alpha \in A}S_{\alpha }$ is the order given by

$(s_{\alpha })_{\alpha \in A}\leq (t_{\alpha })_{\alpha \in A}:\Leftrightarrow \forall \alpha \in A:s_{\alpha }\leq t_{\alpha }$.