Can we add a primitive binary relation $<$ to the language of ZFC, and add the following axioms on top of axioms of ZFC?
- Well ordering: $<$ is a well ordering on the universe.
- Membership: $x \in y \to x < y$
Where 1. is the following schema:
$x < y \to y \not < x \\ x < y < z \to x < z \\ x \neq y \leftrightarrow [x < y \lor y < x] \\ \exists x \phi(x) \to \exists x \phi(x) \land \forall y (\phi(y) \to x \leq y)$
Whenever $E$ is a well-founded and set-like relation on a class $A$, and there is some (class) well-order $\triangleleft$ on $A$ then there is a (class) well-order on $A$ containing $E$.
Namely consider the rank function $\rho \colon A \to ON$ associated with $E$. This is definable. Then we define $x <' y$ iff $\rho(x) < \rho(y)$ or $\rho(x) = \rho(y)$ and $x \triangleleft y$, which is a well-order on $A$ containing $E$, since if $x E y$, then $\rho(x) < \rho(y)$.