[proofplan] Reflexivity is witnessed by the identity map on each cardinal. Transitivity follows by composing the two injections witnessing the two inequalities. For antisymmetry, mutual injections give an equinumerosity by the Schröder-Bernstein theorem; since cardinals are initial ordinals, two distinct cardinals cannot be equinumerous, so the cardinals must be equal. [/proofplan] [step:Use identity maps to prove reflexivity] Let $\kappa \in \mathrm{Card}$. Define the identity map \begin{align*} \operatorname{id}_\kappa: \kappa &\to \kappa \\ \alpha &\mapsto \alpha . \end{align*} If $\operatorname{id}_\kappa(\alpha) = \operatorname{id}_\kappa(\beta)$ for $\alpha, \beta \in \kappa$, then $\alpha = \beta$, so $\operatorname{id}_\kappa$ is injective. Hence $\kappa \le \kappa$ by the definition of the cardinal order. [/step] [step:Compose injections to prove transitivity] Let $\kappa, \lambda, \mu \in \mathrm{Card}$, and suppose $\kappa \le \lambda$ and $\lambda \le \mu$. By definition, there exist injective maps \begin{align*} f: \kappa &\to \lambda, \\ g: \lambda &\to \mu . \end{align*} Define the composite map \begin{align*} g \circ f: \kappa &\to \mu \\ \alpha &\mapsto g(f(\alpha)). \end{align*} To prove injectivity, let $\alpha, \beta \in \kappa$ and suppose $(g \circ f)(\alpha) = (g \circ f)(\beta)$. Since $g$ is injective, $f(\alpha) = f(\beta)$. Since $f$ is injective, $\alpha = \beta$. Therefore $g \circ f$ is injective, and hence $\kappa \le \mu$. [/step] [step:Use mutual injections to obtain an equinumerosity] Let $\kappa, \lambda \in \mathrm{Card}$, and suppose $\kappa \le \lambda$ and $\lambda \le \kappa$. By definition, there exist injective maps \begin{align*} f: \kappa &\to \lambda, \\ g: \lambda &\to \kappa . \end{align*} By the Schröder-Bernstein theorem, the existence of injections in both directions implies that there exists a bijective map \begin{align*} h: \kappa &\to \lambda . \end{align*} Thus $\kappa$ and $\lambda$ are equinumerous, which we denote by $\kappa \approx \lambda$. Here the cited result is not yet resolved in the wiki: Schröder-Bernstein Theorem. [guided] We must prove antisymmetry, so we begin with two cardinals $\kappa, \lambda \in \mathrm{Card}$ satisfying both inequalities $\kappa \le \lambda$ and $\lambda \le \kappa$. By the definition of $\le$ on cardinals, these two inequalities mean exactly that there are injective maps \begin{align*} f: \kappa &\to \lambda, \\ g: \lambda &\to \kappa . \end{align*} The purpose of introducing both maps is to use the Schröder-Bernstein theorem: whenever there is an injection from one set into another and an injection back, the two sets have the same cardinality. Applying that theorem to the sets underlying the ordinals $\kappa$ and $\lambda$, we obtain a bijective map \begin{align*} h: \kappa &\to \lambda . \end{align*} Therefore $\kappa$ and $\lambda$ are equinumerous. We write this as $\kappa \approx \lambda$. The cited result is not yet resolved in the wiki: Schröder-Bernstein Theorem. [/guided] [/step] [step:Use initiality of cardinals to prove antisymmetry] It remains to show that $\kappa \approx \lambda$ forces $\kappa = \lambda$. Since $\kappa$ and $\lambda$ are cardinals, they are initial ordinals: no ordinal strictly smaller than either one is equinumerous with it. Assume for contradiction that $\kappa \ne \lambda$. Since ordinals are linearly ordered by membership, either $\kappa < \lambda$ or $\lambda < \kappa$. If $\kappa < \lambda$, then $\kappa$ is an ordinal strictly smaller than the initial ordinal $\lambda$, while $\kappa \approx \lambda$, contradicting the initiality of $\lambda$. If $\lambda < \kappa$, the same argument contradicts the initiality of $\kappa$. Both cases are impossible, so $\kappa = \lambda$. Therefore $\le$ is reflexive, transitive, and antisymmetric on $\mathrm{Card}$, hence it is a partial order. [/step]