Suppose $\displaystyle C$ is a well orderable set, $\displaystyle f: C \times C \rightarrow C$, $\displaystyle A \subseteq C$, and let

$\displaystyle A_f =_{df} \cap \{ X \subseteq C | A \subseteq X \text{ }\& \text{ }f[X \times X] \subseteq X \}$

be the closure of $\displaystyle A$ under $\displaystyle f$. Define the sets$\displaystyle \{ A_n \}_{n \in \mathbb{N}}$ by the recursion

$\displaystyle A_0=A$, $\displaystyle A_{n+1}=A_n \cup f[A_n \times A_n]$,

and show that

$\displaystyle A_f=\cup_{n \in \mathbb{N}} A_n.$

I do not have any good ideas on how to prove this. It looks like this is true the way the sets are built up, but I do not see how to argue that. Thanks.