Theorem vk15.4j 45278

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 45278 is vk15.4jVD 45663 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
vk15.4j.1	⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
vk15.4j.2	⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
vk15.4j.3	⊢ ¬ ∀𝑥(𝜏 → 𝜑)

Assertion

Ref	Expression
vk15.4j	⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Proof of Theorem vk15.4j

Step	Hyp	Ref	Expression
1		vk15.4j.3	. . . . . 6 ⊢ ¬ ∀𝑥(𝜏 → 𝜑)
2		exanali 1892	. . . . . 6 ⊢ (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏 → 𝜑))
3	1, 2	mpbir 234	. . . . 5 ⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
4		vk15.4j.2	. . . . . 6 ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
5		alex 1859	. . . . . . . . . 10 ⊢ (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
6	5	biimpri 231	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
7	6	19.21bi 2228	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → 𝜃)
8		simpl 488	. . . . . . . . 9 ⊢ ((𝜏 ∧ ¬ 𝜑) → 𝜏)
9	8	a1i 11	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → 𝜏))
10		19.8a 2220	. . . . . . . 8 ⊢ ((𝜃 ∧ 𝜏) → ∃𝑥(𝜃 ∧ 𝜏))
11	7, 9, 10	syl6an 697	. . . . . . 7 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥(𝜃 ∧ 𝜏)))
12		notnot 143	. . . . . . 7 ⊢ (∃𝑥(𝜃 ∧ 𝜏) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏))
13	11, 12	syl6 36	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)))
14		con3 154	. . . . . 6 ⊢ ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) → (¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) → ¬ ∀𝑥𝜒))
15	4, 13, 14	mpsylsyld 70	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ∀𝑥𝜒))
16		hbe1 2181	. . . . . 6 ⊢ (∃𝑥 ¬ 𝜃 → ∀𝑥∃𝑥 ¬ 𝜃)
17	16	hbn 2333	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
18		hbn1 2180	. . . . 5 ⊢ (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
19	3, 15, 17, 18	eexinst01 45276	. . . 4 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜒)
20		exnal 1860	. . . 4 ⊢ (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
21	19, 20	sylibr 237	. . 3 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜒)
22		vk15.4j.1	. . . . . . . . 9 ⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
23		pm3.13 1010	. . . . . . . . 9 ⊢ (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
24	22, 23	ax-mp 5	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
25		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
26	25	a1i 11	. . . . . . . . . . 11 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑))
27		19.8a 2220	. . . . . . . . . . 11 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
28	26, 27	syl6 36	. . . . . . . . . 10 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥 ¬ 𝜑))
29		hbe1 2181	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ 𝜑 → ∀𝑥∃𝑥 ¬ 𝜑)
30	3, 28, 17, 29	eexinst01 45276	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜑)
31		notnot 143	. . . . . . . . 9 ⊢ (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
32	30, 31	syl 18	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ¬ ∃𝑥 ¬ 𝜑)
33		pm2.53 865	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
34	24, 32, 33	mpsyl 69	. . . . . . 7 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35		exanali 1892	. . . . . . . 8 ⊢ (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓 → 𝜒))
36	35	con5i 45273	. . . . . . 7 ⊢ (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓 → 𝜒))
37	34, 36	syl 18	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥(𝜓 → 𝜒))
38	37	19.21bi 2228	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (𝜓 → 𝜒))
39	38	con3d 153	. . . 4 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ¬ 𝜓))
40		19.8a 2220	. . . 4 ⊢ (¬ 𝜓 → ∃𝑥 ¬ 𝜓)
41	39, 40	syl6 36	. . 3 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ∃𝑥 ¬ 𝜓))
42		hbe1 2181	. . 3 ⊢ (∃𝑥 ¬ 𝜓 → ∀𝑥∃𝑥 ¬ 𝜓)
43	21, 41, 17, 42	eexinst11 45277	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜓)
44		exnal 1860	. 2 ⊢ (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
45	43, 44	sylib 221	1 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2179  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by: (None)