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 (1) and (3), and a sketch of a proof of (2) can be found in Diestel's Graph Theory textbook. See here to peruse the book online.