Theorem vk15.4j 42148

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 42148 is vk15.4jVD 42534 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 1862	. . . . . 6 ⊢ (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏 → 𝜑))
3	1, 2	mpbir 230	. . . . 5 ⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
4		vk15.4j.2	. . . . . 6 ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
5		alex 1828	. . . . . . . . . 10 ⊢ (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
6	5	biimpri 227	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
7	6	19.21bi 2182	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → 𝜃)
8		simpl 483	. . . . . . . . 9 ⊢ ((𝜏 ∧ ¬ 𝜑) → 𝜏)
9	8	a1i 11	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → 𝜏))
10		19.8a 2174	. . . . . . . 8 ⊢ ((𝜃 ∧ 𝜏) → ∃𝑥(𝜃 ∧ 𝜏))
11	7, 9, 10	syl6an 681	. . . . . . 7 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥(𝜃 ∧ 𝜏)))
12		notnot 142	. . . . . . 7 ⊢ (∃𝑥(𝜃 ∧ 𝜏) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏))
13	11, 12	syl6 35	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)))
14		con3 153	. . . . . 6 ⊢ ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) → (¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) → ¬ ∀𝑥𝜒))
15	4, 13, 14	mpsylsyld 69	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ∀𝑥𝜒))
16		hbe1 2139	. . . . . 6 ⊢ (∃𝑥 ¬ 𝜃 → ∀𝑥∃𝑥 ¬ 𝜃)
17	16	hbn 2292	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
18		hbn1 2138	. . . . 5 ⊢ (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
19	3, 15, 17, 18	eexinst01 42146	. . . 4 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜒)
20		exnal 1829	. . . 4 ⊢ (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
21	19, 20	sylibr 233	. . 3 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜒)
22		vk15.4j.1	. . . . . . . . 9 ⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
23		pm3.13 992	. . . . . . . . 9 ⊢ (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
24	22, 23	ax-mp 5	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
25		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
26	25	a1i 11	. . . . . . . . . . 11 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑))
27		19.8a 2174	. . . . . . . . . . 11 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
28	26, 27	syl6 35	. . . . . . . . . 10 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥 ¬ 𝜑))
29		hbe1 2139	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ 𝜑 → ∀𝑥∃𝑥 ¬ 𝜑)
30	3, 28, 17, 29	eexinst01 42146	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜑)
31		notnot 142	. . . . . . . . 9 ⊢ (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
32	30, 31	syl 17	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ¬ ∃𝑥 ¬ 𝜑)
33		pm2.53 848	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
34	24, 32, 33	mpsyl 68	. . . . . . 7 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35		exanali 1862	. . . . . . . 8 ⊢ (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓 → 𝜒))
36	35	con5i 42143	. . . . . . 7 ⊢ (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓 → 𝜒))
37	34, 36	syl 17	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥(𝜓 → 𝜒))
38	37	19.21bi 2182	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (𝜓 → 𝜒))
39	38	con3d 152	. . . 4 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ¬ 𝜓))
40		19.8a 2174	. . . 4 ⊢ (¬ 𝜓 → ∃𝑥 ¬ 𝜓)
41	39, 40	syl6 35	. . 3 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ∃𝑥 ¬ 𝜓))
42		hbe1 2139	. . 3 ⊢ (∃𝑥 ¬ 𝜓 → ∀𝑥∃𝑥 ¬ 𝜓)
43	21, 41, 17, 42	eexinst11 42147	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜓)
44		exnal 1829	. 2 ⊢ (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
45	43, 44	sylib 217	1 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 844  ∀wal 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787

This theorem is referenced by: (None)