Every well-ordered set is isomorphic to an ordinal. Common notion, for example see Introduction to https://arxiv.org/abs/2409.07352
β’((π΄βVβ§π Weπ΄)ββπ(domπβOnβ§πIsomE,π (domπ,π΄)))
\[ \vdash ( ( A \in \mathrm{V} \wedge R \mathrm{We} A ) \leftrightarrow \exists f ( \mathrm{dom} f \in \mathrm{On} \wedge f \mathrm{Isom} \mathrm{E} , R ( \mathrm{dom} f , A ) ) ) \]
Every well-ordered set is isomorphic to
a unique ordinal.
β’((π΄βVβ§π Weπ΄)ββ!πβOnβπβ(π΄ββπ)πIsomE,π (π,π΄))
\[ \vdash ( ( A \in \mathrm{V} \wedge R \mathrm{We} A ) \leftrightarrow \exists{!} o \in \mathrm{On} \exists f \in ( A \uparrow_\mathrm{m} o ) f \mathrm{Isom} \mathrm{E} , R ( o , A ) ) \]
We can phrase the Axiom of Choice as "Every set injects into an ordinal."
β’(CHOICEββπ₯βπβOnπ₯βΌπ)
\[ \vdash ( \mathrm{CHOICE} \leftrightarrow \forall x \exists o \in \mathrm{On} x \preccurlyeq o ) \]
