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 (\exists x \neg φ \land \exists x (ψ \land \neg χ))$
	vk15.4j.2	$⊢ \forall x χ \to \neg \exists x (θ \land τ)$
	vk15.4j.3	$⊢ \neg \forall x (τ \to φ)$
Assertion	vk15.4j	$⊢ \neg \exists x \neg θ \to \neg \forall x ψ$

Proof

Step	Hyp	Ref	Expression
1		vk15.4j.1	$⊢ \neg (\exists x \neg φ \land \exists x (ψ \land \neg χ))$
2		vk15.4j.2	$⊢ \forall x χ \to \neg \exists x (θ \land τ)$
3		vk15.4j.3	$⊢ \neg \forall x (τ \to φ)$
4		exanali	$⊢ \exists x (τ \land \neg φ) \leftrightarrow \neg \forall x (τ \to φ)$
5	3 4	mpbir	$⊢ \exists x (τ \land \neg φ)$
6		alex	$⊢ \forall x θ \leftrightarrow \neg \exists x \neg θ$
7	6	biimpri	$⊢ \neg \exists x \neg θ \to \forall x θ$
8	7	19.21bi	$⊢ \neg \exists x \neg θ \to θ$
9		simpl	$⊢ (τ \land \neg φ) \to τ$
10	9	a1i	$⊢ \neg \exists x \neg θ \to ((τ \land \neg φ) \to τ)$
11		19.8a	$⊢ (θ \land τ) \to \exists x (θ \land τ)$
12	8 10 11	syl6an	$⊢ \neg \exists x \neg θ \to ((τ \land \neg φ) \to \exists x (θ \land τ))$
13		notnot	$⊢ \exists x (θ \land τ) \to \neg \neg \exists x (θ \land τ)$
14	12 13	syl6	$⊢ \neg \exists x \neg θ \to ((τ \land \neg φ) \to \neg \neg \exists x (θ \land τ))$
15		con3	$⊢ (\forall x χ \to \neg \exists x (θ \land τ)) \to (\neg \neg \exists x (θ \land τ) \to \neg \forall x χ)$
16	2 14 15	mpsylsyld	$⊢ \neg \exists x \neg θ \to ((τ \land \neg φ) \to \neg \forall x χ)$
17		hbe1	$⊢ \exists x \neg θ \to \forall x \exists x \neg θ$
18	17	hbn	$⊢ \neg \exists x \neg θ \to \forall x \neg \exists x \neg θ$
19		hbn1	$⊢ \neg \forall x χ \to \forall x \neg \forall x χ$
20	5 16 18 19	eexinst01	$⊢ \neg \exists x \neg θ \to \neg \forall x χ$
21		exnal	$⊢ \exists x \neg χ \leftrightarrow \neg \forall x χ$
22	20 21	sylibr	$⊢ \neg \exists x \neg θ \to \exists x \neg χ$
23		pm3.13	$⊢ \neg (\exists x \neg φ \land \exists x (ψ \land \neg χ)) \to (\neg \exists x \neg φ \lor \neg \exists x (ψ \land \neg χ))$
24	1 23	ax-mp	$⊢ (\neg \exists x \neg φ \lor \neg \exists x (ψ \land \neg χ))$
25		simpr	$⊢ (τ \land \neg φ) \to \neg φ$
26	25	a1i	$⊢ \neg \exists x \neg θ \to ((τ \land \neg φ) \to \neg φ)$
27		19.8a	$⊢ \neg φ \to \exists x \neg φ$
28	26 27	syl6	$⊢ \neg \exists x \neg θ \to ((τ \land \neg φ) \to \exists x \neg φ)$
29		hbe1	$⊢ \exists x \neg φ \to \forall x \exists x \neg φ$
30	5 28 18 29	eexinst01	$⊢ \neg \exists x \neg θ \to \exists x \neg φ$
31		notnot	$⊢ \exists x \neg φ \to \neg \neg \exists x \neg φ$
32	30 31	syl	$⊢ \neg \exists x \neg θ \to \neg \neg \exists x \neg φ$
33		pm2.53	$⊢ (\neg \exists x \neg φ \lor \neg \exists x (ψ \land \neg χ)) \to (\neg \neg \exists x \neg φ \to \neg \exists x (ψ \land \neg χ))$
34	24 32 33	mpsyl	$⊢ \neg \exists x \neg θ \to \neg \exists x (ψ \land \neg χ)$
35		exanali	$⊢ \exists x (ψ \land \neg χ) \leftrightarrow \neg \forall x (ψ \to χ)$
36	35	con5i	$⊢ \neg \exists x (ψ \land \neg χ) \to \forall x (ψ \to χ)$
37	34 36	syl	$⊢ \neg \exists x \neg θ \to \forall x (ψ \to χ)$
38	37	19.21bi	$⊢ \neg \exists x \neg θ \to (ψ \to χ)$
39	38	con3d	$⊢ \neg \exists x \neg θ \to (\neg χ \to \neg ψ)$
40		19.8a	$⊢ \neg ψ \to \exists x \neg ψ$
41	39 40	syl6	$⊢ \neg \exists x \neg θ \to (\neg χ \to \exists x \neg ψ)$
42		hbe1	$⊢ \exists x \neg ψ \to \forall x \exists x \neg ψ$
43	22 41 18 42	eexinst11	$⊢ \neg \exists x \neg θ \to \exists x \neg ψ$
44		exnal	$⊢ \exists x \neg ψ \leftrightarrow \neg \forall x ψ$
45	43 44	sylib	$⊢ \neg \exists x \neg θ \to \neg \forall x ψ$

Metamath Proof Explorer

Theorem vk15.4j

Proof