@FishFace Update:

What I refer to as EScbO is usually called #LO the #LinearOrdering principle.

⊢ ∃y ∀a ∈ x ∀b ∈ x ∀c ∈ x (¬ aya ∧ ((ayb ∧ byc) → ayc) ∧ (ayb ∨ a = b ∨ bya))
or using abbreviations in #Metamath
⊢ ∃y y Or x

I think AC implies LO, but LO is independent of DC and CC.