Recognizable extensional properties are positively witnessed by finite information

By [L2], $\overline{A_{TM}}$ is not recognizable: otherwise both $A_{TM}$ and its complement would be recognizable and hence $A_{TM}$ would be decidable.

Choose a recognizer for $A$, and let $\mathrm{\Sigma }$ be its finite input alphabet. Dovetail the recognizer on the words of ${\mathrm{\Sigma }}^{\ast }$ in a fixed length-lexicographic order, outputting each newly accepted word once. This gives an effective enumeration of $A$ by finite stages $F_0\subseteq F_1\subseteq \cdots$ with ${\bigcup }_s{F}_s=A$.

Suppose for contradiction that no finite subset of $A$ belongs to $\mathcal{P}$. For each binary word $x$, effectively construct a recognizer $N_x$ that, on its own input $y$, simulates the stage enumeration from step 1.2 and the recognizer for $A_{TM}$ on $x$ in lockstep. It accepts if $y$ appears in the stage enumeration before the latter recognizer accepts, and otherwise continues forever. The coding in [L3] makes $x\mapsto <mi\; mathvariant="normal">⌜</mi>N_x<mi\; mathvariant="normal">⌝</mi>$ total and computable. If $x\mathrm{\notin }{A}_{TM}$ then $L(N_x)=A\in \mathcal{P}$; if $x\in A_{TM}$ then $L(N_x)=F_s\mathrm{\notin }\mathcal{P}$ for the finite stage $s$ at which that simulation stops admitting new words.

A recognizer for $I_{\mathcal{P}}$ could therefore recognize $\overline{A_{TM}}$: on input $x$, compute $<mi\; mathvariant="normal">⌜</mi>N_x<mi\; mathvariant="normal">⌝</mi>$ and run the index-set recognizer on it. This contradicts step 1.1. Hence there is a finite set $F\subseteq A$ with $F\in \mathcal{P}$.

Let $B$ be recognizable with $F\subseteq B$, and suppose for contradiction that $B\mathrm{\notin }\mathcal{P}$. For each binary word $x$, effectively build a recognizer $K_x$ that accepts every word of $F$ and, if the recognizer for $A_{TM}$ accepts $x$, also simulates a fixed recognizer for $B$. Then $x\mathrm{\notin }{A}_{TM}$ gives $L(K_x)=F\in \mathcal{P}$, while $x\in A_{TM}$ gives $L(K_x)=F\cup B=B\mathrm{\notin }\mathcal{P}$. As in step 3.1, the total computable map $x\mapsto <mi\; mathvariant="normal">⌜</mi>K_x<mi\; mathvariant="normal">⌝</mi>$ and the recognizer for $I_{\mathcal{P}}$ would recognize $\overline{A_{TM}}$, contradicting step 1.1. Therefore every such $B$ belongs to $\mathcal{P}$, and $F$ is the required finite positive witness.