Borel payoffs admit unraveling covers

At rank one, F2 handles open and closed payoffs. At any rank a covering unraveling a set also unravels its complement, since the inverse images are relative complements and the complement of a clopen set is clopen. Thus at a higher rank $\alpha$ it suffices to handle $A={\bigcup }_n{B}_n$ where $B_n\in {\mathrm{\Pi }}_{{\beta }_n}^0([T])$ and $1\le {\beta }_n<\alpha$. Assume by F5 that the theorem holds for all lower ranks and all the quantified parameters.

We justify the dependent sequence of cover choices before using it. A state is a finite tower over this fixed $T$, together with its last projection to $T$; a valid successor adds a covering of its last tree unraveling the next pulled-back $B_n$ at depth $k+n$. By F4 that projection is continuous; F1 preserves ${\beta }_n$ under pullback. The induction hypothesis therefore supplies at least one successor state for every valid state. Use F6 to define $W(s)$ as the set of all valid successors of least member-rank. It is nonempty. On an invalid state define $W(s)=\{s\}$, so this is a definable set-valued operation on every input.

Starting with the singleton of the length-zero tower, define $D_{n+1}=D_n\cup {\bigcup }_{s\in D_n}W(s)$. Replacement and Union form each right side, and F7 forms the sequence (with empty-set default for malformed histories). Then $D={\bigcup }_n{D}_n$ is a set and $W(s)\subseteq D$ for every $s\in D$. A1 chooses $w(s)\in W(s)$ on this set-indexed family. Recursion by F7, $s_{n+1}=w(s_n)$, starting at the valid length-zero state, yields only valid towers of length $n$, since every member of $W(s_n)$ is a valid extension. We have consequently constructed $T_0=T$ and $(k+n)$-coverings $T_{n+1}\to T_n$ unraveling the pullback of $B_n$ to $T_n$. This uses choice on a set, not a choice function on a proper class.

Compose adjacent coverings by F4 to get coherent maps ${\pi }_{j,i}$. They are all $k$-coverings. Given depth $m$, choose $N$ with $k+N\ge m$; every adjacent map beyond $N$ and hence every composite beyond $N$ is identity through that depth, on nodes, taboo labels and the stipulated strategy restrictions. Thus F3 applies and gives $T_{\mathrm{\infty }}$ with coherent $k$-coverings ${\pi }_{\mathrm{\infty },i}$. For each $n$, the inverse image of $B_n$ in $T_{n+1}$ is clopen by the construction, and F4 makes its further pullback to $T_{\mathrm{\infty }}$ clopen. Coherence identifies this pullback with ${\pi }_{\mathrm{\infty },0}^{-1}(B_n)$.

Their union $O={\pi }_{\mathrm{\infty },0}^{-1}(A)$ is open. Apply F2 on the taboo tree $T_{\mathrm{\infty }}$ to $O$ at depth $k$, obtaining a covering $S\to T_{\mathrm{\infty }}$ with clopen inverse image of $O$. Compose with $T_{\mathrm{\infty }}\to T$ by F4. The composite is a $k$-covering, and its inverse image of $A$ is exactly that clopen set. This proves the progressive step; F5 proves all positive ranks, and exhaustion F1 includes every Borel payoff. Empty and whole payoffs are already in the base case. QED.