Lemma·L60
Splitting an initial segment by a shift
The naturals below m+p split into the naturals below m together with m shifted by each natural below p.
For
:
In words
The natural numbers from 0 up to (but not including) m+p split into two pieces: the numbers below m, and m shifted up by each of the numbers below p.
Never needed: F03 · F04 · F05 · F06 · F08 · F10 · F11 · F12 · F13 · A02 · A03 · A04 · A05 · A08 (computed from the citation graph, not asserted).
Proof
- 1By induction on (with fixed), on (Separation; the set exists by Replacement applied to ).
- 2
- 3Step: assume . By D027 and D006: By the induction hypothesis, this is On the other hand, (D006), so ranging over contributes exactly the values contributed by together with the single value at : so (both sides describe exactly the same elements, by the definition of union and Extensionality). This matches computed above, so .
- 4T05 gives : the identity holds for every .
∎
Remarks
A bookkeeping fact about the von Neumann encoding, used to compute the domain of a concatenated sequence in T29 without any ad hoc case-splitting on individual elements.