# Using mathematical induction on $X_n$ within the definition of $X_n$?

Assume we have a domain $$D$$ with a property $$\phi(x)$$ that is either true or false for any $$x\in D$$. Also assume that there is a function $$f:\Phi\to \Phi$$, where $$\Phi = \{x\in D:\phi(x)\}$$.

Consider the following construction: Let $$X_1$$ be a set such that for all $$x\in X_1, \phi(x)$$ holds. And define: $$X_n = \{y\in D: \exists x\in X_{n-1}, f(x)=y \}$$

I am trying to prove by mathematical induction that for all $$n, X_n\subseteq \Phi$$. This seems to me to be very obviously true and almost trivial, but I don't know how to actually prove it, since it seems we need the induction step to even define $$X_n$$. Strictly speaking, $$f(x)$$ within the definition of $$X_n$$ is undefined, since we don't know whether for arbitrary $$x\in X_{n-1}$$, $$x\in \Phi$$. So it seems we need to use mathematical induction to prove that $$X_n\in \Phi$$ before we can even define $$X_n$$.

This seems messy, so what should I do to solve this?

EDIT: Intuitively, if you think of defining $$X_n$$ as a procedure, we can simply do it like this:

Pseudocode:

i=1
prove X_1 subset of \Phi
while true
Define X_{i+1} using the fact that X_i is a subset of $$\Phi$$
Prove that X_{i+1} is a subset of $$\Phi$$.
i++;


But this would be different from mathematical induction (afaik), and I'm not sure how to formalize it mathematically.

Instead of saying $$f(x) = y$$ we can rollback to definition of function and write $$\langle x, y\rangle \in f$$ in definition of $$X_n$$ - it's well defined for any $$x, y$$.
Then we can notice that as $$f \subset \Phi \times \Phi$$, $$\langle x, y\rangle \in f$$ implies $$y \in \Phi$$.