@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.

So we have { 1, 2 } ∈ Fin₁ ⊆ Fin₁ₐ ⊆ Fin₂ ⊆ Fin₃ ⊆ Fin₄ ⊆ Fin₅ ⊆ Fin₆ ⊆ Fin₇

If a set is in Fin₁ then it is considered finite by all the other definitions.

But since the axiom of choice is equivalent to saying every set can be well-ordered, if we accept it VII-finite sets are equinumerous with a finite ordinal and so Fin₇ ⊆ Fin₁ and so the differences between these definitions collapse and ZF becomes ZFC, which is a widely accepted basis for Set Theory.

My consultation with math resources was inspired by a blog post:

https://www.infinitelymore.xyz/p/what-is-the-infinite

#Metamath #ZFC #SetTheory #AxiomOfChoice #FiniteSet #Infinity

Also from #Metamath I learned #infinity is hard to think about.

A . Lévy in "The independence of various definitions of finiteness" Fundamenta Mathematicae, 46:1-13 (1958) established 8 distinct set-theoretic definitions of a #finiteSet which in ZF cannot be equated without the #AxiomOfChoice

I-finite -- equinumerous with a finite ordinal. // i.e. admits a finite well-order (Numerically Finite) ⟺ the powerset of its powerset is Dedekind finite ⟺ every collection of its subsets has a maximum element ⟺ every collection of subsets has a minimal element

Ia-finite -- not the union of two sets which are not I-finite

II-finite -- every possible way of finding within the set a chain of nested subsets always contains a maximum element (Tarski finite) ⟺ equivalently every such chain contains its intersection ⟺ (Linearly Finite) ⟺ (Stäckel Finite)

|||-finite -- It's powerset is |V-finite finite, (weakly Dedekind finite) ⟺ cannot be mapped onto ordinal ω ⟺ doesn't contain a chain of subsets which can be placed in order with ω

|V-finite -- doesn't have a proper subset which is equinumerous to itself. (Dedekind finite) ⟺ there is no 1-1 map from ordinal ω to it ⟺ it is strictly dominated by the disjoint sum of it and a singleton (acts finite under successor)

V-finite -- it is either empty or strictly dominated by the disjoint sum of it with itself (acts finite under addition)

VI-finite -- it is either empty, a singleton or strictly dominated by the Cartesian product of it with itself (acts finite under multiplication)

VII-finite -- it cannot be infinitely well-ordered (not equiinumerous with the ordinal ω or any larger ordinal)