A nontrivial extensional property admits a uniform witness machine construction

If $\mathrm{\varnothing }\mathrm{\notin }\mathcal{P}$, choose a recognizable language $W\in \mathcal{P}$. If instead $\mathrm{\varnothing }\in \mathcal{P}$, choose a recognizable language $W\mathrm{\notin }\mathcal{P}$. In either case, this choice fixes a recognizable language $W$ that lies on the opposite side of $\mathcal{P}$ from $\mathrm{\varnothing }$.

Fix a recognizer $R_W$ for $W$. For each coded pair $x=⟨<mi\; mathvariant="normal">⌜</mi>M<mi\; mathvariant="normal">⌝</mi>,\widehat{w}⟩$, build a machine $N_x$ that on input $y$ simulates $M$ on $w$; if that simulation ever accepts, $N_x$ starts a simulation of $R_W$ on $y$, and if the simulation of $M$ never accepts then $N_x$ never accepts $y$. Because the code of $R_W$ is fixed and $x$ is inserted as data, the map $x\mapsto <mi\; mathvariant="normal">⌜</mi>N_x<mi\; mathvariant="normal">⌝</mi>$ is total and computable.

If $x\in A_{TM}$, then [L2] says that $M$ accepts $w$, so step 2.1 eventually releases the simulation of $R_W$ on every input $y$; hence $L(N_x)=W$. If $x\mathrm{\notin }{A}_{TM}$, the simulation of $M$ on $w$ never accepts, so $N_x$ accepts no input and $L(N_x)=\mathrm{\varnothing }$. This is exactly the required witness-machine construction.