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 44109
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 44109 is vk15.4jVD 44495 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 1854 . . . . . 6 (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏𝜑))
31, 2mpbir 230 . . . . 5 𝑥(𝜏 ∧ ¬ 𝜑)
4 vk15.4j.2 . . . . . 6 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
5 alex 1820 . . . . . . . . . 10 (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
65biimpri 227 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
7619.21bi 2177 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃𝜃)
8 simpl 481 . . . . . . . . 9 ((𝜏 ∧ ¬ 𝜑) → 𝜏)
98a1i 11 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → 𝜏))
10 19.8a 2169 . . . . . . . 8 ((𝜃𝜏) → ∃𝑥(𝜃𝜏))
117, 9, 10syl6an 682 . . . . . . 7 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥(𝜃𝜏)))
12 notnot 142 . . . . . . 7 (∃𝑥(𝜃𝜏) → ¬ ¬ ∃𝑥(𝜃𝜏))
1311, 12syl6 35 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ¬ ∃𝑥(𝜃𝜏)))
14 con3 153 . . . . . 6 ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏)) → (¬ ¬ ∃𝑥(𝜃𝜏) → ¬ ∀𝑥𝜒))
154, 13, 14mpsylsyld 69 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ∀𝑥𝜒))
16 hbe1 2131 . . . . . 6 (∃𝑥 ¬ 𝜃 → ∀𝑥𝑥 ¬ 𝜃)
1716hbn 2284 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
18 hbn1 2130 . . . . 5 (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
193, 15, 17, 18eexinst01 44107 . . . 4 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜒)
20 exnal 1821 . . . 4 (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
2119, 20sylibr 233 . . 3 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜒)
22 vk15.4j.1 . . . . . . . . 9 ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
23 pm3.13 992 . . . . . . . . 9 (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
2422, 23ax-mp 5 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
25 simpr 483 . . . . . . . . . . . 12 ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
2625a1i 11 . . . . . . . . . . 11 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑))
27 19.8a 2169 . . . . . . . . . . 11 𝜑 → ∃𝑥 ¬ 𝜑)
2826, 27syl6 35 . . . . . . . . . 10 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥 ¬ 𝜑))
29 hbe1 2131 . . . . . . . . . 10 (∃𝑥 ¬ 𝜑 → ∀𝑥𝑥 ¬ 𝜑)
303, 28, 17, 29eexinst01 44107 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜑)
31 notnot 142 . . . . . . . . 9 (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
3230, 31syl 17 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃 → ¬ ¬ ∃𝑥 ¬ 𝜑)
33 pm2.53 849 . . . . . . . 8 ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
3424, 32, 33mpsyl 68 . . . . . . 7 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35 exanali 1854 . . . . . . . 8 (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓𝜒))
3635con5i 44104 . . . . . . 7 (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓𝜒))
3734, 36syl 17 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥(𝜓𝜒))
383719.21bi 2177 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → (𝜓𝜒))
3938con3d 152 . . . 4 (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ¬ 𝜓))
40 19.8a 2169 . . . 4 𝜓 → ∃𝑥 ¬ 𝜓)
4139, 40syl6 35 . . 3 (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ∃𝑥 ¬ 𝜓))
42 hbe1 2131 . . 3 (∃𝑥 ¬ 𝜓 → ∀𝑥𝑥 ¬ 𝜓)
4321, 41, 17, 42eexinst11 44108 . 2 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜓)
44 exnal 1821 . 2 (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
4543, 44sylib 217 1 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wo 845  wal 1531  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator