No, this proof is not correct. You can't iterate through all inputs $x\in \Sigma^*$ since it would take you "infinite time".

The correct way to do this is to construct the complement of $D$, which we will call $D^c$, then construct the intersection DFA $D^c\cap M$, and test if its language is empty. If it is, you can be sure that $L(M)\subseteq L(D)$, hence all words in $M$ have more $1$'s than $0$'s

No, this proof is not correct. You can't iterate through all inputs $x\in \Sigma^*$ since it would take you "infinite time".

The correct way to do this is to construct the complement of $D$ (as a pushdown automaton! as @Steven mentioned), which we will call $D^c$, then construct the intersection PDA $D^c\cap M$ (notice that this can be done since $M$ is a DFA), and test if its language is empty. If it is, you can be sure that $L(M)\subseteq L(D)$, hence all words in $M$ have more $1$'s than $0$'s