(This is a subproblem that came up as I was proving that $\{e: \phi_e(x) \text{ has infinite domain}\}$ is $\Pi_2$-complete.)
Let $A$ be a set of natural numbers and suppose $$n\in A\iff \forall y_1\exists y_2 T(n,y_1,y_2)$$
(where $T$ is a (computable) relation).
Consider this partial function on pairs of natural numbers:
$$(n,x) \mapsto 1\text{ if }\forall y_1\leq x\exists y_2 T(n,y_1,y_2)\\(n,x)\text{ is undefined otherwise} $$
If $n\in A$, then the above function as a function of $x$ is total. Is it true that if $n\notin A$, then this function (again as a function of $x$) has finite domain? I think so, and I think this is a trivial result but I can't wrap my head around proving it in a formal way.
Here's what I think informally: if $n\notin A$, then the first condition in the definition may be true for small $x$, but starting from some $x_0$, that wouldn't be true. Is this indeed the case? I can't connect this with the negation of $x\in A$ i.e. with $\exists y_1\forall y_2 \neg T(n,y_2,y_3) $.
Edit: I modified the original function. Does the new function has a finite domain as a function of $x$ when $x\notin A$? If not, I was wondering if there's a way to modify this function further so that (1) it remains computable, (2) if $n\in A$, the domain is still infinite, (3) if $n\notin A$, the domain is finite?
Let $V$ denote the partial function from the question. Suppose $n\notin A$. Then $\exists x_0 \forall y_2 \neg T(n, x_0, y_2)$. Then the domain of $V(n,-)$ is a subset of $\{x\in N: x < x_0 \}$ (hence finite). Here's why nothing outside this finite set can lie in the domain. If $x \ge x_0$, then the condition $$\forall y_1 < x \exists y_2 T(n,y_1,y_2)$$
or equivalently $$\forall y_1\exists y_2 (\neg (y_1 \le x) \lor T(n,y_1,y_2))$$ is violated. Indeed, its negation is $$\exists y_1\forall y_2 ((y_1 \le x)\land \neg T(n,y_1,y_2))$$ and this negation is true (take $y_1=x_0$).