# Is the set of minimal DFA decidable?

Let $\mathrm{MIN}_{\mathrm{DFA}}$ collection of all the codings of DFAs such that they are minimal regarding their states number. I mean if $\langle A \rangle \in \mathrm{MIN}_{\mathrm{DFA}}$ then for every other DFA $B$ with less states than $A$, $L(A)\ne L(B)$ holds. I'm trying to figure out how come that $\mathrm{MIN}_{\mathrm{DFA}} \in R$? How come it is decidable?

Given two DFAs $A,B$, it is decidable (even efficient!) whether $L(A) = L(B)$: use the product construction to get a DFA for $L(A) \triangle L(B)$, and now use reachability analysis.
In order to determine whether $A$ is a minimal DFA, one can just try all DFAs $B$ with less states, looking for one satisfying $L(A) = L(B)$. Alternatively, there are algorithms for minimizing DFAs which are vastly more efficient than that approach. They are even more efficient if all you want to know is whether the DFA is minimal or not.