This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vk15.4j

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 is vk15.4jVD automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vk15.4j.1 ⊢ ¬ ( ∃ 𝑥 ¬ 𝜑 ∧ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) )
vk15.4j.2 ⊢ ( ∀ 𝑥 𝜒 → ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
vk15.4j.3 ⊢ ¬ ∀ 𝑥 ( 𝜏 → 𝜑 )
Assertion vk15.4j ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ∀ 𝑥 𝜓 )

Proof

Step Hyp Ref Expression
1 vk15.4j.1 ⊢ ¬ ( ∃ 𝑥 ¬ 𝜑 ∧ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) )
2 vk15.4j.2 ⊢ ( ∀ 𝑥 𝜒 → ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
3 vk15.4j.3 ⊢ ¬ ∀ 𝑥 ( 𝜏 → 𝜑 )
4 exanali ⊢ ( ∃ 𝑥 ( 𝜏 ∧ ¬ 𝜑 ) ↔ ¬ ∀ 𝑥 ( 𝜏 → 𝜑 ) )
5 3 4 mpbir ⊢ ∃ 𝑥 ( 𝜏 ∧ ¬ 𝜑 )
6 alex ⊢ ( ∀ 𝑥 𝜃 ↔ ¬ ∃ 𝑥 ¬ 𝜃 )
7 6 biimpri ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 𝜃 )
8 7 19.21bi ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → 𝜃 )
9 simpl ⊢ ( ( 𝜏 ∧ ¬ 𝜑 ) → 𝜏 )
10 9 a1i ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → 𝜏 ) )
11 19.8a ⊢ ( ( 𝜃 ∧ 𝜏 ) → ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
12 8 10 11 syl6an ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) ) )
13 notnot ⊢ ( ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) → ¬ ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
14 12 13 syl6 ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → ¬ ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) ) )
15 con3 ⊢ ( ( ∀ 𝑥 𝜒 → ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) ) → ( ¬ ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) → ¬ ∀ 𝑥 𝜒 ) )
16 2 14 15 mpsylsyld ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → ¬ ∀ 𝑥 𝜒 ) )
17 hbe1 ⊢ ( ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 ∃ 𝑥 ¬ 𝜃 )
18 17 hbn ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 ¬ ∃ 𝑥 ¬ 𝜃 )
19 hbn1 ⊢ ( ¬ ∀ 𝑥 𝜒 → ∀ 𝑥 ¬ ∀ 𝑥 𝜒 )
20 5 16 18 19 eexinst01 ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ∀ 𝑥 𝜒 )
21 exnal ⊢ ( ∃ 𝑥 ¬ 𝜒 ↔ ¬ ∀ 𝑥 𝜒 )
22 20 21 sylibr ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∃ 𝑥 ¬ 𝜒 )
23 pm3.13 ⊢ ( ¬ ( ∃ 𝑥 ¬ 𝜑 ∧ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ ∃ 𝑥 ¬ 𝜑 ∨ ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) )
24 1 23 ax-mp ⊢ ( ¬ ∃ 𝑥 ¬ 𝜑 ∨ ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) )
25 simpr ⊢ ( ( 𝜏 ∧ ¬ 𝜑 ) → ¬ 𝜑 )
26 25 a1i ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → ¬ 𝜑 ) )
27 19.8a ⊢ ( ¬ 𝜑 → ∃ 𝑥 ¬ 𝜑 )
28 26 27 syl6 ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ( 𝜏 ∧ ¬ 𝜑 ) → ∃ 𝑥 ¬ 𝜑 ) )
29 hbe1 ⊢ ( ∃ 𝑥 ¬ 𝜑 → ∀ 𝑥 ∃ 𝑥 ¬ 𝜑 )
30 5 28 18 29 eexinst01 ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∃ 𝑥 ¬ 𝜑 )
31 notnot ⊢ ( ∃ 𝑥 ¬ 𝜑 → ¬ ¬ ∃ 𝑥 ¬ 𝜑 )
32 30 31 syl ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ¬ ∃ 𝑥 ¬ 𝜑 )
33 pm2.53 ⊢ ( ( ¬ ∃ 𝑥 ¬ 𝜑 ∨ ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ ¬ ∃ 𝑥 ¬ 𝜑 → ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) )
34 24 32 33 mpsyl ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) )
35 exanali ⊢ ( ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ↔ ¬ ∀ 𝑥 ( 𝜓 → 𝜒 ) )
36 35 con5i ⊢ ( ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) → ∀ 𝑥 ( 𝜓 → 𝜒 ) )
37 34 36 syl ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 ( 𝜓 → 𝜒 ) )
38 37 19.21bi ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( 𝜓 → 𝜒 ) )
39 38 con3d ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ¬ 𝜒 → ¬ 𝜓 ) )
40 19.8a ⊢ ( ¬ 𝜓 → ∃ 𝑥 ¬ 𝜓 )
41 39 40 syl6 ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ( ¬ 𝜒 → ∃ 𝑥 ¬ 𝜓 ) )
42 hbe1 ⊢ ( ∃ 𝑥 ¬ 𝜓 → ∀ 𝑥 ∃ 𝑥 ¬ 𝜓 )
43 22 41 18 42 eexinst11 ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∃ 𝑥 ¬ 𝜓 )
44 exnal ⊢ ( ∃ 𝑥 ¬ 𝜓 ↔ ¬ ∀ 𝑥 𝜓 )
45 43 44 sylib ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ∀ 𝑥 𝜓 )