Determine if $\forall xQx \rightarrow \exists yQy$ is valid I am learning how to draft proof of mathematical logic. Here is my work so far, but I don't feel comfortable, as it is unclean;
'=' is present in this language, and $Q$ is a 1-place predicate symbol:
Let $\mathfrak{U}$ be any structure, and $s:V \rightarrow |\mathfrak{U}|$ be any assignment function. We want to show that $\vDash_{\mathfrak{U}} \forall xQx \rightarrow \exists yQy[s]$, by the definition
$$\vDash_{\mathfrak{U}} \forall xQx \rightarrow \exists yQy[s]$$
$$\Leftrightarrow$$
$$\vDash_{\mathfrak{U}} \forall xQx [s] \longrightarrow \vDash_{\mathfrak{U}} \exists yQy[s]$$
$$\Leftrightarrow$$
$$\forall d_x \in |\mathfrak{U}|, <d_x>\in Q^\mathfrak{U} \longrightarrow \exists d_y , <d_y> \in Q^{\mathfrak{U}}, \text{by the definition of }s(x|d)$$
Suppose for the contradiction that $\nvDash_{\mathfrak{U}} \forall xQx \rightarrow \exists yQy[s]$, then it will only be the case that $\vDash_{\mathfrak{U}} \forall xQx[s]$, but $\nvDash_{\mathfrak{U}} \exists yQy[s]$.
Which is a contradiction already, as $\forall d_x \in |\mathfrak{U}|, <d_x>\in Q^\mathfrak{U}$, it cannot be that $\nexists d_y , <d_y> \in Q^{\mathfrak{U}}$
I feel so sick about my proof. It is awful. And that is the reason I post this, I want to learn the formality of proof.
 A: Besides the comments, let us look into the case a bit further.
In the standard unsorted logical setting, the given sentence is equivalent to
$$\forall xPx\rightarrow\exists xPx$$
which provides a more perspicuous form for the underlying idea. Calvin Jongsma gives a clear explanation of its evaluation in his Introduction to Discrete Mathematics via Logic and Proof (p. 116-17; the boldface is mine, the italics are in the original):

$\forall xPx\rightarrow\exists xPx$ is logically true. To show this,
we must argue that $∃xPx$ is true whenever $∀xPx$ is. If $∀xPx$ is
true, then all members of universe $U$ have property $P$, however $P$
is interpreted. Certainly, then, some member of $U$ has property $P$,
i.e., $∃xPx$ is true. (This depends upon the fact, unstressed until
now, that only non-empty sets are accepted—by convention—as
bona fide universes of discourse.)

What is the basis of this convention? We may reason in two ways in case that a domain of discourse is empty (beware of the distinction between an empty domain and an empty extension of a predicate $P$):

*

*$\forall xPx$ is false $\implies\neg\forall xPx$ is true $\implies\exists x\neg Px$ is true

Since the domain is empty of objects one of which could be assigned to $x$, this is an incoherent interpretation, given the standard definition of $\exists$.

*

*$\forall xPx$ is true $\implies\neg\exists x\neg Px$ is true

Since a non-existence claim is made, this is a coherent interpretation.
Therefore, we can agree on evaluating $\forall xPx$ to true in case of an empty domain of discourse. Notice that this strips $\forall xPx\rightarrow\exists xPx$ off validity.
Though, an empty domain of discourse (i.e., kind of nothingness) is not an absurd idea and worth consideration philosophically, it is hardly a meaningful possibility for many branches of knowledge, including mathematics. So, it is convenient to regard empty domain of discourse as a logical singularity and disregard it standardly.
It should be remarked that there are various logical systems that aim at dealing with the issue of non-existence among other metalogical complications. But they are beyond the scope of the present question.
