Theorem vk15.4jVD 45481

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 45096 is vk15.4jVD 45481 without virtual deductions and was automatically derived from vk15.4jVD 45481. 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 1882	. . . . . . . 8 ⊢ (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏 → 𝜑))
3	2	biimpri 231	. . . . . . 7 ⊢ (¬ ∀𝑥(𝜏 → 𝜑) → ∃𝑥(𝜏 ∧ ¬ 𝜑))
4	1, 3	e0a 45339	. . . . . 6 ⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
5		vk15.4jVD.2	. . . . . . 7 ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))
6		idn1 45142	. . . . . . . . . . . 12 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥 ¬ 𝜃   )
7		alex 1849	. . . . . . . . . . . . 13 ⊢ (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
8	7	biimpri 231	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
9	6, 8	e1a 45195	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∀𝑥𝜃   )
10		sp 2221	. . . . . . . . . . 11 ⊢ (∀𝑥𝜃 → 𝜃)
11	9, 10	e1a 45195	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝜃   )
12		idn2 45181	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
13		simpl 487	. . . . . . . . . . 11 ⊢ ((𝜏 ∧ ¬ 𝜑) → 𝜏)
14	12, 13	e2 45199	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
15		pm3.2 474	. . . . . . . . . 10 ⊢ (𝜃 → (𝜏 → (𝜃 ∧ 𝜏)))
16	11, 14, 15	e12 45291	. . . . . . . . 9 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃 ∧ 𝜏)   )
17		19.8a 2219	. . . . . . . . 9 ⊢ ((𝜃 ∧ 𝜏) → ∃𝑥(𝜃 ∧ 𝜏))
18	16, 17	e2 45199	. . . . . . . 8 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥(𝜃 ∧ 𝜏)   )
19		notnot 143	. . . . . . . 8 ⊢ (∃𝑥(𝜃 ∧ 𝜏) → ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏))
20	18, 19	e2 45199	. . . . . . 7 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)   )
21		con3 154	. . . . . . 7 ⊢ ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏)) → (¬ ¬ ∃𝑥(𝜃 ∧ 𝜏) → ¬ ∀𝑥𝜒))
22	5, 20, 21	e02 45265	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ∀𝑥𝜒   )
23		hbe1 2180	. . . . . . 7 ⊢ (∃𝑥 ¬ 𝜃 → ∀𝑥∃𝑥 ¬ 𝜃)
24	23	hbn 2332	. . . . . 6 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
25		hba1 2330	. . . . . . 7 ⊢ (∀𝑥𝜒 → ∀𝑥∀𝑥𝜒)
26	25	hbn 2332	. . . . . 6 ⊢ (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
27	4, 22, 24, 26	exinst01 45193	. . . . 5 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜒   )
28		exnal 1850	. . . . . 6 ⊢ (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
29	28	biimpri 231	. . . . 5 ⊢ (¬ ∀𝑥𝜒 → ∃𝑥 ¬ 𝜒)
30	27, 29	e1a 45195	. . . 4 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜒   )
31		idn2 45181	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜒   )
32		vk15.4jVD.1	. . . . . . . . . 10 ⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
33		pm3.13 1010	. . . . . . . . . 10 ⊢ (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
34	32, 33	e0a 45339	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
36	12, 35	e2 45199	. . . . . . . . . . . 12 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ 𝜑   )
37		19.8a 2219	. . . . . . . . . . . 12 ⊢ (¬ 𝜑 → ∃𝑥 ¬ 𝜑)
38	36, 37	e2 45199	. . . . . . . . . . 11 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥 ¬ 𝜑   )
39		hbe1 2180	. . . . . . . . . . 11 ⊢ (∃𝑥 ¬ 𝜑 → ∀𝑥∃𝑥 ¬ 𝜑)
40	4, 38, 24, 39	exinst01 45193	. . . . . . . . . 10 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜑   )
41		notnot 143	. . . . . . . . . 10 ⊢ (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
42	40, 41	e1a 45195	. . . . . . . . 9 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ¬ ∃𝑥 ¬ 𝜑   )
43		pm2.53 864	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
44	34, 42, 43	e01 45259	. . . . . . . 8 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)   )
45		exanali 1882	. . . . . . . . 9 ⊢ (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓 → 𝜒))
46	45	con5i 45091	. . . . . . . 8 ⊢ (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓 → 𝜒))
47	44, 46	e1a 45195	. . . . . . 7 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∀𝑥(𝜓 → 𝜒)   )
48		sp 2221	. . . . . . 7 ⊢ (∀𝑥(𝜓 → 𝜒) → (𝜓 → 𝜒))
49	47, 48	e1a 45195	. . . . . 6 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   (𝜓 → 𝜒)   )
50		con3 154	. . . . . . 7 ⊢ ((𝜓 → 𝜒) → (¬ 𝜒 → ¬ 𝜓))
51	50	com12 33	. . . . . 6 ⊢ (¬ 𝜒 → ((𝜓 → 𝜒) → ¬ 𝜓))
52	31, 49, 51	e21 45297	. . . . 5 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜓   )
53		19.8a 2219	. . . . 5 ⊢ (¬ 𝜓 → ∃𝑥 ¬ 𝜓)
54	52, 53	e2 45199	. . . 4 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶   ∃𝑥 ¬ 𝜓   )
55		hbe1 2180	. . . 4 ⊢ (∃𝑥 ¬ 𝜓 → ∀𝑥∃𝑥 ¬ 𝜓)
56	30, 54, 24, 55	exinst11 45194	. . 3 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶   ∃𝑥 ¬ 𝜓   )
57		exnal 1850	. . . 4 ⊢ (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
58	57	biimpi 219	. . 3 ⊢ (∃𝑥 ¬ 𝜓 → ¬ ∀𝑥𝜓)
59	56, 58	e1a 45195	. 2 ⊢ (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜓   )
60	59	in1 45139	1 ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∨ wo 860  ∀wal 1561  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-10 2178  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-nf 1807  df-vd1 45138  df-vd2 45146

This theorem is referenced by: (None)