Finite subsets of a set A in the definable power set of A I'm working through Kunen's famous book on set theory and I'm puzzled by exercise 19 of chapter VI.
Background for the exercise:
In chapter V (Definition 1.1) the author defines certain function of two variables $Df(A,n)$. This is the set of $n$-place relations on $A$ which are definable by a formula with $n$ free variables relativized to $A$. Defining $Df(A,n)$, first he defines recursively sets $Df'(k,A,n),k \in \omega$ and then sets $Df(A,n) = \bigcup_{k \in \omega} Df'(k,A,n)$.
Then he proves Lemma V 1.3 which says that if $\phi(x_0,...,x_{n-1})$ is any formula and $A$ is any set then the set $\{ s \in A^n : \phi^A(s(0),...,s(n-1)) \}$ is in $Df(A,n)$ ($\phi^A$ means $\phi$ relativized to $A$). 
In the next chapter VI (Definition 1.1) the author defines the definable power set of a set $A$, or $\mathcal{D}(A)$. This is the set of subsets of A which are definable from a finite number of elements of $A$ by a formula relativized to $A$. Then in Lemma VI 1.3(c) he proves that the finite subsets of $A$ are in $\mathcal{D}(A)$.
Exercise VI 19:
The exercise asks to define alternatives to $Df$ and $\mathcal{D}$, namely such $Df^*$ and $\mathcal{D}^*$ that $Df^*$ still
satisfies Lemma V 1.3 but Lemma VI 1.3(c) is not provable in ZFC. He also gives a hint:
First define $\alpha = \omega$ if CON(ZF) and alpha = the least Gödel number of a contradiction if not-CON(ZF) (does he mean the least Gödel number of a proof of a contradiction?). Then define $Df^*(A,n) = \bigcup_{k < \alpha} Df'(k,A,n)$.
I think I might understand the idea. We suppose that Lemma VI 1.3(c) is provable. Then somehow we show that it is not possible that $\alpha \in \omega$ so that it must be that $\alpha = \omega$. But then we have proved CON(ZF) which is not possible by Gödel's 2nd.
My questions:
First I can't see how Lemma V 1.3 goes through with $Df^*$. For example the proof uses the fact that $Df(A,n)$ is closed under finite intersections. This is easy to see from the definition of $Df$ but what happens if not-CON(ZF) and alpha is a natural and only finitely many $Df'$ are taken into $Df^*$. Doesn't this destroy the finite intersection property?

In more details this is what I tried to do. The case 'conjunction' of the induction on the structure of the formula. We assume $\phi = \phi_1 \wedge \phi_2$ and
$ZFC \vdash \forall A [ \{ s \in A^n : \phi_1^A(s(0),\ldots,s(n-1)) \} \in Df^*(A,n) ]$
and
$ZFC \vdash \forall A [ \{ s \in A^n : \phi_2^A(s(0),\ldots,s(n-1)) \} \in Df^*(A,n) ]$.
Then we have to show that
$ZFC \vdash \forall A [ \{ s \in A^n : \phi_1^A(s(0),\ldots,s(n-1)) \wedge \phi_2^A(s(0),\ldots,s(n-1))\} \in Df^*(A,n) ]$
or what is the same
$ZFC \vdash \forall A [ \{ s \in A^n : \phi_1^A(s(0),\ldots,s(n-1)) \} \cap \{ s \in A^n : \phi_2^A(s(0),\ldots,s(n-1))\} \in Df^*(A,n) ]$.
To prove this: working inside the formal theory, let $A$ be a set, $A_1 = \{ s \in A^n : \phi_1^A(s(0),\ldots,s(n-1)) \}$ and $A_2 = \{ s \in A^n : \phi_2^A(s(0),\ldots,s(n-1)) \}$. Since $A_1, A_2 \in Df^*(A,n)$ there are $k_1,k_2 < \alpha$ such that $A_1 \in Df'(k_1,A,n)$ and $A_2 \in Df'(k_2,A,n)$. If we let $k = \max \{k_1,k_2\}$ then $A_1 \cap A_2 \in Df'(k+1,A,n)$ by definition of the sets $Df'$. Now in the case of $Df$ there are no problems deducting that $A_1 \cap A_2 \in Df(A,n)$, but in the case of $Df^*$ what can we do if it happens that $k+1 = \alpha$? I can't see how this kind of a situation can be prevented.

Also even if we somehow can prove Lemma V 1.3 with $Df^*$, why does it follow from provability of Lemma VI 1.3(c) (= finite subsets of $A$ are in $\mathcal{D}^*(A)$) that $\alpha \notin \omega$?
 A: The key point in reproving V.1.3 for Df* is that V.1.3 is not actually a single theorem of ZF, it's a scheme of theorems, one for each formula.  The result itself can't even be stated directly in ZF, as Kunen tersely notes in the middle of p. 154. 
The proof V.1.3 is by metainduction on the structure of the formula. As such, the proof only really makes use of the DF' hierarchy for standard natural numbers, not for arbitrary "natural numbers", because the length of any formula is a standard natural number. Now, assuming Con(ZF), if the number $\alpha$ from Exercise VI.19 is defined, it is not a standard natural number - this is exactly what Con(ZF) says when we assert it in the metatheory. So assuming Con(ZF) we can still prove V.1.3 in the metatheory, because even if $\alpha$ is defined it is larger than any standard natural, so we still have the whole DF' hierarchy for standard naturals.  
One very subtle point in Exercise VI.19 is the distinction between Con(ZF), which is assumed in the metatheory, and CON($\ulcorner$ZF$\urcorner$), which is the formalization of Con(ZF) that is used in the definition of Df*.
For proving the final part of Exercise VI.19, if my memory serves you can do it by looking at $A = \omega$ and analyzing the structure of the DF' hierarchy in this case. But I haven't looked at the definitions of Df' closely enough to verify this, so please take this last paragraph as just a suggestion. 
