in Jech's paper: On Gödel's Second Incompleteness Theorem
Theorem if ZF proves there is a model of ZF, then ZF proves 0=1.
In the beginning of the proof he passes to a “big enough” finite subset S of ZF (that proves there is a model of ZF and defines formulas and their satisfaction etc.)
The proof goes by looking at a model M of S and models of S within M, which can be lifted to be a model in the ‘outside world’, and using some diagonal sentence G for a contradiction.
Why does passing to a finite subset needed for the proof?
Another question: If once actually builds a model of set theory, the above theorem proves that ZF is inconsistent. But would that mean one could explicitly write down a list of inferences that will derive a contradiction? Could we be sure such a list exists?