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$.