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 38255
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 38255 is vk15.4jVD 38672 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 1783 . . . . . 6 (∃𝑥(𝜏 ∧ ¬ 𝜑) ↔ ¬ ∀𝑥(𝜏𝜑))
31, 2mpbir 221 . . . . 5 𝑥(𝜏 ∧ ¬ 𝜑)
4 vk15.4j.2 . . . . . 6 (∀𝑥𝜒 → ¬ ∃𝑥(𝜃𝜏))
5 alex 1750 . . . . . . . . . 10 (∀𝑥𝜃 ↔ ¬ ∃𝑥 ¬ 𝜃)
65biimpri 218 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥𝜃)
7619.21bi 2057 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃𝜃)
8 simpl 473 . . . . . . . . 9 ((𝜏 ∧ ¬ 𝜑) → 𝜏)
98a1i 11 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → 𝜏))
10 19.8a 2049 . . . . . . . 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 2018 . . . . . 6 (∃𝑥 ¬ 𝜃 → ∀𝑥𝑥 ¬ 𝜃)
1716hbn 2142 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥 ¬ ∃𝑥 ¬ 𝜃)
18 hbn1 2017 . . . . 5 (¬ ∀𝑥𝜒 → ∀𝑥 ¬ ∀𝑥𝜒)
193, 15, 17, 18eexinst01 38253 . . . 4 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜒)
20 exnal 1751 . . . 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 2049 . . . . . . . . . . 11 𝜑 → ∃𝑥 ¬ 𝜑)
2826, 27syl6 35 . . . . . . . . . 10 (¬ ∃𝑥 ¬ 𝜃 → ((𝜏 ∧ ¬ 𝜑) → ∃𝑥 ¬ 𝜑))
29 hbe1 2018 . . . . . . . . . 10 (∃𝑥 ¬ 𝜑 → ∀𝑥𝑥 ¬ 𝜑)
303, 28, 17, 29eexinst01 38253 . . . . . . . . 9 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜑)
31 notnot 136 . . . . . . . . 9 (∃𝑥 ¬ 𝜑 → ¬ ¬ ∃𝑥 ¬ 𝜑)
3230, 31syl 17 . . . . . . . 8 (¬ ∃𝑥 ¬ 𝜃 → ¬ ¬ ∃𝑥 ¬ 𝜑)
33 pm2.53 388 . . . . . . . 8 ((¬ ∃𝑥 ¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)) → (¬ ¬ ∃𝑥 ¬ 𝜑 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒)))
3424, 32, 33mpsyl 68 . . . . . . 7 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
35 exanali 1783 . . . . . . . 8 (∃𝑥(𝜓 ∧ ¬ 𝜒) ↔ ¬ ∀𝑥(𝜓𝜒))
3635con5i 38250 . . . . . . 7 (¬ ∃𝑥(𝜓 ∧ ¬ 𝜒) → ∀𝑥(𝜓𝜒))
3734, 36syl 17 . . . . . 6 (¬ ∃𝑥 ¬ 𝜃 → ∀𝑥(𝜓𝜒))
383719.21bi 2057 . . . . 5 (¬ ∃𝑥 ¬ 𝜃 → (𝜓𝜒))
3938con3d 148 . . . 4 (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ¬ 𝜓))
40 19.8a 2049 . . . 4 𝜓 → ∃𝑥 ¬ 𝜓)
4139, 40syl6 35 . . 3 (¬ ∃𝑥 ¬ 𝜃 → (¬ 𝜒 → ∃𝑥 ¬ 𝜓))
42 hbe1 2018 . . 3 (∃𝑥 ¬ 𝜓 → ∀𝑥𝑥 ¬ 𝜓)
4321, 41, 17, 42eexinst11 38254 . 2 (¬ ∃𝑥 ¬ 𝜃 → ∃𝑥 ¬ 𝜓)
44 exnal 1751 . 2 (∃𝑥 ¬ 𝜓 ↔ ¬ ∀𝑥𝜓)
4543, 44sylib 208 1 (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator