Theorem vk15.4jVD 38172

Description: The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 15 Excercise 4.f. found in the "Answers to Starred Exercises" on page 442 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted to be a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. vk15.4j 37755 is vk15.4jVD 38172 without virtual deductions and was automatically derived from vk15.4jVD 38172. Step numbers greater than 25 are additional steps necessary for the sequent calculus proof not contained in the Fitch-style proof. Otherwise, step i of the User's Proof corresponds to step i of the Fitch-style proof.

h1::	⊢ ¬ (∃𝑥¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
h2::	⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏 ))
h3::	⊢ ¬ ∀𝑥(𝜏 → 𝜑)
4::	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ¬ ∃𝑥¬ 𝜃   )
5:4:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ∀𝑥𝜃   )
6:3:	⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
7::	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
8:7:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
9:7:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ¬ 𝜑   )
10:5:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   𝜃   )
11:10,8:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃 ∧ 𝜏)   )
12:11:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥(𝜃 ∧ 𝜏)   )
13:12:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)   )
14:2,13:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ¬ ∀𝑥𝜒   )
140::	⊢ (∃𝑥¬ 𝜃 → ∀𝑥∃𝑥¬ 𝜃 )
141:140:	⊢ (¬ ∃𝑥¬ 𝜃 → ∀𝑥¬ ∃𝑥 ¬ 𝜃)
142::	⊢ (∀𝑥𝜒 → ∀𝑥∀𝑥𝜒)
143:142:	⊢ (¬ ∀𝑥𝜒 → ∀𝑥¬ ∀𝑥𝜒 )
144:6,14,141,143:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ¬ ∀𝑥𝜒    )
15:1:	⊢ (¬ ∃𝑥¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
16:9:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥¬ 𝜑   )
161::	⊢ (∃𝑥¬ 𝜑 → ∀𝑥∃𝑥¬ 𝜑 )
162:6,16,141,161:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ∃𝑥¬ 𝜑    )
17:162:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ¬ ¬ ∃𝑥 ¬ 𝜑   )
18:15,17:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ¬ ∃𝑥( 𝜓 ∧ ¬ 𝜒)   )
19:18:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ∀𝑥(𝜓 → 𝜒)   )
20:144:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ∃𝑥¬ 𝜒    )
21::	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   ¬ 𝜒   ▶   ¬ 𝜒   )
22:19:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   (𝜓 → 𝜒 )   )
23:21,22:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   ¬ 𝜒   ▶   ¬ 𝜓   )
24:23:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   ¬ 𝜒   ▶   ∃ 𝑥¬ 𝜓   )
240::	⊢ (∃𝑥¬ 𝜓 → ∀𝑥∃𝑥¬ 𝜓 )
241:20,24,141,240:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ∃𝑥¬ 𝜓    )
25:241:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ¬ ∀𝑥𝜓    )
qed:25:	⊢ (¬ ∃𝑥¬ 𝜃 → ¬ ∀𝑥𝜓)

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

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

Assertion

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

Proof of Theorem vk15.4jVD

Step	Hyp	Ref	Expression
1		vk15.4jVD.3	. . . . . . 7 ⊢ ¬ ∀𝑥(𝜏 → 𝜑)
2		exanali 1773	. . . . . . . 8 ⊢ (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏 → 𝜑))
3	2	biimpri 217	. . . . . . 7 ⊢ (¬ ∀𝑥(𝜏 → 𝜑) → ∃𝑥(𝜏 ∧ ¬ 𝜑))
4	1, 3	e0a 38020	. . . . . 6 ⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
5		vk15.4jVD.2	. . . . . . 7 ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
6		idn1 37811	. . . . . . . . . . . 12 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥 ¬ 𝜃   )
7		alex 1743	. . . . . . . . . . . . 13 ⊢ (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
8	7	biimpri 217	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
9	6, 8	e1a 37873	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∀𝑥𝜃   )
10		sp 2041	. . . . . . . . . . 11 ⊢ (∀𝑥𝜃 → 𝜃)
11	9, 10	e1a 37873	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝜃   )
12		idn2 37859	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
13		simpl 472	. . . . . . . . . . 11 ⊢ ((𝜏 ∧ ¬ 𝜑) → 𝜏)
14	12, 13	e2 37877	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
15		pm3.2 462	. . . . . . . . . 10 ⊢ (𝜃 → (𝜏 → (𝜃 ∧ 𝜏)))
16	11, 14, 15	e12 37972	. . . . . . . . 9 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃 ∧ 𝜏)   )
17		19.8a 2039	. . . . . . . . 9 ⊢ ((𝜃 ∧ 𝜏) → ∃𝑥(𝜃 ∧ 𝜏))
18	16, 17	e2 37877	. . . . . . . 8 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥(𝜃 ∧ 𝜏)   )
19		notnot 135	. . . . . . . 8 ⊢ (∃𝑥(𝜃 ∧ 𝜏) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏))
20	18, 19	e2 37877	. . . . . . 7 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)   )
21		con3 148	. . . . . . 7 ⊢ ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) → (¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) → ¬ ∀𝑥𝜒))
22	5, 20, 21	e02 37943	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ∀𝑥𝜒   )
23		hbe1 2008	. . . . . . 7 ⊢ (∃𝑥 ¬ 𝜃 → ∀𝑥∃𝑥 ¬ 𝜃)
24	23	hbn 2131	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
25		hba1 2137	. . . . . . 7 ⊢ (∀𝑥𝜒 → ∀𝑥∀𝑥𝜒)
26	25	hbn 2131	. . . . . 6 ⊢ (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
27	4, 22, 24, 26	exinst01 37871	. . . . 5 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜒   )
28		exnal 1744	. . . . . 6 ⊢ (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
29	28	biimpri 217	. . . . 5 ⊢ (¬ ∀𝑥𝜒 → ∃𝑥 ¬ 𝜒)
30	27, 29	e1a 37873	. . . 4 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜒   )
31		idn2 37859	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜒   )
32		vk15.4jVD.1	. . . . . . . . . 10 ⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
33		pm3.13 521	. . . . . . . . . 10 ⊢ (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
34	32, 33	e0a 38020	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35		simpr 476	. . . . . . . . . . . . 13 ⊢ ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
36	12, 35	e2 37877	. . . . . . . . . . . 12 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ 𝜑   )
37		19.8a 2039	. . . . . . . . . . . 12 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
38	36, 37	e2 37877	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥 ¬ 𝜑   )
39		hbe1 2008	. . . . . . . . . . 11 ⊢ (∃𝑥 ¬ 𝜑 → ∀𝑥∃𝑥 ¬ 𝜑)
40	4, 38, 24, 39	exinst01 37871	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜑   )
41		notnot 135	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
42	40, 41	e1a 37873	. . . . . . . . 9 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ¬ ∃𝑥 ¬ 𝜑   )
43		pm2.53 387	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
44	34, 42, 43	e01 37937	. . . . . . . 8 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)   )
45		exanali 1773	. . . . . . . . 9 ⊢ (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓 → 𝜒))
46	45	con5i 37750	. . . . . . . 8 ⊢ (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓 → 𝜒))
47	44, 46	e1a 37873	. . . . . . 7 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∀𝑥(𝜓 → 𝜒)   )
48		sp 2041	. . . . . . 7 ⊢ (∀𝑥(𝜓 → 𝜒) → (𝜓 → 𝜒))
49	47, 48	e1a 37873	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   (𝜓 → 𝜒)   )
50		con3 148	. . . . . . 7 ⊢ ((𝜓 → 𝜒) → (¬ 𝜒 → ¬ 𝜓))
51	50	com12 32	. . . . . 6 ⊢ (¬ 𝜒 → ((𝜓 → 𝜒) → ¬ 𝜓))
52	31, 49, 51	e21 37978	. . . . 5 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜓   )
53		19.8a 2039	. . . . 5 ⊢ (¬ 𝜓 → ∃𝑥 ¬ 𝜓)
54	52, 53	e2 37877	. . . 4 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶   ∃𝑥 ¬ 𝜓   )
55		hbe1 2008	. . . 4 ⊢ (∃𝑥 ¬ 𝜓 → ∀𝑥∃𝑥 ¬ 𝜓)
56	30, 54, 24, 55	exinst11 37872	. . 3 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜓   )
57		exnal 1744	. . . 4 ⊢ (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
58	57	biimpi 205	. . 3 ⊢ (∃𝑥 ¬ 𝜓 → ¬ ∀𝑥𝜓)
59	56, 58	e1a 37873	. 2 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜓   )
60	59	in1 37808	1 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701  df-vd1 37807  df-vd2 37815

This theorem is referenced by: (None)