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	⊢ ¬ ( ∃ 𝑥 ¬ 𝜑 ∧ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) )
	vk15.4j.2	⊢ ( ∀ 𝑥 𝜒 → ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
	vk15.4j.3	⊢ ¬ ∀ 𝑥 ( 𝜏 → 𝜑 )
Assertion	vk15.4j	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ∀ 𝑥 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		vk15.4j.1	⊢ ¬ ( ∃ 𝑥 ¬ 𝜑 ∧ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) )
2		vk15.4j.2	⊢ ( ∀ 𝑥 𝜒 → ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
3		vk15.4j.3	⊢ ¬ ∀ 𝑥 ( 𝜏 → 𝜑 )
4		exanali	⊢ ( ∃ 𝑥 ( 𝜏 ∧ ¬ 𝜑 ) ↔ ¬ ∀ 𝑥 ( 𝜏 → 𝜑 ) )
5	3 4	mpbir	⊢ ∃ 𝑥 ( 𝜏 ∧ ¬ 𝜑 )
6		alex	⊢ ( ∀ 𝑥 𝜃 ↔ ¬ ∃ 𝑥 ¬ 𝜃 )
7	6	biimpri	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 𝜃 )
8	7	19.21bi	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → 𝜃 )
9		simpl	⊢ ( ( 𝜏 ∧ ¬ 𝜑 ) → 𝜏 )
10	9	a1i	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → 𝜏 ) )
11		19.8a	⊢ ( ( 𝜃 ∧ 𝜏 ) → ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
12	8 10 11	syl6an	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) ) )
13		notnot	⊢ ( ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) → ¬ ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
14	12 13	syl6	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → ¬ ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) ) )
15		con3	⊢ ( ( ∀ 𝑥 𝜒 → ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) ) → ( ¬ ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) → ¬ ∀ 𝑥 𝜒 ) )
16	2 14 15	mpsylsyld	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → ¬ ∀ 𝑥 𝜒 ) )
17		hbe1	⊢ ( ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 ∃ 𝑥 ¬ 𝜃 )
18	17	hbn	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 ¬ ∃ 𝑥 ¬ 𝜃 )
19		hbn1	⊢ ( ¬ ∀ 𝑥 𝜒 → ∀ 𝑥 ¬ ∀ 𝑥 𝜒 )
20	5 16 18 19	eexinst01	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ∀ 𝑥 𝜒 )
21		exnal	⊢ ( ∃ 𝑥 ¬ 𝜒 ↔ ¬ ∀ 𝑥 𝜒 )
22	20 21	sylibr	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∃ 𝑥 ¬ 𝜒 )
23		pm3.13	⊢ ( ¬ ( ∃ 𝑥 ¬ 𝜑 ∧ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ ∃ 𝑥 ¬ 𝜑 ∨ ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) )
24	1 23	ax-mp	⊢ ( ¬ ∃ 𝑥 ¬ 𝜑 ∨ ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) )
25		simpr	⊢ ( ( 𝜏 ∧ ¬ 𝜑 ) → ¬ 𝜑 )
26	25	a1i	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → ¬ 𝜑 ) )
27		19.8a	⊢ ( ¬ 𝜑 → ∃ 𝑥 ¬ 𝜑 )
28	26 27	syl6	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → ∃ 𝑥 ¬ 𝜑 ) )
29		hbe1	⊢ ( ∃ 𝑥 ¬ 𝜑 → ∀ 𝑥 ∃ 𝑥 ¬ 𝜑 )
30	5 28 18 29	eexinst01	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∃ 𝑥 ¬ 𝜑 )
31		notnot	⊢ ( ∃ 𝑥 ¬ 𝜑 → ¬ ¬ ∃ 𝑥 ¬ 𝜑 )
32	30 31	syl	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ¬ ∃ 𝑥 ¬ 𝜑 )
33		pm2.53	⊢ ( ( ¬ ∃ 𝑥 ¬ 𝜑 ∨ ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ ¬ ∃ 𝑥 ¬ 𝜑 → ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) )
34	24 32 33	mpsyl	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) )
35		exanali	⊢ ( ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ↔ ¬ ∀ 𝑥 ( 𝜓 → 𝜒 ) )
36	35	con5i	⊢ ( ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) → ∀ 𝑥 ( 𝜓 → 𝜒 ) )
37	34 36	syl	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 ( 𝜓 → 𝜒 ) )
38	37	19.21bi	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( 𝜓 → 𝜒 ) )
39	38	con3d	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ¬ 𝜒 → ¬ 𝜓 ) )
40		19.8a	⊢ ( ¬ 𝜓 → ∃ 𝑥 ¬ 𝜓 )
41	39 40	syl6	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ¬ 𝜒 → ∃ 𝑥 ¬ 𝜓 ) )
42		hbe1	⊢ ( ∃ 𝑥 ¬ 𝜓 → ∀ 𝑥 ∃ 𝑥 ¬ 𝜓 )
43	22 41 18 42	eexinst11	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∃ 𝑥 ¬ 𝜓 )
44		exnal	⊢ ( ∃ 𝑥 ¬ 𝜓 ↔ ¬ ∀ 𝑥 𝜓 )
45	43 44	sylib	⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ∀ 𝑥 𝜓 )