Solution (source code)

= Solution

Work in a background model of <ZFC>. Each structure below satisfies every axiom of <ZF> except the indicated one and falsifies that axiom; the background model supplies the other consistency direction.

For the <Axiom of union>, put $\lambda=\beth_\omega$ and use the <hereditarily locally small membership model>
$$
B_\lambda=\{x:(\forall y\in\operatorname{TC}(\{x\}))\ |y|<\lambda\}.
$$
The <transitive class> $B_\lambda$ inherits <extensionality> and <foundation>. Definable subsets of its sets remain in it. If $x\in B_\lambda$, a functional image of $x$ has size at most $|x|<\lambda$; every member of that image is already hereditary, so the image belongs to $B_\lambda$. This verifies <replacement>, even though its values can have unbounded ranks. Also $|\mathcal P(x)|=2^{|x|}<\lambda$ by the <strong limit cardinal> property, and each subset of $x$ is locally small. This verifies the <Axiom of power set>. Pairing and <infinity> follow similarly. But
$$
A=\{V_{\omega+n}:n<\omega\}\in B_\lambda,\qquad
\bigcup A=V_{\omega+\omega}\notin B_\lambda,
$$
since $|V_{\omega+n}|=\beth_n<\lambda$ while $|V_{\omega+\omega}|=\lambda$. This is failure of sumset without failure of <replacement> or <power set>.

For the <Axiom of power set>, use the <hereditarily countable sets> $H_{\omega_1}$. This is a <transitive class>. A countable union of countable <transitive closures> is countable, so it is closed under pairs, unions and functional images of its countable domains; these facts verify <pairing>, <union> and <replacement>. <Separation>, <foundation> and <infinity> also hold. Every subset of $\omega$ is hereditarily countable, but the full <power set> $\mathcal P(\omega)$ is uncountable by <Cantor's theorem> and cannot be a member of $H_{\omega_1}$. Since every candidate internal power set would have to contain all those subsets, the power-set axiom fails.

For <replacement>, take the rank-initial <transitive set> $V_{\omega+\omega}$. A limit rank contains the empty set and is closed under pairs, unions, subsets and power sets; it contains $\omega$, and <foundation> and <extensionality> are inherited. Fix the parameter $V_\omega$. The definable map
$$
n\longmapsto\mathcal P^n(V_\omega)=V_{\omega+n}
$$
is internally described by a finite sequence of power-set iterations. Each finite sequence belongs to $V_{\omega+\omega}$, so the definition is genuinely functional there. Its range has rank $\omega+\omega$ and is not in the structure. Thus this instance of <replacement> fails.

For <extensionality>, use the <non-extensional membership model with one atom>. Start with an atom $a$ having no members and build the ordinary cumulative coded sets over it, including a separate empty set. Interpret membership by the contents of a set code and give $a$ no members. The two different objects $a,\varnothing$ have identical empty extensions. <Foundation> holds by the code ranks; pure finite ordinals give <infinity>; pairs, unions, definable subsets and functional ranges have their usual set codes. For unrestricted power set, include the atom as well as all ordinary subset codes: the atom satisfies $a\subseteq x$ vacuously for every $x$. This detail is necessary because the formulas here are the unmodified <ZF> formulas, without a set predicate. The collection still has a set code, so the <Axiom of power set> holds. All axioms except <extensionality> are satisfied.

Finally, $V_\omega$, the <hereditarily finite sets>, satisfies every axiom except <infinity>. Pairs, unions, power sets and subsets of finite sets are finite, and every functional image of a finite domain is finite, so the full <replacement> schema holds. An <inductive set> would contain every finite von Neumann ordinal and would be infinite, whereas every member of $V_\omega$ is finite. Hence <infinity> fails.