Well-founded pointed graphs have unique decorations

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

An accessible pointed graph consists of a set $X$ of nodes, a root $r\in X$, and a relation $R\subseteq X^2$. Draw an arrow $x\to y$ precisely when $yRx$. Accessibility means that for every $x\in X$ there are $n\in \omega$ and a function $p:n+1\to X$ with $p(0)=r$, $p(n)=x$, and $p(i+1)Rp(i)$ for $i<n$. The path of length zero reaches the root. A decoration is a set function $d$ on $X$ such that $d(x)=\{d(y):yRx\}$ for each node. A well-founded graph means that $R$ has the minimal-element property, not an unqualified no-infinite-path characterization. Extensionality is not part of the graph definition. No axiom of anti-foundation is assumed. Conventions and prerequisites: def-well-founded-setlike-relations. (Accessible pointed membership graphs)

A setlike relation $R$ on $X$ is extensional when ${\mathrm{pred}}_R(x)={\mathrm{pred}}_R(y)$ implies $x=y$ for $x,y\in X$. If $R$ is also well-founded, its collapse map is the unique definable function $\pi (x)=\{\pi (y):yRx\}\mathrm{.}$ Existence and uniqueness follow from well-founded recursion with $G(x,h)=\mathrm{ran}(h)$, a set by Replacement. A collapse map is defined even without extensionality; injectivity is a further conclusion requiring extensionality. The construction for a supplied well-founded relation uses no ambient Foundation. Conventions and prerequisites: thm-recursion-on-well-founded-setlike-relations. (Extensional relations and collapse maps)

For every set $a$, $\mathrm{TC}(a)$ is transitive, contains $a$ as a subset, and is contained in every transitive set $T$ with $a\subseteq T$. Moreover $a\subseteq b$ implies $\mathrm{TC}(a)\subseteq \mathrm{TC}(b)$, and $\mathrm{TC}(\mathrm{TC}(a))=\mathrm{TC}(a)$. In particular $a\in \mathrm{TC}(\{a\})$. (Minimality and closure laws of TC)

Every well-founded setlike extensional relation $R$ on a definable class $X$ is isomorphic to membership on a unique transitive definable class $Y$, by a unique definable isomorphism $\pi :X\to Y$. For a set domain $X$, the isomorphism and its image are sets. This holds without ambient Foundation. (Mostowski collapse for extensional relations)