Theorem vk15.4jVD 41993

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 41607 is vk15.4jVD 41993 without virtual deductions and was automatically derived from vk15.4jVD 41993. 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 231	. . . . . . 7 ⊢ (¬ ∀𝑥(𝜏 → 𝜑) → ∃𝑥(𝜏 ∧ ¬ 𝜑))
4	1, 3	e0a 41851	. . . . . 6 ⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
5		vk15.4jVD.2	. . . . . . 7 ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
6		idn1 41653	. . . . . . . . . . . 12 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥 ¬ 𝜃   )
7		alex 1827	. . . . . . . . . . . . 13 ⊢ (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
8	7	biimpri 231	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
9	6, 8	e1a 41706	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∀𝑥𝜃   )
10		sp 2180	. . . . . . . . . . 11 ⊢ (∀𝑥𝜃 → 𝜃)
11	9, 10	e1a 41706	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝜃   )
12		idn2 41692	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
13		simpl 486	. . . . . . . . . . 11 ⊢ ((𝜏 ∧ ¬ 𝜑) → 𝜏)
14	12, 13	e2 41710	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
15		pm3.2 473	. . . . . . . . . 10 ⊢ (𝜃 → (𝜏 → (𝜃 ∧ 𝜏)))
16	11, 14, 15	e12 41803	. . . . . . . . 9 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃 ∧ 𝜏)   )
17		19.8a 2178	. . . . . . . . 9 ⊢ ((𝜃 ∧ 𝜏) → ∃𝑥(𝜃 ∧ 𝜏))
18	16, 17	e2 41710	. . . . . . . 8 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥(𝜃 ∧ 𝜏)   )
19		notnot 144	. . . . . . . 8 ⊢ (∃𝑥(𝜃 ∧ 𝜏) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏))
20	18, 19	e2 41710	. . . . . . 7 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)   )
21		con3 156	. . . . . . 7 ⊢ ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) → (¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) → ¬ ∀𝑥𝜒))
22	5, 20, 21	e02 41776	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ∀𝑥𝜒   )
23		hbe1 2144	. . . . . . 7 ⊢ (∃𝑥 ¬ 𝜃 → ∀𝑥∃𝑥 ¬ 𝜃)
24	23	hbn 2299	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
25		hba1 2297	. . . . . . 7 ⊢ (∀𝑥𝜒 → ∀𝑥∀𝑥𝜒)
26	25	hbn 2299	. . . . . 6 ⊢ (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
27	4, 22, 24, 26	exinst01 41704	. . . . 5 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜒   )
28		exnal 1828	. . . . . 6 ⊢ (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
29	28	biimpri 231	. . . . 5 ⊢ (¬ ∀𝑥𝜒 → ∃𝑥 ¬ 𝜒)
30	27, 29	e1a 41706	. . . 4 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜒   )
31		idn2 41692	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜒   )
32		vk15.4jVD.1	. . . . . . . . . 10 ⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
33		pm3.13 992	. . . . . . . . . 10 ⊢ (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
34	32, 33	e0a 41851	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
36	12, 35	e2 41710	. . . . . . . . . . . 12 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ 𝜑   )
37		19.8a 2178	. . . . . . . . . . . 12 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
38	36, 37	e2 41710	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥 ¬ 𝜑   )
39		hbe1 2144	. . . . . . . . . . 11 ⊢ (∃𝑥 ¬ 𝜑 → ∀𝑥∃𝑥 ¬ 𝜑)
40	4, 38, 24, 39	exinst01 41704	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜑   )
41		notnot 144	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
42	40, 41	e1a 41706	. . . . . . . . 9 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ¬ ∃𝑥 ¬ 𝜑   )
43		pm2.53 848	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
44	34, 42, 43	e01 41770	. . . . . . . 8 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)   )
45		exanali 1860	. . . . . . . . 9 ⊢ (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓 → 𝜒))
46	45	con5i 41602	. . . . . . . 8 ⊢ (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓 → 𝜒))
47	44, 46	e1a 41706	. . . . . . 7 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∀𝑥(𝜓 → 𝜒)   )
48		sp 2180	. . . . . . 7 ⊢ (∀𝑥(𝜓 → 𝜒) → (𝜓 → 𝜒))
49	47, 48	e1a 41706	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   (𝜓 → 𝜒)   )
50		con3 156	. . . . . . 7 ⊢ ((𝜓 → 𝜒) → (¬ 𝜒 → ¬ 𝜓))
51	50	com12 32	. . . . . 6 ⊢ (¬ 𝜒 → ((𝜓 → 𝜒) → ¬ 𝜓))
52	31, 49, 51	e21 41809	. . . . 5 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜓   )
53		19.8a 2178	. . . . 5 ⊢ (¬ 𝜓 → ∃𝑥 ¬ 𝜓)
54	52, 53	e2 41710	. . . 4 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶   ∃𝑥 ¬ 𝜓   )
55		hbe1 2144	. . . 4 ⊢ (∃𝑥 ¬ 𝜓 → ∀𝑥∃𝑥 ¬ 𝜓)
56	30, 54, 24, 55	exinst11 41705	. . 3 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜓   )
57		exnal 1828	. . . 4 ⊢ (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
58	57	biimpi 219	. . 3 ⊢ (∃𝑥 ¬ 𝜓 → ¬ ∀𝑥𝜓)
59	56, 58	e1a 41706	. 2 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜓   )
60	59	in1 41650	1 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 844  ∀wal 1536  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-vd1 41649  df-vd2 41657

This theorem is referenced by: (None)