Is this a correct statement of what a well-ordering of R is?
Looks OK to me, though I can’t guarantee that there isn’t a subtle oops I haven’t spotted. (Of course it assumes you’ve got some definition for what sort of a thing (a ⇐ b) is; you might e.g. use a Kuratowski ordered pair {{a},{a,b}} or something.)
Is this a correct statement of what a well-ordering of R is?
%20\land%20\forall%20B%20(B%20\subseteq%20\mathbb{R}%20\land%20B%20\neq%20\emptyset%20\implies%20\exists%20x%20\in%20B%20\forall%20y%20\in%20B%20((x%20\preceq%20y)%20\in%20A)))%0A%0A\forall%20A%20\forall%20B%20(\text{total-order}(A,%20B)%20\iff%20\forall%20a%20\forall%20b%20\forall%20c(a,%20b,%20c%20\in%20B%20\implies%20(((a%20\preceq%20b)%20\in%20A%20\lor%20(b%20\preceq%20a)%20\in%20A)%20\land%20((a%20\preceq%20b)%20\in%20A%20\land%20(b%20\preceq%20a)%20\in%20A%20\implies%20a%20=%20b)%20\land%20((a%20\preceq%20b)%20\in%20A%20\land%20(b%20\preceq%20c)%20\in%20A%20\implies%20(a%20\preceq%20c)%20\in%20A)))))Looks OK to me, though I can’t guarantee that there isn’t a subtle oops I haven’t spotted. (Of course it assumes you’ve got some definition for what sort of a thing (a ⇐ b) is; you might e.g. use a Kuratowski ordered pair {{a},{a,b}} or something.)