Theorem vk15.4j 44499

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 44499 is vk15.4jVD 44885 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 1858	. . . . . 6 ⊢ (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏 → 𝜑))
3	1, 2	mpbir 231	. . . . 5 ⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
4		vk15.4j.2	. . . . . 6 ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
5		alex 1824	. . . . . . . . . 10 ⊢ (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
6	5	biimpri 228	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
7	6	19.21bi 2190	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → 𝜃)
8		simpl 482	. . . . . . . . 9 ⊢ ((𝜏 ∧ ¬ 𝜑) → 𝜏)
9	8	a1i 11	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → 𝜏))
10		19.8a 2182	. . . . . . . 8 ⊢ ((𝜃 ∧ 𝜏) → ∃𝑥(𝜃 ∧ 𝜏))
11	7, 9, 10	syl6an 683	. . . . . . 7 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥(𝜃 ∧ 𝜏)))
12		notnot 142	. . . . . . 7 ⊢ (∃𝑥(𝜃 ∧ 𝜏) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏))
13	11, 12	syl6 35	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)))
14		con3 153	. . . . . 6 ⊢ ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) → (¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) → ¬ ∀𝑥𝜒))
15	4, 13, 14	mpsylsyld 69	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ∀𝑥𝜒))
16		hbe1 2143	. . . . . 6 ⊢ (∃𝑥 ¬ 𝜃 → ∀𝑥∃𝑥 ¬ 𝜃)
17	16	hbn 2299	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
18		hbn1 2142	. . . . 5 ⊢ (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
19	3, 15, 17, 18	eexinst01 44497	. . . 4 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜒)
20		exnal 1825	. . . 4 ⊢ (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
21	19, 20	sylibr 234	. . 3 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜒)
22		vk15.4j.1	. . . . . . . . 9 ⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
23		pm3.13 995	. . . . . . . . 9 ⊢ (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
24	22, 23	ax-mp 5	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
25		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
26	25	a1i 11	. . . . . . . . . . 11 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑))
27		19.8a 2182	. . . . . . . . . . 11 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
28	26, 27	syl6 35	. . . . . . . . . 10 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥 ¬ 𝜑))
29		hbe1 2143	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ 𝜑 → ∀𝑥∃𝑥 ¬ 𝜑)
30	3, 28, 17, 29	eexinst01 44497	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜑)
31		notnot 142	. . . . . . . . 9 ⊢ (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
32	30, 31	syl 17	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ¬ ∃𝑥 ¬ 𝜑)
33		pm2.53 850	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
34	24, 32, 33	mpsyl 68	. . . . . . 7 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35		exanali 1858	. . . . . . . 8 ⊢ (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓 → 𝜒))
36	35	con5i 44494	. . . . . . 7 ⊢ (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓 → 𝜒))
37	34, 36	syl 17	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥(𝜓 → 𝜒))
38	37	19.21bi 2190	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (𝜓 → 𝜒))
39	38	con3d 152	. . . 4 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ¬ 𝜓))
40		19.8a 2182	. . . 4 ⊢ (¬ 𝜓 → ∃𝑥 ¬ 𝜓)
41	39, 40	syl6 35	. . 3 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ∃𝑥 ¬ 𝜓))
42		hbe1 2143	. . 3 ⊢ (∃𝑥 ¬ 𝜓 → ∀𝑥∃𝑥 ¬ 𝜓)
43	21, 41, 17, 42	eexinst11 44498	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜓)
44		exnal 1825	. 2 ⊢ (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
45	43, 44	sylib 218	1 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 846  ∀wal 1535  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782

This theorem is referenced by: (None)