Ill-founded trees form an analytic non-Borel set

The set $C=\{(T,x):\mathrm{\forall }nx\upharpoonright n\in T\}$ in $\mathrm{T}\mathrm{r}\times \mathcal{N}$ is closed. Failure is witnessed by n; fixing the first n coordinates of x and the tree coordinate excluding its prefix gives an open neighbourhood still failing that condition. By F2 its projection is exactly IF. Thus IF is analytic by the closed-projection convention, and its complement WF is coanalytic.

If WF were analytic, F3 with A1 would give a countable $\gamma$ strictly bounding every well-founded tree rank. F2 with A1 supplies a tree of rank $\gamma$, contradicting that strict bound. Therefore WF is not analytic. If IF were Borel its complement WF would be Borel by the sigma-algebra axiom, hence analytic by F4 and A1, again a contradiction. Thus IF is not Borel. QED.