Recursion for deterministic finite graph updates

By F5 every $n\in \mathbb{N}$ is finite. Every finite ordinal $n$ is a subset of $\mathbb{N}$, and every edge of a simple graph on $n$ is a subset of $\mathbb{N}$. Thus each such graph $(n,E)$ belongs to $\mathbb{N}\times \mathcal{P}(\mathcal{P}(\mathbb{N}))$. By Separation, the members of this product for which $E$ consists of two-element subsets of $n$ form a set $X$; these are exactly the stated graphs, since every selected vertex set $n$ is finite.

Apply recursion to the set $X$, initial value $J_1$, and self-map $T$. It yields a unique $g:\mathbb{N}\to X$ with $g(0)=J_1$ and $g(\sigma (n))=T(g(n))$. Define $J_{\sigma (n)}=g(n)$ for every $n\in \mathbb{N}$. The relation $\{(\sigma (n),g(n)):n\in \mathbb{N}\}$ exists by Separation inside $\mathbb{N}\times X$. Every positive natural number has a unique predecessor in the Peano system, so this relation is a function on precisely the positive indices in the sense of F4; its first term is $J_1$ and $J_{r+1}=T(J_r)$.

Conversely, shifting any sequence satisfying those initial and update equations back by one index gives a function satisfying the recursion equations for $g$; uniqueness in recursion therefore makes the sequence unique. Every term is in $X$, so every term is a finite simple graph.

Let $P$ be a property of elements of $X$ holding at $J_1$ and preserved by $T$. The property $P(g(n))$ holds at $0$ and, by the recursion equation and preservation, passes from $n$ to $\sigma (n)$. Induction gives $P(g(n))$ for every $n$, hence $P(J_r)$ for every positive stage $r$. This proves the assertions.