How much Replacement does this axiom provide?

Question

(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'$.

Answer 1

Asaf points out that Axiom A is true in $V_{\delta}$ if $\delta$ is a $\beth$ fixed point. Full replacement only holds if $\delta$ is worldly. So, in $V_{\delta}$ models of these, replacement implies a proper class of $\beth$ fixed points (since all worldly cardinals are $\beth$ fixed point-sized limits of $\beth$ fixed points), but Axiom A is compatible with the statement that there are no $\beth$ fixed points. In fact, ZFC does proves that there's a proper class of $\beth$ fixed points, since for any ordinal $\alpha$ the limit of the sequence $\beta_0 = \alpha; \beta_{n+1} = \beth_{\beta_{n}}$ is a $\beth$ fixed point greater than $\alpha$.

Answer 2

The principle is essentially asserting that $\aleph_\alpha$ exists for every ordinal $\alpha$. More precisely, it asserts that for every well-order type $\alpha$, there is a set of cardinality $\aleph_\alpha$; the difference is that without the replacement axiom, one doesn't necessarily have the usual von Neumann ordinals.

This axiom is not provable in Zermelo set theory, since $V_{\omega+\omega}$ models the Zermelo theory, but it has only countably many infinite cardinals, and so $\aleph_{\omega+\omega}$ does not exist in this model, even though there are orders of type $\omega+\omega$ there.

The axiom is provable in ZFC and is strictly weaker than ZFC, as has been pointed out by B2C, since $V_\kappa$ is a model of the principle if and only if $\kappa$ is a beth-fixed point $\kappa=\beth_\kappa$.

What I would like to mention is that the principle is a natural instance of the principle of recursion:

Principle of transfinite recursion. (See the account on my blog) If $A$ is any set with well-ordering $<$ and $F:V\to V$ is any class function, then there is a function $s:A\to V$ such that $s(b)=F(s\upharpoonright b)$ for all $b\in A$, where $s\upharpoonright b$ denotes the function $\langle s(a)\mid a<b\rangle$.

In my blog post, The axiom of well-ordered replacement is equivalent to full replacement over Zermelo + foundation, I explain how Alfredo Roque Freire and I had realized that the axiom of well-ordered replacement is equivalent to the full replacement axiom, over the Zermelo set theory with foundation. From this it follows that the principle of transfinite recursion is equivalent to the axiom of replacement.

Corollary. The principle of transfinite recursion is equivalent to the replacement axiom over Zermelo set theory with foundation.

ZF = Z + foundation + transfinite recursion

There is no need for the axiom of choice.

My perspective is that the axiom A of the question is naturally seen as an instance of the principle of transfinite recursion, which naturally generalizes it. By adopting that principle, one arrives at ZF set theory and the axiom of replacement.