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 38970
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 38554 is vk15.4jVD 38970 without virtual deductions and was automatically derived from vk15.4jVD 38970. 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 1784 . . . . . . . 8 (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏𝜑))
32biimpri 218 . . . . . . 7 (¬ ∀𝑥(𝜏𝜑) → ∃𝑥(𝜏 ∧ ¬ 𝜑))
41, 3e0a 38819 . . . . . 6 𝑥(𝜏 ∧ ¬ 𝜑)
5 vk15.4jVD.2 . . . . . . 7 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
6 idn1 38610 . . . . . . . . . . . 12 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥 ¬ 𝜃   )
7 alex 1751 . . . . . . . . . . . . 13 (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
87biimpri 218 . . . . . . . . . . . 12 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
96, 8e1a 38672 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥𝜃   )
10 sp 2051 . . . . . . . . . . 11 (∀𝑥𝜃𝜃)
119, 10e1a 38672 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝜃   )
12 idn2 38658 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
13 simpl 473 . . . . . . . . . . 11 ((𝜏 ∧ ¬ 𝜑) → 𝜏)
1412, 13e2 38676 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
15 pm3.2 463 . . . . . . . . . 10 (𝜃 → (𝜏 → (𝜃𝜏)))
1611, 14, 15e12 38771 . . . . . . . . 9 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃𝜏)   )
17 19.8a 2050 . . . . . . . . 9 ((𝜃𝜏) → ∃𝑥(𝜃𝜏))
1816, 17e2 38676 . . . . . . . 8 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝑥(𝜃𝜏)   )
19 notnot 136 . . . . . . . 8 (∃𝑥(𝜃𝜏) → ¬ ¬ ∃𝑥(𝜃𝜏))
2018, 19e2 38676 . . . . . . 7 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ¬ ∃𝑥(𝜃𝜏)   )
21 con3 149 . . . . . . 7 ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏)) → (¬ ¬ ∃𝑥(𝜃𝜏) → ¬ ∀𝑥𝜒))
225, 20, 21e02 38742 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ∀𝑥𝜒   )
23 hbe1 2019 . . . . . . 7 (∃𝑥 ¬ 𝜃 → ∀𝑥𝑥 ¬ 𝜃)
2423hbn 2144 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
25 hba1 2149 . . . . . . 7 (∀𝑥𝜒 → ∀𝑥𝑥𝜒)
2625hbn 2144 . . . . . 6 (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
274, 22, 24, 26exinst01 38670 . . . . 5 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜒   )
28 exnal 1752 . . . . . 6 (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
2928biimpri 218 . . . . 5 (¬ ∀𝑥𝜒 → ∃𝑥 ¬ 𝜒)
3027, 29e1a 38672 . . . 4 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜒   )
31 idn2 38658 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜒   )
32 vk15.4jVD.1 . . . . . . . . . 10 ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
33 pm3.13 522 . . . . . . . . . 10 (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
3432, 33e0a 38819 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35 simpr 477 . . . . . . . . . . . . 13 ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
3612, 35e2 38676 . . . . . . . . . . . 12 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ 𝜑   )
37 19.8a 2050 . . . . . . . . . . . 12 𝜑 → ∃𝑥 ¬ 𝜑)
3836, 37e2 38676 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝑥 ¬ 𝜑   )
39 hbe1 2019 . . . . . . . . . . 11 (∃𝑥 ¬ 𝜑 → ∀𝑥𝑥 ¬ 𝜑)
404, 38, 24, 39exinst01 38670 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜑   )
41 notnot 136 . . . . . . . . . 10 (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
4240, 41e1a 38672 . . . . . . . . 9 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ¬ ∃𝑥 ¬ 𝜑   )
43 pm2.53 388 . . . . . . . . 9 ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
4434, 42, 43e01 38736 . . . . . . . 8 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)   )
45 exanali 1784 . . . . . . . . 9 (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓𝜒))
4645con5i 38549 . . . . . . . 8 (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓𝜒))
4744, 46e1a 38672 . . . . . . 7 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥(𝜓𝜒)   )
48 sp 2051 . . . . . . 7 (∀𝑥(𝜓𝜒) → (𝜓𝜒))
4947, 48e1a 38672 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ▶   (𝜓𝜒)   )
50 con3 149 . . . . . . 7 ((𝜓𝜒) → (¬ 𝜒 → ¬ 𝜓))
5150com12 32 . . . . . 6 𝜒 → ((𝜓𝜒) → ¬ 𝜓))
5231, 49, 51e21 38777 . . . . 5 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜓   )
53 19.8a 2050 . . . . 5 𝜓 → ∃𝑥 ¬ 𝜓)
5452, 53e2 38676 . . . 4 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶   𝑥 ¬ 𝜓   )
55 hbe1 2019 . . . 4 (∃𝑥 ¬ 𝜓 → ∀𝑥𝑥 ¬ 𝜓)
5630, 54, 24, 55exinst11 38671 . . 3 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜓   )
57 exnal 1752 . . . 4 (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
5857biimpi 206 . . 3 (∃𝑥 ¬ 𝜓 → ¬ ∀𝑥𝜓)
5956, 58e1a 38672 . 2 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜓   )
6059in1 38607 1 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384  wal 1479  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-10 2017  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1703  df-nf 1708  df-vd1 38606  df-vd2 38614
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator