Theorem vk15.4j 44979

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 44979 is vk15.4jVD 45364 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 1866	. . . . . 6 ⊢ (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏 → 𝜑))
3	1, 2	mpbir 232	. . . . 5 ⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
4		vk15.4j.2	. . . . . 6 ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
5		alex 1833	. . . . . . . . . 10 ⊢ (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
6	5	biimpri 229	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
7	6	19.21bi 2201	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → 𝜃)
8		simpl 483	. . . . . . . . 9 ⊢ ((𝜏 ∧ ¬ 𝜑) → 𝜏)
9	8	a1i 11	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → 𝜏))
10		19.8a 2193	. . . . . . . 8 ⊢ ((𝜃 ∧ 𝜏) → ∃𝑥(𝜃 ∧ 𝜏))
11	7, 9, 10	syl6an 690	. . . . . . 7 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥(𝜃 ∧ 𝜏)))
12		notnot 142	. . . . . . 7 ⊢ (∃𝑥(𝜃 ∧ 𝜏) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏))
13	11, 12	syl6 35	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)))
14		con3 153	. . . . . 6 ⊢ ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) → (¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) → ¬ ∀𝑥𝜒))
15	4, 13, 14	mpsylsyld 69	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ∀𝑥𝜒))
16		hbe1 2154	. . . . . 6 ⊢ (∃𝑥 ¬ 𝜃 → ∀𝑥∃𝑥 ¬ 𝜃)
17	16	hbn 2306	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
18		hbn1 2153	. . . . 5 ⊢ (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
19	3, 15, 17, 18	eexinst01 44977	. . . 4 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜒)
20		exnal 1834	. . . 4 ⊢ (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
21	19, 20	sylibr 235	. . 3 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜒)
22		vk15.4j.1	. . . . . . . . 9 ⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
23		pm3.13 1002	. . . . . . . . 9 ⊢ (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
24	22, 23	ax-mp 5	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
25		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
26	25	a1i 11	. . . . . . . . . . 11 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑))
27		19.8a 2193	. . . . . . . . . . 11 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
28	26, 27	syl6 35	. . . . . . . . . 10 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥 ¬ 𝜑))
29		hbe1 2154	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ 𝜑 → ∀𝑥∃𝑥 ¬ 𝜑)
30	3, 28, 17, 29	eexinst01 44977	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜑)
31		notnot 142	. . . . . . . . 9 ⊢ (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
32	30, 31	syl 17	. . . . . . . 8 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ¬ ∃𝑥 ¬ 𝜑)
33		pm2.53 857	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
34	24, 32, 33	mpsyl 68	. . . . . . 7 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35		exanali 1866	. . . . . . . 8 ⊢ (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓 → 𝜒))
36	35	con5i 44974	. . . . . . 7 ⊢ (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓 → 𝜒))
37	34, 36	syl 17	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥(𝜓 → 𝜒))
38	37	19.21bi 2201	. . . . 5 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (𝜓 → 𝜒))
39	38	con3d 152	. . . 4 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ¬ 𝜓))
40		19.8a 2193	. . . 4 ⊢ (¬ 𝜓 → ∃𝑥 ¬ 𝜓)
41	39, 40	syl6 35	. . 3 ⊢ (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ∃𝑥 ¬ 𝜓))
42		hbe1 2154	. . 3 ⊢ (∃𝑥 ¬ 𝜓 → ∀𝑥∃𝑥 ¬ 𝜓)
43	21, 41, 17, 42	eexinst11 44978	. 2 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜓)
44		exnal 1834	. 2 ⊢ (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
45	43, 44	sylib 219	1 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 853  ∀wal 1545  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791

This theorem is referenced by: (None)