Theorem vk15.4jVD 45449

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 45064 is vk15.4jVD 45449 without virtual deductions and was automatically derived from vk15.4jVD 45449. 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 1878	. . . . . . . 8 ⊢ (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏 → 𝜑))
3	2	biimpri 230	. . . . . . 7 ⊢ (¬ ∀𝑥(𝜏 → 𝜑) → ∃𝑥(𝜏 ∧ ¬ 𝜑))
4	1, 3	e0a 45307	. . . . . 6 ⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
5		vk15.4jVD.2	. . . . . . 7 ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
6		idn1 45110	. . . . . . . . . . . 12 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥 ¬ 𝜃   )
7		alex 1845	. . . . . . . . . . . . 13 ⊢ (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
8	7	biimpri 230	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
9	6, 8	e1a 45163	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∀𝑥𝜃   )
10		sp 2217	. . . . . . . . . . 11 ⊢ (∀𝑥𝜃 → 𝜃)
11	9, 10	e1a 45163	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝜃   )
12		idn2 45149	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
13		simpl 486	. . . . . . . . . . 11 ⊢ ((𝜏 ∧ ¬ 𝜑) → 𝜏)
14	12, 13	e2 45167	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
15		pm3.2 473	. . . . . . . . . 10 ⊢ (𝜃 → (𝜏 → (𝜃 ∧ 𝜏)))
16	11, 14, 15	e12 45259	. . . . . . . . 9 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃 ∧ 𝜏)   )
17		19.8a 2215	. . . . . . . . 9 ⊢ ((𝜃 ∧ 𝜏) → ∃𝑥(𝜃 ∧ 𝜏))
18	16, 17	e2 45167	. . . . . . . 8 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥(𝜃 ∧ 𝜏)   )
19		notnot 142	. . . . . . . 8 ⊢ (∃𝑥(𝜃 ∧ 𝜏) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏))
20	18, 19	e2 45167	. . . . . . 7 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)   )
21		con3 153	. . . . . . 7 ⊢ ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) → (¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) → ¬ ∀𝑥𝜒))
22	5, 20, 21	e02 45233	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ∀𝑥𝜒   )
23		hbe1 2176	. . . . . . 7 ⊢ (∃𝑥 ¬ 𝜃 → ∀𝑥∃𝑥 ¬ 𝜃)
24	23	hbn 2328	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
25		hba1 2326	. . . . . . 7 ⊢ (∀𝑥𝜒 → ∀𝑥∀𝑥𝜒)
26	25	hbn 2328	. . . . . 6 ⊢ (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
27	4, 22, 24, 26	exinst01 45161	. . . . 5 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜒   )
28		exnal 1846	. . . . . 6 ⊢ (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
29	28	biimpri 230	. . . . 5 ⊢ (¬ ∀𝑥𝜒 → ∃𝑥 ¬ 𝜒)
30	27, 29	e1a 45163	. . . 4 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜒   )
31		idn2 45149	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜒   )
32		vk15.4jVD.1	. . . . . . . . . 10 ⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
33		pm3.13 1007	. . . . . . . . . 10 ⊢ (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
34	32, 33	e0a 45307	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
36	12, 35	e2 45167	. . . . . . . . . . . 12 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ 𝜑   )
37		19.8a 2215	. . . . . . . . . . . 12 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
38	36, 37	e2 45167	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥 ¬ 𝜑   )
39		hbe1 2176	. . . . . . . . . . 11 ⊢ (∃𝑥 ¬ 𝜑 → ∀𝑥∃𝑥 ¬ 𝜑)
40	4, 38, 24, 39	exinst01 45161	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜑   )
41		notnot 142	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
42	40, 41	e1a 45163	. . . . . . . . 9 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ¬ ∃𝑥 ¬ 𝜑   )
43		pm2.53 862	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
44	34, 42, 43	e01 45227	. . . . . . . 8 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)   )
45		exanali 1878	. . . . . . . . 9 ⊢ (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓 → 𝜒))
46	45	con5i 45059	. . . . . . . 8 ⊢ (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓 → 𝜒))
47	44, 46	e1a 45163	. . . . . . 7 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∀𝑥(𝜓 → 𝜒)   )
48		sp 2217	. . . . . . 7 ⊢ (∀𝑥(𝜓 → 𝜒) → (𝜓 → 𝜒))
49	47, 48	e1a 45163	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   (𝜓 → 𝜒)   )
50		con3 153	. . . . . . 7 ⊢ ((𝜓 → 𝜒) → (¬ 𝜒 → ¬ 𝜓))
51	50	com12 32	. . . . . 6 ⊢ (¬ 𝜒 → ((𝜓 → 𝜒) → ¬ 𝜓))
52	31, 49, 51	e21 45265	. . . . 5 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜓   )
53		19.8a 2215	. . . . 5 ⊢ (¬ 𝜓 → ∃𝑥 ¬ 𝜓)
54	52, 53	e2 45167	. . . 4 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶   ∃𝑥 ¬ 𝜓   )
55		hbe1 2176	. . . 4 ⊢ (∃𝑥 ¬ 𝜓 → ∀𝑥∃𝑥 ¬ 𝜓)
56	30, 54, 24, 55	exinst11 45162	. . 3 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜓   )
57		exnal 1846	. . . 4 ⊢ (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
58	57	biimpi 218	. . 3 ⊢ (∃𝑥 ¬ 𝜓 → ¬ ∀𝑥𝜓)
59	56, 58	e1a 45163	. 2 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜓   )
60	59	in1 45107	1 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 858  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-10 2174  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-nf 1803  df-vd1 45106  df-vd2 45114

This theorem is referenced by: (None)