I'll just remark that the fact that every surface has a finite number of excluded minors (and also topological minors) does not require the full strength of the Graph Minors Theorem. Indeed, the proof relies on the following three facts:
The Grid Theorem. There exists a function $f: \mathbb{N} \to \mathbb{N}$, such that every graph with tree-width at least $f(n)$, contains the $n \times n$ grid as a minor.
Graphs of bounded tree-width are well-quasi-ordered. For any $k$, the class of graphs of tree-width at most $k$ is well-quasi-ordered.
Forbidden minors for surfaces do not contain arbitrarily large grid minors. There is a function $h: \mathbb{N} \to \mathbb{N}$, such that every minor-minimal graph not embeddable on a surface of genus $g$ does not contain an $h(g) \times h(g)$ grid as a minor.
All three of these facts now have very compact proofs. In fact, proofs for all three are included in the third and fourth editions of Diestel's Graph Theory. See here to peruse the book online.