The following excerpt is from Frank Drake's 'Large Cardinals' book, in the chapter on Constructibility. He gives a (non-ZFC) proof of the following theorem:
Theroem: There are $\kappa^+$models of ZF of the form $L_\alpha$ for $\alpha$ between $\kappa$ and $\kappa^+$
which he uses to proves results about the famous 'gaps' in the Constructible hierarchy. I will give the proof below. The remarkable thing about this proof is that the actuall non-ZFC part of it is very much 'intuitively true', and therefore the proof seems to be a strong heuristic for believing in the consistency of ZFC. Here is the proof:
Proof: Using the definable well ordering $<_L$ of $L$, define a Skolem function in $L$ for each formula $\phi(x_0,...,x_n)$ by letting $f_\phi(x_0,...,x_n)$ be the $<_L$-least element satisfying $\phi$, or $\emptyset$ otherwise. For each$\phi$, $f_\phi$ is a definable Skolem function in $L$.
The collection F of all such Skolem functions is not definable in ZFC as if it were, it would imply a truth definition for $L$ (and hence $V$, if $V=L$), and also models of ZFC. But we will make the (non-ZFC) assumption that the countable collection F exists.
Take any $L_\beta$ for $\kappa\le\beta\le\kappa^+$. Form the closure $X$ of $L_\beta$ under F; we shall have $|X|=\kappa$ and also $(X,E(X))\prec L$. Hence $(X,E(X))$ is well-founded and a model of extensionality, do Mostowski's theorem implies that we have a unique collapsing isomorphism $f:X\to Y$ for some transitive $Y$.Since $X\models ZFL$, also $Y\models ZFL$; and so by 1.12 (a previous theorem where he proves that any set-model of ZFL is of the form $L_\alpha$ for some $\alpha$) $Y=L_\alpha$ for some $\alpha$. (There rest of the proof simply shows that there are $\kappa^+$ such models, and is not directly related to my question).
Question: Am I missing something here? It seems like the very intuitive assumption that the non-definable collection F exists gives us a clear reason to believe in the consistency of ZFC. Yet I have read many expository articles on ZFC and have never seen this argument used before. I feel like there must be some circular argument in here somewhere.