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)$