As Chris Eagle said, the incompleteness theorems actually imply that ZF does not have a complete consistent extension that is recursively axiomatizable, not just that ZF is incomplete. A much more general version is that any formal system that can prove the outputs of halting program executions and has a proof verifier program cannot be both consistent and complete in its theorems about the outputs of halting program executions. This immediately implies that any recursively enumerable FOL theory that interprets (i.e. can perform the same reasoning as) TC or PA− (mentioned in the linked post) is either inconsistent or incomplete.
You also said that "the incompleteness theorem requires some sort of nontrivial Gödel encoding". That is actually incorrect, and is one of the misconceptions that I address in the linked post. Gödel coding is only needed in the case of theories extending PA− for the sole purpose of demonstrating that PA− can prove basic facts about strings (represented as finite sequences of natural numbers that are in turn encoded as natural numbers). You can observe that the incompleteness theorems for TC needs no such coding business! For similar reasons, Gödel coding is unnecessary to prove the incompleteness theorems for stronger theories that have basic ability to reason about functions on naturals, such as any FOL theory that interprets ACA (a weak theory that is essentially PA plus the ability to construct any set of naturals satisfying some arithmetical property, plus full induction).
This is because any finite string can be naturally encoded as the set $S$ such that $⟨k,x⟩∈S$ iff the k-th number (0-indexed) in the string is $x$, using the easy pair-coding methods. With this, finite strings are definable over ACA as sets encoding functions from $[0..l{−}1]→\mathbb{N}$ for some $l∈\mathbb{N}$, and the length of a string $S$, which shall be denoted as $len(S)$, is then definable as the minimum $l∈\mathbb{N}$ such that $⟨l,x⟩∉S$ for every natural $x$. Concatenation of strings $S,T$ can then be easily defined as $S ∪ \{ ⟨len(S)+k,x⟩ : ⟨k,x⟩∈T \}$, and all basic string manipulation is equally easy.
In particular, ZFC clearly interprets ACA, so you can very well prove the incompleteness theorem for every recursively axiomatizable extension of ZFC without using Gödel coding.
Hence the real reason Gödel needed coding via the β-lemma was that he proved the theorem for a weak theory of arithmetic, which did not have any set-theoretic ability, and so he had to code finite sequences of naturals as a natural itself. In general, the weaker a formal system, the harder it is to prove the incompleteness theorem for it. And Gödel chose a weak system to tackle.