 Case 2: Each φn is satisfiable. There are only finitely many possible models with universe {x0,…, xn+1}. Gödel orders them as a tree by defining a model M to be below a model M′ if M is a submodel of M′. In this way we obtain a tree which is finitely branching but infinite. By König’s Lemma there is an infinite branch B. (In the proof, Gödel explicitly constructs the branch given by König’s Lemma rather than citing it by name.) The union of the models on B forms a model M with universe {x0, x1,…}. Since M satisfies each φn, the original formula φ holds in M. So φ is satisfiable and we are done.