# Does a hereditary size set exist for every set in ZF-Regularity+Aczel's anti-foundation axiom?

It is known that: $\forall x \exists H_x"$, where $H_x$ is defined as the set of all sets hereditarily subnumerous to $x$, is a theorem of $\text{ZF}$. The formal definition of $H_x$ is:

$$H_x=\{y| \forall z \in TC(\{y\}) (\exists f (f:z \to x \wedge f \text{ is injective}))\}$$, where $TC(k)$ stands for the "Transitive closure of($k$)" defined in the standard manner as the minimal transitive superset of $k$.

Question: is $\forall x \exists H_x"$ a thorem of "$\text{ZF-Regularity + Aczel's anti-foundation axiom}$"?

• It would be very advisable, if you want more people to understand your questions, that you use actually standard terminology, and not things you expect everyone to understand. What is "subnumerous"? What is "hereditarily subnumerous"? Since you're familiar with the notation $H_x$, surely you are familiar with the more formal definition of "the transitive closure of $y$ has a strictly smaller cardinality than $x$". No? Then why invent new terms? We have too many already. – Asaf Karagila Jun 29 '18 at 19:44
• honestly I thought those terminologies are well understood. Anyhow I'll try to edit with some detail. – Zuhair Al-Johar Jun 29 '18 at 19:57

The reason is that in AFA, every set is determined by the isomorphism type of the $\in$ relation on its transitive closure. So if a set $y$ hereditarily injects into another set $x$, then the transitive closure of $y$ is determined by a certain graph relation on the nodes coming from the graph of $x$. By suitable applications of the power set axiom and separation, the collection of all such graphs exists as a set, and the sets to which they correspond exists by the replacement axiom. So $H_x$ exists.