Comment by jesuslop

In Gödel's collected works vol. 2 one has the detailed argument by transfinite induction up to the first inaccesible ordinal. Interesting to have this as guidemap.