Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  vk15.4jVD Structured version   Visualization version   GIF version

Theorem vk15.4jVD 39672
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 39259 is vk15.4jVD 39672 without virtual deductions and was automatically derived from vk15.4jVD 39672. 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
StepHypRef Expression
1 vk15.4jVD.3 . . . . . . 7 ¬ ∀𝑥(𝜏𝜑)
2 exanali 1937 . . . . . . . 8 (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏𝜑))
32biimpri 218 . . . . . . 7 (¬ ∀𝑥(𝜏𝜑) → ∃𝑥(𝜏 ∧ ¬ 𝜑))
41, 3e0a 39524 . . . . . 6 𝑥(𝜏 ∧ ¬ 𝜑)
5 vk15.4jVD.2 . . . . . . 7 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
6 idn1 39315 . . . . . . . . . . . 12 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥 ¬ 𝜃   )
7 alex 1901 . . . . . . . . . . . . 13 (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
87biimpri 218 . . . . . . . . . . . 12 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
96, 8e1a 39377 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥𝜃   )
10 sp 2207 . . . . . . . . . . 11 (∀𝑥𝜃𝜃)
119, 10e1a 39377 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝜃   )
12 idn2 39363 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
13 simpl 468 . . . . . . . . . . 11 ((𝜏 ∧ ¬ 𝜑) → 𝜏)
1412, 13e2 39381 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
15 pm3.2 446 . . . . . . . . . 10 (𝜃 → (𝜏 → (𝜃𝜏)))
1611, 14, 15e12 39476 . . . . . . . . 9 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃𝜏)   )
17 19.8a 2206 . . . . . . . . 9 ((𝜃𝜏) → ∃𝑥(𝜃𝜏))
1816, 17e2 39381 . . . . . . . 8 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝑥(𝜃𝜏)   )
19 notnot 138 . . . . . . . 8 (∃𝑥(𝜃𝜏) → ¬ ¬ ∃𝑥(𝜃𝜏))
2018, 19e2 39381 . . . . . . 7 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ¬ ∃𝑥(𝜃𝜏)   )
21 con3 150 . . . . . . 7 ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏)) → (¬ ¬ ∃𝑥(𝜃𝜏) → ¬ ∀𝑥𝜒))
225, 20, 21e02 39447 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ∀𝑥𝜒   )
23 hbe1 2176 . . . . . . 7 (∃𝑥 ¬ 𝜃 → ∀𝑥𝑥 ¬ 𝜃)
2423hbn 2311 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
25 hba1 2315 . . . . . . 7 (∀𝑥𝜒 → ∀𝑥𝑥𝜒)
2625hbn 2311 . . . . . 6 (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
274, 22, 24, 26exinst01 39375 . . . . 5 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜒   )
28 exnal 1902 . . . . . 6 (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
2928biimpri 218 . . . . 5 (¬ ∀𝑥𝜒 → ∃𝑥 ¬ 𝜒)
3027, 29e1a 39377 . . . 4 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜒   )
31 idn2 39363 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜒   )
32 vk15.4jVD.1 . . . . . . . . . 10 ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
33 pm3.13 979 . . . . . . . . . 10 (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
3432, 33e0a 39524 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35 simpr 471 . . . . . . . . . . . . 13 ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
3612, 35e2 39381 . . . . . . . . . . . 12 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ 𝜑   )
37 19.8a 2206 . . . . . . . . . . . 12 𝜑 → ∃𝑥 ¬ 𝜑)
3836, 37e2 39381 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝑥 ¬ 𝜑   )
39 hbe1 2176 . . . . . . . . . . 11 (∃𝑥 ¬ 𝜑 → ∀𝑥𝑥 ¬ 𝜑)
404, 38, 24, 39exinst01 39375 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜑   )
41 notnot 138 . . . . . . . . . 10 (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
4240, 41e1a 39377 . . . . . . . . 9 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ¬ ∃𝑥 ¬ 𝜑   )
43 pm2.53 840 . . . . . . . . 9 ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
4434, 42, 43e01 39441 . . . . . . . 8 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)   )
45 exanali 1937 . . . . . . . . 9 (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓𝜒))
4645con5i 39254 . . . . . . . 8 (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓𝜒))
4744, 46e1a 39377 . . . . . . 7 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥(𝜓𝜒)   )
48 sp 2207 . . . . . . 7 (∀𝑥(𝜓𝜒) → (𝜓𝜒))
4947, 48e1a 39377 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ▶   (𝜓𝜒)   )
50 con3 150 . . . . . . 7 ((𝜓𝜒) → (¬ 𝜒 → ¬ 𝜓))
5150com12 32 . . . . . 6 𝜒 → ((𝜓𝜒) → ¬ 𝜓))
5231, 49, 51e21 39482 . . . . 5 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜓   )
53 19.8a 2206 . . . . 5 𝜓 → ∃𝑥 ¬ 𝜓)
5452, 53e2 39381 . . . 4 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶   𝑥 ¬ 𝜓   )
55 hbe1 2176 . . . 4 (∃𝑥 ¬ 𝜓 → ∀𝑥𝑥 ¬ 𝜓)
5630, 54, 24, 55exinst11 39376 . . 3 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜓   )
57 exnal 1902 . . . 4 (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
5857biimpi 206 . . 3 (∃𝑥 ¬ 𝜓 → ¬ ∀𝑥𝜓)
5956, 58e1a 39377 . 2 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜓   )
6059in1 39312 1 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  wo 836  wal 1629  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-ex 1853  df-nf 1858  df-vd1 39311  df-vd2 39319
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator