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 38554
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 38554 is vk15.4jVD 38970 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 1784 . . . . . 6 (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏𝜑))
31, 2mpbir 221 . . . . 5 𝑥(𝜏 ∧ ¬ 𝜑)
4 vk15.4j.2 . . . . . 6 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
5 alex 1751 . . . . . . . . . 10 (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
65biimpri 218 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
7619.21bi 2057 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃𝜃)
8 simpl 473 . . . . . . . . 9 ((𝜏 ∧ ¬ 𝜑) → 𝜏)
98a1i 11 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → 𝜏))
10 19.8a 2050 . . . . . . . 8 ((𝜃𝜏) → ∃𝑥(𝜃𝜏))
117, 9, 10syl6an 567 . . . . . . 7 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥(𝜃𝜏)))
12 notnot 136 . . . . . . 7 (∃𝑥(𝜃𝜏) → ¬ ¬ ∃𝑥(𝜃𝜏))
1311, 12syl6 35 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ¬ ∃𝑥(𝜃𝜏)))
14 con3 149 . . . . . 6 ((∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏)) → (¬ ¬ ∃𝑥(𝜃𝜏) → ¬ ∀𝑥𝜒))
154, 13, 14mpsylsyld 69 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ ∀𝑥𝜒))
16 hbe1 2019 . . . . . 6 (∃𝑥 ¬ 𝜃 → ∀𝑥𝑥 ¬ 𝜃)
1716hbn 2144 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
18 hbn1 2018 . . . . 5 (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
193, 15, 17, 18eexinst01 38552 . . . 4 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜒)
20 exnal 1752 . . . 4 (∃𝑥 ¬ 𝜒 ↔ ¬ ∀𝑥𝜒)
2119, 20sylibr 224 . . 3 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜒)
22 vk15.4j.1 . . . . . . . . 9 ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
23 pm3.13 522 . . . . . . . . 9 (¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
2422, 23ax-mp 5 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
25 simpr 477 . . . . . . . . . . . 12 ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑)
2625a1i 11 . . . . . . . . . . 11 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ¬ 𝜑))
27 19.8a 2050 . . . . . . . . . . 11 𝜑 → ∃𝑥 ¬ 𝜑)
2826, 27syl6 35 . . . . . . . . . 10 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥 ¬ 𝜑))
29 hbe1 2019 . . . . . . . . . 10 (∃𝑥 ¬ 𝜑 → ∀𝑥𝑥 ¬ 𝜑)
303, 28, 17, 29eexinst01 38552 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜑)
31 notnot 136 . . . . . . . . 9 (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
3230, 31syl 17 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃 → ¬ ¬ ∃𝑥 ¬ 𝜑)
33 pm2.53 388 . . . . . . . 8 ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
3424, 32, 33mpsyl 68 . . . . . . 7 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35 exanali 1784 . . . . . . . 8 (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓𝜒))
3635con5i 38549 . . . . . . 7 (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓𝜒))
3734, 36syl 17 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥(𝜓𝜒))
383719.21bi 2057 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → (𝜓𝜒))
3938con3d 148 . . . 4 (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ¬ 𝜓))
40 19.8a 2050 . . . 4 𝜓 → ∃𝑥 ¬ 𝜓)
4139, 40syl6 35 . . 3 (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ∃𝑥 ¬ 𝜓))
42 hbe1 2019 . . 3 (∃𝑥 ¬ 𝜓 → ∀𝑥𝑥 ¬ 𝜓)
4321, 41, 17, 42eexinst11 38553 . 2 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜓)
44 exnal 1752 . 2 (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
4543, 44sylib 208 1 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384  wal 1479  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-10 2017  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1703  df-nf 1708
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator