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 43608
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 43222 is vk15.4jVD 43608 without virtual deductions and was automatically derived from vk15.4jVD 43608. 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 1863 . . . . . . . 8 (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏𝜑))
32biimpri 227 . . . . . . 7 (¬ ∀𝑥(𝜏𝜑) → ∃𝑥(𝜏 ∧ ¬ 𝜑))
41, 3e0a 43466 . . . . . 6 𝑥(𝜏 ∧ ¬ 𝜑)
5 vk15.4jVD.2 . . . . . . 7 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
6 idn1 43268 . . . . . . . . . . . 12 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥 ¬ 𝜃   )
7 alex 1829 . . . . . . . . . . . . 13 (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
87biimpri 227 . . . . . . . . . . . 12 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
96, 8e1a 43321 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥𝜃   )
10 sp 2177 . . . . . . . . . . 11 (∀𝑥𝜃𝜃)
119, 10e1a 43321 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝜃   )
12 idn2 43307 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
13 simpl 484 . . . . . . . . . . 11 ((𝜏 ∧ ¬ 𝜑) → 𝜏)
1412, 13e2 43325 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
15 pm3.2 471 . . . . . . . . . 10 (𝜃 → (𝜏 → (𝜃𝜏)))
1611, 14, 15e12 43418 . . . . . . . . 9 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃𝜏)   )
17 19.8a 2175 . . . . . . . . 9 ((𝜃𝜏) → ∃𝑥(𝜃𝜏))
1816, 17e2 43325 . . . . . . . 8 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝑥(𝜃𝜏)   )
19 notnot 142 . . . . . . . 8 (∃𝑥(𝜃𝜏) → ¬ ¬ ∃𝑥(𝜃𝜏))
2018, 19e2 43325 . . . . . . 7 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ¬ ∃𝑥(𝜃𝜏)   )
21 con3 153 . . . . . . 7 ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏)) → (¬ ¬ ∃𝑥(𝜃𝜏) → ¬ ∀𝑥𝜒))
225, 20, 21e02 43391 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ∀𝑥𝜒   )
23 hbe1 2140 . . . . . . 7 (∃𝑥 ¬ 𝜃 → ∀𝑥𝑥 ¬ 𝜃)
2423hbn 2292 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
25 hba1 2290 . . . . . . 7 (∀𝑥𝜒 → ∀𝑥𝑥𝜒)
2625hbn 2292 . . . . . 6 (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
274, 22, 24, 26exinst01 43319 . . . . 5 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜒   )
28 exnal 1830 . . . . . 6 (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
2928biimpri 227 . . . . 5 (¬ ∀𝑥𝜒 → ∃𝑥 ¬ 𝜒)
3027, 29e1a 43321 . . . 4 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜒   )
31 idn2 43307 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜒   )
32 vk15.4jVD.1 . . . . . . . . . 10 ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
33 pm3.13 994 . . . . . . . . . 10 (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
3432, 33e0a 43466 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35 simpr 486 . . . . . . . . . . . . 13 ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
3612, 35e2 43325 . . . . . . . . . . . 12 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ 𝜑   )
37 19.8a 2175 . . . . . . . . . . . 12 𝜑 → ∃𝑥 ¬ 𝜑)
3836, 37e2 43325 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝑥 ¬ 𝜑   )
39 hbe1 2140 . . . . . . . . . . 11 (∃𝑥 ¬ 𝜑 → ∀𝑥𝑥 ¬ 𝜑)
404, 38, 24, 39exinst01 43319 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜑   )
41 notnot 142 . . . . . . . . . 10 (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
4240, 41e1a 43321 . . . . . . . . 9 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ¬ ∃𝑥 ¬ 𝜑   )
43 pm2.53 850 . . . . . . . . 9 ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
4434, 42, 43e01 43385 . . . . . . . 8 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)   )
45 exanali 1863 . . . . . . . . 9 (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓𝜒))
4645con5i 43217 . . . . . . . 8 (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓𝜒))
4744, 46e1a 43321 . . . . . . 7 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥(𝜓𝜒)   )
48 sp 2177 . . . . . . 7 (∀𝑥(𝜓𝜒) → (𝜓𝜒))
4947, 48e1a 43321 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ▶   (𝜓𝜒)   )
50 con3 153 . . . . . . 7 ((𝜓𝜒) → (¬ 𝜒 → ¬ 𝜓))
5150com12 32 . . . . . 6 𝜒 → ((𝜓𝜒) → ¬ 𝜓))
5231, 49, 51e21 43424 . . . . 5 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜓   )
53 19.8a 2175 . . . . 5 𝜓 → ∃𝑥 ¬ 𝜓)
5452, 53e2 43325 . . . 4 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶   𝑥 ¬ 𝜓   )
55 hbe1 2140 . . . 4 (∃𝑥 ¬ 𝜓 → ∀𝑥𝑥 ¬ 𝜓)
5630, 54, 24, 55exinst11 43320 . . 3 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜓   )
57 exnal 1830 . . . 4 (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
5857biimpi 215 . . 3 (∃𝑥 ¬ 𝜓 → ¬ ∀𝑥𝜓)
5956, 58e1a 43321 . 2 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜓   )
6059in1 43265 1 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wo 846  wal 1540  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-vd1 43264  df-vd2 43272
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator