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

Theorem vk15.4j 39259
Description: Excercise 4j of Unit 15 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. This proof is the minimized Hilbert-style axiomatic version of the Fitch-style Natural Deduction proof found on page 442 of Klenk and was automatically derived from that proof. vk15.4j 39259 is vk15.4jVD 39672 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
vk15.4j.1 ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
vk15.4j.2 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
vk15.4j.3 ¬ ∀𝑥(𝜏𝜑)
Assertion
Ref Expression
vk15.4j (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Proof of Theorem vk15.4j
StepHypRef Expression
1 vk15.4j.3 . . . . . 6 ¬ ∀𝑥(𝜏𝜑)
2 exanali 1937 . . . . . 6 (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏𝜑))
31, 2mpbir 221 . . . . 5 𝑥(𝜏 ∧ ¬ 𝜑)
4 vk15.4j.2 . . . . . 6 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
5 alex 1901 . . . . . . . . . 10 (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
65biimpri 218 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
7619.21bi 2213 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃𝜃)
8 simpl 468 . . . . . . . . 9 ((𝜏 ∧ ¬ 𝜑) → 𝜏)
98a1i 11 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → 𝜏))
10 19.8a 2206 . . . . . . . 8 ((𝜃𝜏) → ∃𝑥(𝜃𝜏))
117, 9, 10syl6an 663 . . . . . . 7 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥(𝜃𝜏)))
12 notnot 138 . . . . . . 7 (∃𝑥(𝜃𝜏) → ¬ ¬ ∃𝑥(𝜃𝜏))
1311, 12syl6 35 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ¬ ∃𝑥(𝜃𝜏)))
14 con3 150 . . . . . 6 ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏)) → (¬ ¬ ∃𝑥(𝜃𝜏) → ¬ ∀𝑥𝜒))
154, 13, 14mpsylsyld 69 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ∀𝑥𝜒))
16 hbe1 2176 . . . . . 6 (∃𝑥 ¬ 𝜃 → ∀𝑥𝑥 ¬ 𝜃)
1716hbn 2311 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
18 hbn1 2175 . . . . 5 (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
193, 15, 17, 18eexinst01 39257 . . . 4 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜒)
20 exnal 1902 . . . 4 (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
2119, 20sylibr 224 . . 3 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜒)
22 vk15.4j.1 . . . . . . . . 9 ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
23 pm3.13 979 . . . . . . . . 9 (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
2422, 23ax-mp 5 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
25 simpr 471 . . . . . . . . . . . 12 ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
2625a1i 11 . . . . . . . . . . 11 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑))
27 19.8a 2206 . . . . . . . . . . 11 𝜑 → ∃𝑥 ¬ 𝜑)
2826, 27syl6 35 . . . . . . . . . 10 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥 ¬ 𝜑))
29 hbe1 2176 . . . . . . . . . 10 (∃𝑥 ¬ 𝜑 → ∀𝑥𝑥 ¬ 𝜑)
303, 28, 17, 29eexinst01 39257 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜑)
31 notnot 138 . . . . . . . . 9 (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
3230, 31syl 17 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃 → ¬ ¬ ∃𝑥 ¬ 𝜑)
33 pm2.53 840 . . . . . . . 8 ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
3424, 32, 33mpsyl 68 . . . . . . 7 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35 exanali 1937 . . . . . . . 8 (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓𝜒))
3635con5i 39254 . . . . . . 7 (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓𝜒))
3734, 36syl 17 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥(𝜓𝜒))
383719.21bi 2213 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → (𝜓𝜒))
3938con3d 149 . . . 4 (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ¬ 𝜓))
40 19.8a 2206 . . . 4 𝜓 → ∃𝑥 ¬ 𝜓)
4139, 40syl6 35 . . 3 (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ∃𝑥 ¬ 𝜓))
42 hbe1 2176 . . 3 (∃𝑥 ¬ 𝜓 → ∀𝑥𝑥 ¬ 𝜓)
4321, 41, 17, 42eexinst11 39258 . 2 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜓)
44 exnal 1902 . 2 (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
4543, 44sylib 208 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
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator