As mentioned in Prof. Weaver's answer, the graph minor theorem (also known as the Robertson-Seymour theorem) uses large countable ordinals. The graph minor theorem is quite relevant to non-set-theoretic "mainstream" mathematical topics, in particular it can be characterized either as "every infinite set of finite graphs contains $A,B$ such that $A$ is a graph minor of $B$", or for added relevance to forbidden minor problems, "every minor-closed class of finite graphs can be characterized by a finite set of forbidden minors". [2]
Robertson and Seymour's 2004 proof is arguably even more involved with large countable ordinals than theorems such as Cantor-Bendixson as it uses specific large countable ordinals explicitly. In particular an ordinal $\psi_0(\Omega_\omega)$ appears, this ordinal is named using one of Wilfried Buchholz's representation systems for large countable ordinals. (Buchholz's naming system originates from his 1984 paper, "A new system of proof-theoretic ordinal functions" [1], and it is a simplification of an earlier system by Feferman.)
In proving that the graph minor relation is a well-quasi-order, Harvey Friedman's gap-embedding relation on labeled finite trees is introduced, and this relation is intended to mimic Buchholz's comparison criteria for comparing two terms in his ordinal representation system. Historically, any proof of a forbidden minor criterion not using orfinals (e.g. Wagner's theorem) is a special case of Robertson-Seymour [2], however the current published proof of full Robertson-Seymour is 500 pages, involving Buchholz's system for large countable ordinals via gap-embeddibility. [3]
[1]: W. Buchholz, "A new system of proof-theoretic ordinal functions" (1984)
[2]: Kolya, "The Graph Minor Theorem" (2015)
[3]: M. Rathjen, "The Realm of Ordinal Analysis" (2007)