Does the theory of infinite sets in the language of pure equality have a non-redundant axiomatization?

Question

This is a follow-up to a previous question. Consider the theory of infinite sets in the language of pure equality. Is there a set of axioms that axiomatize that theory where no axiom is redundant?

Answer 1

It is easy enough to write a sentence that means (for an $n$ given at the metalevel)

There are at least $n$ different things.

namely

$$ \forall x_1 \forall x_2 \cdots \forall x_{n-1} \exists y (y\ne x_1 \land \cdots \land y \ne x_{n-1} ) $$

Therefore you can also write a sentence that means

There are exactly $n$ different things.

(Namely, there are at least $n$ different things, but there are not at least $n+1$ different things).

Now your independent axiomatization could consist of the negation of the latter sentence for each possible $n$.