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 43288
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 42902 is vk15.4jVD 43288 without virtual deductions and was automatically derived from vk15.4jVD 43288. 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 43146 . . . . . 6 𝑥(𝜏 ∧ ¬ 𝜑)
5 vk15.4jVD.2 . . . . . . 7 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
6 idn1 42948 . . . . . . . . . . . 12 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥 ¬ 𝜃   )
7 alex 1829 . . . . . . . . . . . . 13 (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
87biimpri 227 . . . . . . . . . . . 12 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
96, 8e1a 43001 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥𝜃   )
10 sp 2177 . . . . . . . . . . 11 (∀𝑥𝜃𝜃)
119, 10e1a 43001 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝜃   )
12 idn2 42987 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
13 simpl 484 . . . . . . . . . . 11 ((𝜏 ∧ ¬ 𝜑) → 𝜏)
1412, 13e2 43005 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
15 pm3.2 471 . . . . . . . . . 10 (𝜃 → (𝜏 → (𝜃𝜏)))
1611, 14, 15e12 43098 . . . . . . . . 9 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃𝜏)   )
17 19.8a 2175 . . . . . . . . 9 ((𝜃𝜏) → ∃𝑥(𝜃𝜏))
1816, 17e2 43005 . . . . . . . 8 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝑥(𝜃𝜏)   )
19 notnot 142 . . . . . . . 8 (∃𝑥(𝜃𝜏) → ¬ ¬ ∃𝑥(𝜃𝜏))
2018, 19e2 43005 . . . . . . 7 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ¬ ∃𝑥(𝜃𝜏)   )
21 con3 153 . . . . . . 7 ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏)) → (¬ ¬ ∃𝑥(𝜃𝜏) → ¬ ∀𝑥𝜒))
225, 20, 21e02 43071 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ ∀𝑥𝜒   )
23 hbe1 2140 . . . . . . 7 (∃𝑥 ¬ 𝜃 → ∀𝑥𝑥 ¬ 𝜃)
2423hbn 2292 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
25 hba1 2290 . . . . . . 7 (∀𝑥𝜒 → ∀𝑥𝑥𝜒)
2625hbn 2292 . . . . . 6 (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
274, 22, 24, 26exinst01 42999 . . . . 5 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜒   )
28 exnal 1830 . . . . . 6 (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
2928biimpri 227 . . . . 5 (¬ ∀𝑥𝜒 → ∃𝑥 ¬ 𝜒)
3027, 29e1a 43001 . . . 4 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜒   )
31 idn2 42987 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜒   )
32 vk15.4jVD.1 . . . . . . . . . 10 ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
33 pm3.13 994 . . . . . . . . . 10 (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
3432, 33e0a 43146 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35 simpr 486 . . . . . . . . . . . . 13 ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
3612, 35e2 43005 . . . . . . . . . . . 12 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶    ¬ 𝜑   )
37 19.8a 2175 . . . . . . . . . . . 12 𝜑 → ∃𝑥 ¬ 𝜑)
3836, 37e2 43005 . . . . . . . . . . 11 (    ¬ ∃𝑥 ¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝑥 ¬ 𝜑   )
39 hbe1 2140 . . . . . . . . . . 11 (∃𝑥 ¬ 𝜑 → ∀𝑥𝑥 ¬ 𝜑)
404, 38, 24, 39exinst01 42999 . . . . . . . . . 10 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜑   )
41 notnot 142 . . . . . . . . . 10 (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
4240, 41e1a 43001 . . . . . . . . 9 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ¬ ∃𝑥 ¬ 𝜑   )
43 pm2.53 850 . . . . . . . . 9 ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
4434, 42, 43e01 43065 . . . . . . . 8 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)   )
45 exanali 1863 . . . . . . . . 9 (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓𝜒))
4645con5i 42897 . . . . . . . 8 (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓𝜒))
4744, 46e1a 43001 . . . . . . 7 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥(𝜓𝜒)   )
48 sp 2177 . . . . . . 7 (∀𝑥(𝜓𝜒) → (𝜓𝜒))
4947, 48e1a 43001 . . . . . 6 (    ¬ ∃𝑥 ¬ 𝜃   ▶   (𝜓𝜒)   )
50 con3 153 . . . . . . 7 ((𝜓𝜒) → (¬ 𝜒 → ¬ 𝜓))
5150com12 32 . . . . . 6 𝜒 → ((𝜓𝜒) → ¬ 𝜓))
5231, 49, 51e21 43104 . . . . 5 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶    ¬ 𝜓   )
53 19.8a 2175 . . . . 5 𝜓 → ∃𝑥 ¬ 𝜓)
5452, 53e2 43005 . . . 4 (    ¬ ∃𝑥 ¬ 𝜃   ,    ¬ 𝜒   ▶   𝑥 ¬ 𝜓   )
55 hbe1 2140 . . . 4 (∃𝑥 ¬ 𝜓 → ∀𝑥𝑥 ¬ 𝜓)
5630, 54, 24, 55exinst11 43000 . . 3 (    ¬ ∃𝑥 ¬ 𝜃   ▶   𝑥 ¬ 𝜓   )
57 exnal 1830 . . . 4 (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
5857biimpi 215 . . 3 (∃𝑥 ¬ 𝜓 → ¬ ∀𝑥𝜓)
5956, 58e1a 43001 . 2 (    ¬ ∃𝑥 ¬ 𝜃   ▶    ¬ ∀𝑥𝜓   )
6059in1 42945 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 42944  df-vd2 42952
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator