(There have been many questions on MathOverflow about the axiom scheme of replacement, including a few with a similar flavour to mine. Some have very informative answers and link to excellent papers and blog posts. I've spent a while reading the older questions etc., and as far as I know, my question isn't answered in any of them — but it's entirely possible that it is and I missed it. In that case, I'll be grateful if someone points out where.)

Consider the following statement about sets and functions, which I'll call "axiom A":

A.For all well-ordered sets $(B, \leq)$, there exist a set $X$ and a function $p: X \to B$ with the following property:for all $b \in B$, the fibre $p^{-1}(b)$ is an infinite set of smallest cardinality greater than that of $p^{-1}(b')$ for each $b' < b$.

In the traditional notation of set theory, if $(B, \leq)$ is an ordinal $\beta$, then $p^{-1}(\alpha) \cong \aleph_\alpha$ for each $\alpha \in \beta$. So, $X$ is the disjoint union $\coprod_{\alpha \in \beta} \aleph_\alpha$ and $p: X \to \beta$ is the obvious projection.

My question is about ETCS (Lawvere's Elementary Theory of the Category of Sets) together with axiom A. In what follows, I'm going to take ETCS as the background theory. Thus, when I say "*this* is weaker than *that*", I mean weaker in the presence of ETCS.

On the one hand, A isn't a theorem of ETCS (unless, of course, ETCS is inconsistent). That's because ETCS+A proves the existence of $\aleph_\omega$ but ETCS alone doesn't.

On the other, if I'm not mistaken, A is weaker than replacement. That's because ETCS+replacement is bi-interpretable with ZFC, and unless I'm misremembering, the fact that ETCS+A is a *finite* list of axioms (not involving axiom *schemes*) somehow implies that it can't be as strong as ZFC.

So, it seems that axiom A is a weaker form of replacement. My question:

To what fragment of replacement is axiom A equivalent (in the presence of the axioms of ETCS)?

That question is a little vague, so let me focus it more:

What's the simplest statement you can think of that's true in ETCS+replacement (or equivalently ZFC) but not provable in ETCS+A?

I don't mind whether the statement is purely set-theoretic or from another part of mathematics.

**Added later** Incidentally, "axiom A" is equivalent (under ETCS) to the following simpler statement:

for every set $B$, there exists a map into $B$ whose fibres all have different cardinalities.

Formally: for all sets $B$, there exist a set $X$ and a map $p: X \to B$ such that for all $b, b' \in B$, if $p^{-1}(b) \cong p^{-1}(b')$ then $b = b'$.

8more comments