Proof by Iteration It seems that I suffer the "too-much-logic-too-pedantic-too-confused"-disease. (You know? This very disease which lets you doubt everything and lets you yell for formalized proof. It's annoying, especially in real life.) 
The last days I've been trying to understand a certain argument which uses "iteration" (it is out of Hatcher's "Algebraic Topology", the proof for proposition 2B.1. a), page 169 -- but it doesn't matter, I would say). 
The generalized problem
Generalized, what I want to proof are the following two claims:
1) For an intervall $I$, assuming $A(I)$, one can construct an intervall $J$, such that 


*

*$J \subsetneqq I$, 

*$length(I) = 2\cdot length(J)$ and that 

*$A(J)$ holds. 


2) Then, by iteration, one has intervals 
$$I_0 \supsetneqq I_1 \supsetneqq \ldots$$
with $A(I_m)$ for every $m\in\mathbb{N}$.
Where I stumble
While 1) just goes through by instantiating an arbitrary interval $I$ and constructing a $J$, part 2) seems quite hard to conclude, but just in a detail. In fact, 1) is the inductive step with the exception, that I have nothing which is a successor of something, as $J$ was constructed within the induction. 
If I would have a sequence of intervals $\{I_m\}_{m\in\mathbb{N}}$, then of course, I could just run induction on it, using 1). But $I$ and $J$ are not related in this sense.
Ideas
The very first idea is: I'm just confused. This can happen from time to time, especially the more (mathematical) logic I consume. And I did.
The second idea: The sequence of intervals I would need to construct unravels (don't know if this is the right word here...). Take $I_0 = [0,1]$ for example. There are two possibilities (in Hatcher's proof) $[0,\frac{1}{2}]$ and $[\frac{1}{2},1]$. If it was the first, the sequence continues with either $[0,\frac{1}{4}]$ or $[\frac{1}{4},\frac{1}{2}]$. As I know the borders explicitly, maybe I could modify 1) into something where 
$$J = [\frac{b}{2},b]\text{ or }[a,\frac{b}{2}]$$ and use this? Not sure.
The third idea: putting the borders as a "depending sequence", $a_{n+1} = f(a_n)$, but I have no clue what that should be.
Thanks for any help.
PS: Of course, this is just about formalizing as I cannot see how to give a more pedantic proof. I see the argument, but saying "then run the argument again", which has to happen infinite times, is not a proof at all, as it would need infinite steps.
 A: It follows from the following.
Dedekind's Recursion Theorem: Given a set $X$, $x\in X$ and a map $f\colon X\to X$, there exists (one and only one) function $h\colon \mathbb N\to \mathbb X$ such that $h(0)=x$ and $\forall m\in \mathbb N(h(m+1)=f(h(m)))$.
(For a proof see, for instance, Thomas Jech's Introduction to Set Theory, (chapter 3, section 3). I finally found it on wikipedia too).
In the notation of the theorem, let $X$ be the set of all intervals, let $f$ be one of the maps given by the process described in 1 and let $x=I$. The function $h$ is your desired sequence of intervals.
A: You are actually using induction in step 2) as well, start with $I_0: A(I_0)$ (I assume $A$ is a predicate?). The step 1) gives you a new interval $I_1$ s.t. $A(I_1), I_1 \subsetneq I_0, l(I_1) = \frac12 l(I_0)$.
Now you've shown (in step 1)) that given $I_n, A(I_n)$ you can construct $I_{n+1}\subsetneq I_n, A(I_{n+1}), l(I_{n+1}) = \frac12 l(I_n)$. By induction (in step 2)) you obtain a sequence of intervals
$$(I_k)_{k=0}^\infty \text{ such that } A(I_k), l(I_k) = 2^{-k} l(I_0) \text{ and } I_j \subsetneq I_k\qquad\forall k,j\in\mathbb N, k<j$$
What you want to do with this sequence (build it's limit?) is up to you now.

The predicate used for induction will be
$$\phi(n): \exists! (I_k)_{k=0}^n, \underbrace{l(I_k) = 2^{-k} l(I_0), I_j \subsetneq I_k, A(I_k), R(I_k) = I_{k+1} \ \forall k,j\in\{1,\ldots, n\}, k<j}_{P((I_k))}$$
Where $R$ is the construction in step 1).
Then $\phi(n)$ gives you a sequence $(I_k)_{k=0}^n$ and you extend it to a sequence $(I_k)_{k=0}^{n+1}$ in the inductive step. This new sequence is a "witness" for $\phi(n+1)$ by construction, so you show $\phi(n) \Rightarrow \phi(n+1)$
The last step now is a short proof of the claim
$$\exists! (I_k)_{k=0}^\infty : P((I_k)_{k=0}^N)\ \forall N\in\mathbb N$$
Existence follows by defining $I_k := R^k(I_0)$ the $k$-times application of the reduction.
Uniqueness is given by contradiction: Assume $(I_k)$ and $(J_k)$ satisfy the claim but $I_N \ne J_N$. Then since $P((I_k)_{k=0}^N)$ and $P((J_k)_{k=0}^N)$, $\phi(N)$ implies $(I_k)_{k=0}^N = (J_k)_{k=0}^N$ contradicting the assumption.
