Theorem vk15.4j 41234

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 41234 is vk15.4jVD 41620 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 1860	. . . . . 6 ⊢ (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏 → 𝜑))
3	1, 2	mpbir 234	. . . . 5 ⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
4		vk15.4j.2	. . . . . 6 ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
5		alex 1827	. . . . . . . . . 10 ⊢ (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
6	5	biimpri 231	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
7	6	19.21bi 2186	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → 𝜃)
8		simpl 486	. . . . . . . . 9 ⊢ ((𝜏 ∧ ¬ 𝜑) → 𝜏)
9	8	a1i 11	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → 𝜏))
10		19.8a 2178	. . . . . . . 8 ⊢ ((𝜃 ∧ 𝜏) → ∃𝑥(𝜃 ∧ 𝜏))
11	7, 9, 10	syl6an 683	. . . . . . 7 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥(𝜃 ∧ 𝜏)))
12		notnot 144	. . . . . . 7 ⊢ (∃𝑥(𝜃 ∧ 𝜏) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏))
13	11, 12	syl6 35	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)))
14		con3 156	. . . . . 6 ⊢ ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) → (¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) → ¬ ∀𝑥𝜒))
15	4, 13, 14	mpsylsyld 69	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ∀𝑥𝜒))
16		hbe1 2144	. . . . . 6 ⊢ (∃𝑥 ¬ 𝜃 → ∀𝑥∃𝑥 ¬ 𝜃)
17	16	hbn 2299	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
18		hbn1 2143	. . . . 5 ⊢ (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
19	3, 15, 17, 18	eexinst01 41232	. . . 4 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜒)
20		exnal 1828	. . . 4 ⊢ (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
21	19, 20	sylibr 237	. . 3 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜒)
22		vk15.4j.1	. . . . . . . . 9 ⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
23		pm3.13 992	. . . . . . . . 9 ⊢ (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
24	22, 23	ax-mp 5	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
25		simpr 488	. . . . . . . . . . . 12 ⊢ ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
26	25	a1i 11	. . . . . . . . . . 11 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑))
27		19.8a 2178	. . . . . . . . . . 11 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
28	26, 27	syl6 35	. . . . . . . . . 10 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥 ¬ 𝜑))
29		hbe1 2144	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ 𝜑 → ∀𝑥∃𝑥 ¬ 𝜑)
30	3, 28, 17, 29	eexinst01 41232	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜑)
31		notnot 144	. . . . . . . . 9 ⊢ (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
32	30, 31	syl 17	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ¬ ∃𝑥 ¬ 𝜑)
33		pm2.53 848	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
34	24, 32, 33	mpsyl 68	. . . . . . 7 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35		exanali 1860	. . . . . . . 8 ⊢ (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓 → 𝜒))
36	35	con5i 41229	. . . . . . 7 ⊢ (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓 → 𝜒))
37	34, 36	syl 17	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥(𝜓 → 𝜒))
38	37	19.21bi 2186	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (𝜓 → 𝜒))
39	38	con3d 155	. . . 4 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ¬ 𝜓))
40		19.8a 2178	. . . 4 ⊢ (¬ 𝜓 → ∃𝑥 ¬ 𝜓)
41	39, 40	syl6 35	. . 3 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ∃𝑥 ¬ 𝜓))
42		hbe1 2144	. . 3 ⊢ (∃𝑥 ¬ 𝜓 → ∀𝑥∃𝑥 ¬ 𝜓)
43	21, 41, 17, 42	eexinst11 41233	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜓)
44		exnal 1828	. 2 ⊢ (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
45	43, 44	sylib 221	1 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 844  ∀wal 1536  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786

This theorem is referenced by: (None)