Theorem vk15.4jVD 44952

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 44567 is vk15.4jVD 44952 without virtual deductions and was automatically derived from vk15.4jVD 44952. 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 1860	. . . . . . . 8 ⊢ (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏 → 𝜑))
3	2	biimpri 228	. . . . . . 7 ⊢ (¬ ∀𝑥(𝜏 → 𝜑) → ∃𝑥(𝜏 ∧ ¬ 𝜑))
4	1, 3	e0a 44810	. . . . . 6 ⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
5		vk15.4jVD.2	. . . . . . 7 ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
6		idn1 44613	. . . . . . . . . . . 12 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥 ¬ 𝜃   )
7		alex 1827	. . . . . . . . . . . . 13 ⊢ (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
8	7	biimpri 228	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
9	6, 8	e1a 44666	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∀𝑥𝜃   )
10		sp 2186	. . . . . . . . . . 11 ⊢ (∀𝑥𝜃 → 𝜃)
11	9, 10	e1a 44666	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝜃   )
12		idn2 44652	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
13		simpl 482	. . . . . . . . . . 11 ⊢ ((𝜏 ∧ ¬ 𝜑) → 𝜏)
14	12, 13	e2 44670	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
15		pm3.2 469	. . . . . . . . . 10 ⊢ (𝜃 → (𝜏 → (𝜃 ∧ 𝜏)))
16	11, 14, 15	e12 44762	. . . . . . . . 9 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃 ∧ 𝜏)   )
17		19.8a 2184	. . . . . . . . 9 ⊢ ((𝜃 ∧ 𝜏) → ∃𝑥(𝜃 ∧ 𝜏))
18	16, 17	e2 44670	. . . . . . . 8 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥(𝜃 ∧ 𝜏)   )
19		notnot 142	. . . . . . . 8 ⊢ (∃𝑥(𝜃 ∧ 𝜏) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏))
20	18, 19	e2 44670	. . . . . . 7 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)   )
21		con3 153	. . . . . . 7 ⊢ ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) → (¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) → ¬ ∀𝑥𝜒))
22	5, 20, 21	e02 44736	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ∀𝑥𝜒   )
23		hbe1 2146	. . . . . . 7 ⊢ (∃𝑥 ¬ 𝜃 → ∀𝑥∃𝑥 ¬ 𝜃)
24	23	hbn 2297	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
25		hba1 2295	. . . . . . 7 ⊢ (∀𝑥𝜒 → ∀𝑥∀𝑥𝜒)
26	25	hbn 2297	. . . . . 6 ⊢ (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
27	4, 22, 24, 26	exinst01 44664	. . . . 5 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜒   )
28		exnal 1828	. . . . . 6 ⊢ (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
29	28	biimpri 228	. . . . 5 ⊢ (¬ ∀𝑥𝜒 → ∃𝑥 ¬ 𝜒)
30	27, 29	e1a 44666	. . . 4 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜒   )
31		idn2 44652	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜒   )
32		vk15.4jVD.1	. . . . . . . . . 10 ⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
33		pm3.13 996	. . . . . . . . . 10 ⊢ (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
34	32, 33	e0a 44810	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
36	12, 35	e2 44670	. . . . . . . . . . . 12 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ 𝜑   )
37		19.8a 2184	. . . . . . . . . . . 12 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
38	36, 37	e2 44670	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥 ¬ 𝜑   )
39		hbe1 2146	. . . . . . . . . . 11 ⊢ (∃𝑥 ¬ 𝜑 → ∀𝑥∃𝑥 ¬ 𝜑)
40	4, 38, 24, 39	exinst01 44664	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜑   )
41		notnot 142	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
42	40, 41	e1a 44666	. . . . . . . . 9 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ¬ ∃𝑥 ¬ 𝜑   )
43		pm2.53 851	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
44	34, 42, 43	e01 44730	. . . . . . . 8 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)   )
45		exanali 1860	. . . . . . . . 9 ⊢ (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓 → 𝜒))
46	45	con5i 44562	. . . . . . . 8 ⊢ (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓 → 𝜒))
47	44, 46	e1a 44666	. . . . . . 7 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∀𝑥(𝜓 → 𝜒)   )
48		sp 2186	. . . . . . 7 ⊢ (∀𝑥(𝜓 → 𝜒) → (𝜓 → 𝜒))
49	47, 48	e1a 44666	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   (𝜓 → 𝜒)   )
50		con3 153	. . . . . . 7 ⊢ ((𝜓 → 𝜒) → (¬ 𝜒 → ¬ 𝜓))
51	50	com12 32	. . . . . 6 ⊢ (¬ 𝜒 → ((𝜓 → 𝜒) → ¬ 𝜓))
52	31, 49, 51	e21 44768	. . . . 5 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜓   )
53		19.8a 2184	. . . . 5 ⊢ (¬ 𝜓 → ∃𝑥 ¬ 𝜓)
54	52, 53	e2 44670	. . . 4 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶   ∃𝑥 ¬ 𝜓   )
55		hbe1 2146	. . . 4 ⊢ (∃𝑥 ¬ 𝜓 → ∀𝑥∃𝑥 ¬ 𝜓)
56	30, 54, 24, 55	exinst11 44665	. . 3 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜓   )
57		exnal 1828	. . . 4 ⊢ (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
58	57	biimpi 216	. . 3 ⊢ (∃𝑥 ¬ 𝜓 → ¬ ∀𝑥𝜓)
59	56, 58	e1a 44666	. 2 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜓   )
60	59	in1 44610	1 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2144  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-vd1 44609  df-vd2 44617

This theorem is referenced by: (None)