How to prove this is a tautology $\forall x : (p(x) \wedge \neg q(x)) \vee \exists x: \neg p(x) \vee \neg \exists x: q(x)$
The problem is I know that this is a tautology, but I don't know how to prove it. Can anyone can help me?
 A: Try breaking it up in words.  The second two conditions are:
"there is an $x$ such that $p(x)$ is false"
"there is no $x$ such that $q(x)$ is true"
You need to show that if neither of these conditions holds (that is, both of these statements are false), then necessarily the first one ("for every $x$, $p(x)$ is true and $q(x)$ is false") must be true.  
Can you see how to prove that?
A: Edit
Here is a way without EI
(a lot quicker,too):
$\forall x : (p(x) \wedge \neg q(x)) \vee \exists x: \neg p(x) \vee \neg \exists x: q(x) \Rightarrow$
$\forall x : \neg(\neg p(x) \vee  q(x)) \vee \exists x: \neg p(x) \vee \neg \exists x: q(x)\Rightarrow$
$\exists x : (\neg p(x) \vee  q(x)) \vee \exists x: \neg p(x) \vee \neg \exists x: q(x)\Rightarrow$
$\exists x : \neg p(x) \vee  \exists x: q(x) \vee \exists x: \neg p(x) \vee \neg \exists x: q(x)\Rightarrow$
$\exists x : \neg p(x) \vee  (\exists x: q(x) \vee \neg \exists x: q(x))\vee \exists x: \neg p(x)\Rightarrow$
$\exists x : \neg p(x) \vee  T \vee \exists x: \neg p(x)\Rightarrow $
$\exists x : \neg p(x) \vee  T \Rightarrow  T$
A: The following proof uses a proof checker to make sure I am not violating any rules:

On line 1, I assume the negation of what I want to prove. 
Between lines 2 and 8, I use De Morgan rule (DeM), conjunction elimination (∧E) and change of quantifiers (CQ) to arrive at lines 5 and 8. I will attempt to use existential elimination and universal elimination to derive a contradiction using these lines.
To attempt to eliminate the existential statement on line 5, I assume that I can replace the variable $x$ with the name $a$. I will attempt to derive a contradiction (⊥). I am able to do that by using universal elimination from line 8 on line 12.  Because this is a universal elimination I can use any name and so I reuse the name $a$ which will help me derive the contradiction. Lines 11 and 12 are now contradictory and so I can derive the desired contradiction on line 13.  That allows me to discharge the assumption on line 9 and place the contradiction on line 14 justified by existential elimination (∃E).
The contradiction on line 14 is what I need to use indirect proof (IP) to derive the result I sought.
Links to the proof checker and the forallx text associated with it are below.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf
