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 38630
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 38213 is vk15.4jVD 38630 without virtual deductions and was automatically derived from vk15.4jVD 38630. 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 1783 . . . . . . . 8 (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏𝜑))
32biimpri 218 . . . . . . 7 (¬ ∀𝑥(𝜏𝜑) → ∃𝑥(𝜏 ∧ ¬ 𝜑))
41, 3e0a 38478 . . . . . 6 𝑥(𝜏 ∧ ¬ 𝜑)
5 vk15.4jVD.2 . . . . . . 7 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
6 idn1 38269 . . . . . . . . . . . 12 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥 ¬ 𝜃   )
7 alex 1750 . . . . . . . . . . . . 13 (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
87biimpri 218 . . . . . . . . . . . 12 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
96, 8e1a 38331 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥𝜃   )
10 sp 2051 . . . . . . . . . . 11 (∀𝑥𝜃𝜃)
119, 10e1a 38331 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝜃   )
12 idn2 38317 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
13 simpl 473 . . . . . . . . . . 11 ((𝜏 ∧ ¬ 𝜑) → 𝜏)
1412, 13e2 38335 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
15 pm3.2 463 . . . . . . . . . 10 (𝜃 → (𝜏 → (𝜃𝜏)))
1611, 14, 15e12 38430 . . . . . . . . 9 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃𝜏)   )
17 19.8a 2049 . . . . . . . . 9 ((𝜃𝜏) → ∃𝑥(𝜃𝜏))
1816, 17e2 38335 . . . . . . . 8 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝑥(𝜃𝜏)   )
19 notnot 136 . . . . . . . 8 (∃𝑥(𝜃𝜏) → ¬ ¬ ∃𝑥(𝜃𝜏))
2018, 19e2 38335 . . . . . . 7 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ¬ ∃𝑥(𝜃𝜏)   )
21 con3 149 . . . . . . 7 ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏)) → (¬ ¬ ∃𝑥(𝜃𝜏) → ¬ ∀𝑥𝜒))
225, 20, 21e02 38401 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ∀𝑥𝜒   )
23 hbe1 2018 . . . . . . 7 (∃𝑥 ¬ 𝜃 → ∀𝑥𝑥 ¬ 𝜃)
2423hbn 2142 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
25 hba1 2148 . . . . . . 7 (∀𝑥𝜒 → ∀𝑥𝑥𝜒)
2625hbn 2142 . . . . . 6 (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
274, 22, 24, 26exinst01 38329 . . . . 5 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜒   )
28 exnal 1751 . . . . . 6 (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
2928biimpri 218 . . . . 5 (¬ ∀𝑥𝜒 → ∃𝑥 ¬ 𝜒)
3027, 29e1a 38331 . . . 4 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜒   )
31 idn2 38317 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜒   )
32 vk15.4jVD.1 . . . . . . . . . 10 ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
33 pm3.13 522 . . . . . . . . . 10 (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
3432, 33e0a 38478 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35 simpr 477 . . . . . . . . . . . . 13 ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
3612, 35e2 38335 . . . . . . . . . . . 12 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ 𝜑   )
37 19.8a 2049 . . . . . . . . . . . 12 𝜑 → ∃𝑥 ¬ 𝜑)
3836, 37e2 38335 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝑥 ¬ 𝜑   )
39 hbe1 2018 . . . . . . . . . . 11 (∃𝑥 ¬ 𝜑 → ∀𝑥𝑥 ¬ 𝜑)
404, 38, 24, 39exinst01 38329 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜑   )
41 notnot 136 . . . . . . . . . 10 (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
4240, 41e1a 38331 . . . . . . . . 9 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ¬ ∃𝑥 ¬ 𝜑   )
43 pm2.53 388 . . . . . . . . 9 ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
4434, 42, 43e01 38395 . . . . . . . 8 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)   )
45 exanali 1783 . . . . . . . . 9 (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓𝜒))
4645con5i 38208 . . . . . . . 8 (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓𝜒))
4744, 46e1a 38331 . . . . . . 7 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥(𝜓𝜒)   )
48 sp 2051 . . . . . . 7 (∀𝑥(𝜓𝜒) → (𝜓𝜒))
4947, 48e1a 38331 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ▶   (𝜓𝜒)   )
50 con3 149 . . . . . . 7 ((𝜓𝜒) → (¬ 𝜒 → ¬ 𝜓))
5150com12 32 . . . . . 6 𝜒 → ((𝜓𝜒) → ¬ 𝜓))
5231, 49, 51e21 38436 . . . . 5 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜓   )
53 19.8a 2049 . . . . 5 𝜓 → ∃𝑥 ¬ 𝜓)
5452, 53e2 38335 . . . 4 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶   𝑥 ¬ 𝜓   )
55 hbe1 2018 . . . 4 (∃𝑥 ¬ 𝜓 → ∀𝑥𝑥 ¬ 𝜓)
5630, 54, 24, 55exinst11 38330 . . 3 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜓   )
57 exnal 1751 . . . 4 (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
5857biimpi 206 . . 3 (∃𝑥 ¬ 𝜓 → ¬ ∀𝑥𝜓)
5956, 58e1a 38331 . 2 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜓   )
6059in1 38266 1 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-vd1 38265  df-vd2 38273
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator