Theorem vk15.4j

Description: Excercise 4j of Unit 15 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. This proof is the minimized Hilbert-style axiomatic version of the Fitch-style Natural Deduction proof found on page 442 of Klenk and was automatically derived from that proof. vk15.4j is vk15.4jVD automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		vk15.4j.1	$$⊢\neg \left(\exists x\neg \phi \wedge \exists x\left(\psi \wedge \neg \chi \right)\right)$$
2		vk15.4j.2	$$⊢\forall x\chi \to \neg \exists x\left(\theta \wedge \tau \right)$$
3		vk15.4j.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	3 4	mpbir	$$⊢\exists x\left(\tau \wedge \neg \phi \right)$$
6		alex	$$⊢\forall x\theta \leftrightarrow \neg \exists x\neg \theta$$
7	6	biimpri	$$⊢\neg \exists x\neg \theta \to \forall x\theta$$
8	7	19.21bi	$$⊢\neg \exists x\neg \theta \to \theta$$
9		simpl	$$⊢\left(\tau \wedge \neg \phi \right)\to \tau$$
10	9	a1i	$$⊢\neg \exists x\neg \theta \to \left(\left(\tau \wedge \neg \phi \right)\to \tau \right)$$
11		19.8a	$$⊢\left(\theta \wedge \tau \right)\to \exists x\left(\theta \wedge \tau \right)$$
12	8 10 11	syl6an	$$⊢\neg \exists x\neg \theta \to \left(\left(\tau \wedge \neg \phi \right)\to \exists x\left(\theta \wedge \tau \right)\right)$$
13		notnot	$$⊢\exists x\left(\theta \wedge \tau \right)\to \neg \neg \exists x\left(\theta \wedge \tau \right)$$
14	12 13	syl6	$$⊢\neg \exists x\neg \theta \to \left(\left(\tau \wedge \neg \phi \right)\to \neg \neg \exists x\left(\theta \wedge \tau \right)\right)$$
15		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)$$
16	2 14 15	mpsylsyld	$$⊢\neg \exists x\neg \theta \to \left(\left(\tau \wedge \neg \phi \right)\to \neg \forall x\chi \right)$$
17		hbe1	$$⊢\exists x\neg \theta \to \forall x\exists x\neg \theta$$
18	17	hbn	$$⊢\neg \exists x\neg \theta \to \forall x\neg \exists x\neg \theta$$
19		hbn1	$$⊢\neg \forall x\chi \to \forall x\neg \forall x\chi$$
20	5 16 18 19	eexinst01	$$⊢\neg \exists x\neg \theta \to \neg \forall x\chi$$
21		exnal	$$⊢\exists x\neg \chi \leftrightarrow \neg \forall x\chi$$
22	20 21	sylibr	$$⊢\neg \exists x\neg \theta \to \exists x\neg \chi$$
23		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)$$
24	1 23	ax-mp	$$⊢\left(\neg \exists x\neg \phi \vee \neg \exists x\left(\psi \wedge \neg \chi \right)\right)$$
25		simpr	$$⊢\left(\tau \wedge \neg \phi \right)\to \neg \phi$$
26	25	a1i	$$⊢\neg \exists x\neg \theta \to \left(\left(\tau \wedge \neg \phi \right)\to \neg \phi \right)$$
27		19.8a	$$⊢\neg \phi \to \exists x\neg \phi$$
28	26 27	syl6	$$⊢\neg \exists x\neg \theta \to \left(\left(\tau \wedge \neg \phi \right)\to \exists x\neg \phi \right)$$
29		hbe1	$$⊢\exists x\neg \phi \to \forall x\exists x\neg \phi$$
30	5 28 18 29	eexinst01	$$⊢\neg \exists x\neg \theta \to \exists x\neg \phi$$
31		notnot	$$⊢\exists x\neg \phi \to \neg \neg \exists x\neg \phi$$
32	30 31	syl	$$⊢\neg \exists x\neg \theta \to \neg \neg \exists x\neg \phi$$
33		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)$$
34	24 32 33	mpsyl	$$⊢\neg \exists x\neg \theta \to \neg \exists x\left(\psi \wedge \neg \chi \right)$$
35		exanali	$$⊢\exists x\left(\psi \wedge \neg \chi \right)\leftrightarrow \neg \forall x\left(\psi \to \chi \right)$$
36	35	con5i	$$⊢\neg \exists x\left(\psi \wedge \neg \chi \right)\to \forall x\left(\psi \to \chi \right)$$
37	34 36	syl	$$⊢\neg \exists x\neg \theta \to \forall x\left(\psi \to \chi \right)$$
38	37	19.21bi	$$⊢\neg \exists x\neg \theta \to \left(\psi \to \chi \right)$$
39	38	con3d	$$⊢\neg \exists x\neg \theta \to \left(\neg \chi \to \neg \psi \right)$$
40		19.8a	$$⊢\neg \psi \to \exists x\neg \psi$$
41	39 40	syl6	$$⊢\neg \exists x\neg \theta \to \left(\neg \chi \to \exists x\neg \psi \right)$$
42		hbe1	$$⊢\exists x\neg \psi \to \forall x\exists x\neg \psi$$
43	22 41 18 42	eexinst11	$$⊢\neg \exists x\neg \theta \to \exists x\neg \psi$$
44		exnal	$$⊢\exists x\neg \psi \leftrightarrow \neg \forall x\psi$$
45	43 44	sylib	$$⊢\neg \exists x\neg \theta \to \neg \forall x\psi$$