Theorem vk15.4jVD

Description: The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 15 Excercise 4.f. found in the "Answers to Starred Exercises" on page 442 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted to be a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. vk15.4j is vk15.4jVD without virtual deductions and was automatically derived from vk15.4jVD . Step numbers greater than 25 are additional steps necessary for the sequent calculus proof not contained in the Fitch-style proof. Otherwise, step i of the User's Proof corresponds to step i of the Fitch-style proof.

	Ref	Expression
Hypotheses	vk15.4jVD.1	$$⊢\neg \left(\exists x\neg \phi \wedge \exists x\left(\psi \wedge \neg \chi \right)\right)$$
	vk15.4jVD.2	$$⊢\forall x\chi \to \neg \exists x\left(\theta \wedge \tau \right)$$
	vk15.4jVD.3	$$⊢\neg \forall x\left(\tau \to \phi \right)$$
Assertion	vk15.4jVD	$$⊢\neg \exists x\neg \theta \to \neg \forall x\psi$$

Proof

Step	Hyp	Ref	Expression
1		vk15.4jVD.1	$$⊢\neg \left(\exists x\neg \phi \wedge \exists x\left(\psi \wedge \neg \chi \right)\right)$$
2		vk15.4jVD.2	$$⊢\forall x\chi \to \neg \exists x\left(\theta \wedge \tau \right)$$
3		vk15.4jVD.3	$$⊢\neg \forall x\left(\tau \to \phi \right)$$
4		exanali	$$⊢\exists x\left(\tau \wedge \neg \phi \right)\leftrightarrow \neg \forall x\left(\tau \to \phi \right)$$
5	4	biimpri	$$⊢\neg \forall x\left(\tau \to \phi \right)\to \exists x\left(\tau \wedge \neg \phi \right)$$
6	3 5	e0a	$$⊢\exists x\left(\tau \wedge \neg \phi \right)$$
7		idn1	$$⊢\left(\neg \exists x\neg \theta \to \neg \exists x\neg \theta \right)$$
8		alex	$$⊢\forall x\theta \leftrightarrow \neg \exists x\neg \theta$$
9	8	biimpri	$$⊢\neg \exists x\neg \theta \to \forall x\theta$$
10	7 9	e1a	$$⊢\left(\neg \exists x\neg \theta \to \forall x\theta \right)$$
11		sp	$$⊢\forall x\theta \to \theta$$
12	10 11	e1a	$$⊢\left(\neg \exists x\neg \theta \to \theta \right)$$
13		idn2	$$⊢\left(\neg \exists x\neg \theta ,\left(\tau \wedge \neg \phi \right)\to \left(\tau \wedge \neg \phi \right)\right)$$
14		simpl	$$⊢\left(\tau \wedge \neg \phi \right)\to \tau$$
15	13 14	e2	$$⊢\left(\neg \exists x\neg \theta ,\left(\tau \wedge \neg \phi \right)\to \tau \right)$$
16		pm3.2	$$⊢\theta \to \left(\tau \to \left(\theta \wedge \tau \right)\right)$$
17	12 15 16	e12	$$⊢\left(\neg \exists x\neg \theta ,\left(\tau \wedge \neg \phi \right)\to \left(\theta \wedge \tau \right)\right)$$
18		19.8a	$$⊢\left(\theta \wedge \tau \right)\to \exists x\left(\theta \wedge \tau \right)$$
19	17 18	e2	$$⊢\left(\neg \exists x\neg \theta ,\left(\tau \wedge \neg \phi \right)\to \exists x\left(\theta \wedge \tau \right)\right)$$
20		notnot	$$⊢\exists x\left(\theta \wedge \tau \right)\to \neg \neg \exists x\left(\theta \wedge \tau \right)$$
21	19 20	e2	$$⊢\left(\neg \exists x\neg \theta ,\left(\tau \wedge \neg \phi \right)\to \neg \neg \exists x\left(\theta \wedge \tau \right)\right)$$
22		con3	$$⊢\left(\forall x\chi \to \neg \exists x\left(\theta \wedge \tau \right)\right)\to \left(\neg \neg \exists x\left(\theta \wedge \tau \right)\to \neg \forall x\chi \right)$$
23	2 21 22	e02	$$⊢\left(\neg \exists x\neg \theta ,\left(\tau \wedge \neg \phi \right)\to \neg \forall x\chi \right)$$
24		hbe1	$$⊢\exists x\neg \theta \to \forall x\exists x\neg \theta$$
25	24	hbn	$$⊢\neg \exists x\neg \theta \to \forall x\neg \exists x\neg \theta$$
26		hba1	$$⊢\forall x\chi \to \forall x\forall x\chi$$
27	26	hbn	$$⊢\neg \forall x\chi \to \forall x\neg \forall x\chi$$
28	6 23 25 27	exinst01	$$⊢\left(\neg \exists x\neg \theta \to \neg \forall x\chi \right)$$
29		exnal	$$⊢\exists x\neg \chi \leftrightarrow \neg \forall x\chi$$
30	29	biimpri	$$⊢\neg \forall x\chi \to \exists x\neg \chi$$
31	28 30	e1a	$$⊢\left(\neg \exists x\neg \theta \to \exists x\neg \chi \right)$$
32		idn2	$$⊢\left(\neg \exists x\neg \theta ,\neg \chi \to \neg \chi \right)$$
33		pm3.13	$$⊢\neg \left(\exists x\neg \phi \wedge \exists x\left(\psi \wedge \neg \chi \right)\right)\to \left(\neg \exists x\neg \phi \vee \neg \exists x\left(\psi \wedge \neg \chi \right)\right)$$
34	1 33	e0a	$$⊢\left(\neg \exists x\neg \phi \vee \neg \exists x\left(\psi \wedge \neg \chi \right)\right)$$
35		simpr	$$⊢\left(\tau \wedge \neg \phi \right)\to \neg \phi$$
36	13 35	e2	$$⊢\left(\neg \exists x\neg \theta ,\left(\tau \wedge \neg \phi \right)\to \neg \phi \right)$$
37		19.8a	$$⊢\neg \phi \to \exists x\neg \phi$$
38	36 37	e2	$$⊢\left(\neg \exists x\neg \theta ,\left(\tau \wedge \neg \phi \right)\to \exists x\neg \phi \right)$$
39		hbe1	$$⊢\exists x\neg \phi \to \forall x\exists x\neg \phi$$
40	6 38 25 39	exinst01	$$⊢\left(\neg \exists x\neg \theta \to \exists x\neg \phi \right)$$
41		notnot	$$⊢\exists x\neg \phi \to \neg \neg \exists x\neg \phi$$
42	40 41	e1a	$$⊢\left(\neg \exists x\neg \theta \to \neg \neg \exists x\neg \phi \right)$$
43		pm2.53	$$⊢\left(\neg \exists x\neg \phi \vee \neg \exists x\left(\psi \wedge \neg \chi \right)\right)\to \left(\neg \neg \exists x\neg \phi \to \neg \exists x\left(\psi \wedge \neg \chi \right)\right)$$
44	34 42 43	e01	$$⊢\left(\neg \exists x\neg \theta \to \neg \exists x\left(\psi \wedge \neg \chi \right)\right)$$
45		exanali	$$⊢\exists x\left(\psi \wedge \neg \chi \right)\leftrightarrow \neg \forall x\left(\psi \to \chi \right)$$
46	45	con5i	$$⊢\neg \exists x\left(\psi \wedge \neg \chi \right)\to \forall x\left(\psi \to \chi \right)$$
47	44 46	e1a	$$⊢\left(\neg \exists x\neg \theta \to \forall x\left(\psi \to \chi \right)\right)$$
48		sp	$$⊢\forall x\left(\psi \to \chi \right)\to \left(\psi \to \chi \right)$$
49	47 48	e1a	$$⊢\left(\neg \exists x\neg \theta \to \left(\psi \to \chi \right)\right)$$
50		con3	$$⊢\left(\psi \to \chi \right)\to \left(\neg \chi \to \neg \psi \right)$$
51	50	com12	$$⊢\neg \chi \to \left(\left(\psi \to \chi \right)\to \neg \psi \right)$$
52	32 49 51	e21	$$⊢\left(\neg \exists x\neg \theta ,\neg \chi \to \neg \psi \right)$$
53		19.8a	$$⊢\neg \psi \to \exists x\neg \psi$$
54	52 53	e2	$$⊢\left(\neg \exists x\neg \theta ,\neg \chi \to \exists x\neg \psi \right)$$
55		hbe1	$$⊢\exists x\neg \psi \to \forall x\exists x\neg \psi$$
56	31 54 25 55	exinst11	$$⊢\left(\neg \exists x\neg \theta \to \exists x\neg \psi \right)$$
57		exnal	$$⊢\exists x\neg \psi \leftrightarrow \neg \forall x\psi$$
58	57	biimpi	$$⊢\exists x\neg \psi \to \neg \forall x\psi$$
59	56 58	e1a	$$⊢\left(\neg \exists x\neg \theta \to \neg \forall x\psi \right)$$
60	59	in1	$$⊢\neg \exists x\neg \theta \to \neg \forall x\psi$$