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 39430
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 39430 is vk15.4jVD 39826 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 1955 . . . . . 6 (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏𝜑))
31, 2mpbir 222 . . . . 5 𝑥(𝜏 ∧ ¬ 𝜑)
4 vk15.4j.2 . . . . . 6 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
5 alex 1920 . . . . . . . . . 10 (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
65biimpri 219 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
7619.21bi 2221 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃𝜃)
8 simpl 474 . . . . . . . . 9 ((𝜏 ∧ ¬ 𝜑) → 𝜏)
98a1i 11 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → 𝜏))
10 19.8a 2214 . . . . . . . 8 ((𝜃𝜏) → ∃𝑥(𝜃𝜏))
117, 9, 10syl6an 674 . . . . . . 7 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥(𝜃𝜏)))
12 notnot 138 . . . . . . 7 (∃𝑥(𝜃𝜏) → ¬ ¬ ∃𝑥(𝜃𝜏))
1311, 12syl6 35 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ¬ ∃𝑥(𝜃𝜏)))
14 con3 150 . . . . . 6 ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏)) → (¬ ¬ ∃𝑥(𝜃𝜏) → ¬ ∀𝑥𝜒))
154, 13, 14mpsylsyld 69 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ∀𝑥𝜒))
16 hbe1 2185 . . . . . 6 (∃𝑥 ¬ 𝜃 → ∀𝑥𝑥 ¬ 𝜃)
1716hbn 2321 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
18 hbn1 2184 . . . . 5 (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
193, 15, 17, 18eexinst01 39428 . . . 4 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜒)
20 exnal 1921 . . . 4 (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
2119, 20sylibr 225 . . 3 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜒)
22 vk15.4j.1 . . . . . . . . 9 ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
23 pm3.13 1017 . . . . . . . . 9 (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
2422, 23ax-mp 5 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
25 simpr 477 . . . . . . . . . . . 12 ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
2625a1i 11 . . . . . . . . . . 11 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑))
27 19.8a 2214 . . . . . . . . . . 11 𝜑 → ∃𝑥 ¬ 𝜑)
2826, 27syl6 35 . . . . . . . . . 10 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥 ¬ 𝜑))
29 hbe1 2185 . . . . . . . . . 10 (∃𝑥 ¬ 𝜑 → ∀𝑥𝑥 ¬ 𝜑)
303, 28, 17, 29eexinst01 39428 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜑)
31 notnot 138 . . . . . . . . 9 (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
3230, 31syl 17 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃 → ¬ ¬ ∃𝑥 ¬ 𝜑)
33 pm2.53 877 . . . . . . . 8 ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
3424, 32, 33mpsyl 68 . . . . . . 7 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35 exanali 1955 . . . . . . . 8 (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓𝜒))
3635con5i 39425 . . . . . . 7 (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓𝜒))
3734, 36syl 17 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥(𝜓𝜒))
383719.21bi 2221 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → (𝜓𝜒))
3938con3d 149 . . . 4 (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ¬ 𝜓))
40 19.8a 2214 . . . 4 𝜓 → ∃𝑥 ¬ 𝜓)
4139, 40syl6 35 . . 3 (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ∃𝑥 ¬ 𝜓))
42 hbe1 2185 . . 3 (∃𝑥 ¬ 𝜓 → ∀𝑥𝑥 ¬ 𝜓)
4321, 41, 17, 42eexinst11 39429 . 2 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜓)
44 exnal 1921 . 2 (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
4543, 44sylib 209 1 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wo 873  wal 1650  wex 1874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-10 2183  ax-12 2211
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-ex 1875  df-nf 1879
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator