Explicit set of types and terms in MLTT
How do you actually construct the sets of types and terms (more) formally 
  in set theory, and convince me that these actually do form a set?


It's essentially the same argument that BNF grammars define sets.


Start with the set of untyped terms (conventionally dubbed the preterms), and the set of untyped contexts (sequences $x_1:A_1, \ldots, x_n:A_n$ where the $x_i$ are variables and $A_i$ are preterms).
Think of each judgement form as a predicate. Think of $\Gamma \vdash e : A$ as a three-argument predicate on precontexts, preterms, and preterms, $\Gamma \vdash A \mbox{ type}$ as a two-argument predicate on preterms, $\Gamma \vdash e \equiv e' : A$ as a four-place predicate and so on. 
Interpret each rule of MLTT as a predicate transformer. 
So a rule like 
$$
  \frac{\displaystyle \Gamma \vdash e : \Sigma x:A.B}
       {\displaystyle \Gamma \vdash \pi_1 e : A}
  $$
is defining a new predicate $\vdash'(\_, \_, \_)$ from the old predicate $\vdash(\_, \_, \_)$ such that $\vdash'(\Gamma, \pi_1 e, A)$ holds when  $\vdash(\Gamma, e, \Sigma x:A.B)$ holds. 
Observe that every rule is a Horn clause without negation. 
As a result, the predicate transformer induced by the interpretation of a rule is monotone on the inclusion order on the lattice of sets of terms (or tuples of contexts and terms; or tuples of contexts, terms and terms; and so on). 
Furthermore, the pointwise union of monotone predicate transformers is also monotone. So we can interpret all of the rules as jointly defining a monotone predicate transformer.
By the Knaster-Tarski theorem, there is a least fixed point to the this lattice.
That fixed point gives you the set of well-typed terms, contexts, etc.