Metamath Proof Explorer

Theorem vk15.4jVD

Description: The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 15 Excercise 4.f. found in the "Answers to Starred Exercises" on page 442 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted to be a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. vk15.4j is vk15.4jVD without virtual deductions and was automatically derived from vk15.4jVD . Step numbers greater than 25 are additional steps necessary for the sequent calculus proof not contained in the Fitch-style proof. Otherwise, step i of the User's Proof corresponds to step i of the Fitch-style proof.

h1:: |- -. ( E. x -. ph /\ E. x ( ps /\ -. ch ) )
h2:: |- ( A. x ch -> -. E. x ( th /\ ta ) )
h3:: |- -. A. x ( ta -> ph )
4:: |- (. -. E. x -. th ->. -. E. x -. th ).
5:4: |- (. -. E. x -. th ->. A. x th ).
6:3: |- E. x ( ta /\ -. ph )
7:: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. ( ta /\ -. ph ) ).
8:7: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. ta ).
9:7: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. -. ph ).
10:5: |- (. -. E. x -. th ->. th ).
11:10,8: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. ( th /\ ta ) ).
12:11: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. E. x ( th /\ ta ) ).
13:12: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. -. -. E. x ( th /\ ta ) ).
14:2,13: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. -. A. x ch ).
140:: |- ( E. x -. th -> A. x E. x -. th )
141:140: |- ( -. E. x -. th -> A. x -. E. x -. th )
142:: |- ( A. x ch -> A. x A. x ch )
143:142: |- ( -. A. x ch -> A. x -. A. x ch )
144:6,14,141,143: |- (. -. E. x -. th ->. -. A. x ch ).
15:1: |- ( -. E. x -. ph \/ -. E. x ( ps /\ -. ch ) )
16:9: |- (. -. E. x -. th ,. ( ta /\ -. ph ) ->. E. x -. ph ).
161:: |- ( E. x -. ph -> A. x E. x -. ph )
162:6,16,141,161: |- (. -. E. x -. th ->. E. x -. ph ).
17:162: |- (. -. E. x -. th ->. -. -. E. x -. ph ).
18:15,17: |- (. -. E. x -. th ->. -. E. x ( ps /\ -. ch ) ).
19:18: |- (. -. E. x -. th ->. A. x ( ps -> ch ) ).
20:144: |- (. -. E. x -. th ->. E. x -. ch ).
21:: |- (. -. E. x -. th ,. -. ch ->. -. ch ).
22:19: |- (. -. E. x -. th ->. ( ps -> ch ) ).
23:21,22: |- (. -. E. x -. th ,. -. ch ->. -. ps ).
24:23: |- (. -. E. x -. th ,. -. ch ->. E. x -. ps ).
240:: |- ( E. x -. ps -> A. x E. x -. ps )
241:20,24,141,240: |- (. -. E. x -. th ->. E. x -. ps ).
25:241: |- (. -. E. x -. th ->. -. A. x ps ).
qed:25: |- ( -. E. x -. th -> -. A. x ps )
(Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 vk15.4jVD.1 ⊢ ¬ ( ∃ 𝑥 ¬ 𝜑 ∧ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) )
2 vk15.4jVD.2 ⊢ ( ∀ 𝑥 𝜒 → ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
3 vk15.4jVD.3 ⊢ ¬ ∀ 𝑥 ( 𝜏 → 𝜑 )
4 exanali ⊢ ( ∃ 𝑥 ( 𝜏 ∧ ¬ 𝜑 ) ↔ ¬ ∀ 𝑥 ( 𝜏 → 𝜑 ) )
5 4 biimpri ⊢ ( ¬ ∀ 𝑥 ( 𝜏 → 𝜑 ) → ∃ 𝑥 ( 𝜏 ∧ ¬ 𝜑 ) )
6 3 5 e0a ⊢ ∃ 𝑥 ( 𝜏 ∧ ¬ 𝜑 )
7 idn1 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ¬ ∃ 𝑥 ¬ 𝜃    )
8 alex ⊢ ( ∀ 𝑥 𝜃 ↔ ¬ ∃ 𝑥 ¬ 𝜃 )
9 8 biimpri ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 𝜃 )
10 7 9 e1a ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ∀ 𝑥 𝜃    )
11 sp ⊢ ( ∀ 𝑥 𝜃 → 𝜃 )
12 10 11 e1a ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    𝜃    )
13 idn2 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ( 𝜏 ∧ ¬ 𝜑 )    ▶    ( 𝜏 ∧ ¬ 𝜑 )    )
14 simpl ⊢ ( ( 𝜏 ∧ ¬ 𝜑 ) → 𝜏 )
15 13 14 e2 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ( 𝜏 ∧ ¬ 𝜑 )    ▶    𝜏    )
16 pm3.2 ⊢ ( 𝜃 → ( 𝜏 → ( 𝜃 ∧ 𝜏 ) ) )
17 12 15 16 e12 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ( 𝜏 ∧ ¬ 𝜑 )    ▶    ( 𝜃 ∧ 𝜏 )    )
18 19.8a ⊢ ( ( 𝜃 ∧ 𝜏 ) → ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
19 17 18 e2 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ( 𝜏 ∧ ¬ 𝜑 )    ▶    ∃ 𝑥 ( 𝜃 ∧ 𝜏 )    )
20 notnot ⊢ ( ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) → ¬ ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) )
21 19 20 e2 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ( 𝜏 ∧ ¬ 𝜑 )    ▶    ¬ ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 )    )
22 con3 ⊢ ( ( ∀ 𝑥 𝜒 → ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) ) → ( ¬ ¬ ∃ 𝑥 ( 𝜃 ∧ 𝜏 ) → ¬ ∀ 𝑥 𝜒 ) )
23 2 21 22 e02 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ( 𝜏 ∧ ¬ 𝜑 )    ▶    ¬ ∀ 𝑥 𝜒    )
24 hbe1 ⊢ ( ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 ∃ 𝑥 ¬ 𝜃 )
25 24 hbn ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ∀ 𝑥 ¬ ∃ 𝑥 ¬ 𝜃 )
26 hba1 ⊢ ( ∀ 𝑥 𝜒 → ∀ 𝑥 ∀ 𝑥 𝜒 )
27 26 hbn ⊢ ( ¬ ∀ 𝑥 𝜒 → ∀ 𝑥 ¬ ∀ 𝑥 𝜒 )
28 6 23 25 27 exinst01 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ¬ ∀ 𝑥 𝜒    )
29 exnal ⊢ ( ∃ 𝑥 ¬ 𝜒 ↔ ¬ ∀ 𝑥 𝜒 )
30 29 biimpri ⊢ ( ¬ ∀ 𝑥 𝜒 → ∃ 𝑥 ¬ 𝜒 )
31 28 30 e1a ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ∃ 𝑥 ¬ 𝜒    )
32 idn2 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ¬ 𝜒    ▶    ¬ 𝜒    )
33 pm3.13 ⊢ ( ¬ ( ∃ 𝑥 ¬ 𝜑 ∧ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ ∃ 𝑥 ¬ 𝜑 ∨ ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) )
34 1 33 e0a ⊢ ( ¬ ∃ 𝑥 ¬ 𝜑 ∨ ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) )
35 simpr ⊢ ( ( 𝜏 ∧ ¬ 𝜑 ) → ¬ 𝜑 )
36 13 35 e2 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ( 𝜏 ∧ ¬ 𝜑 )    ▶    ¬ 𝜑    )
37 19.8a ⊢ ( ¬ 𝜑 → ∃ 𝑥 ¬ 𝜑 )
38 36 37 e2 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ( 𝜏 ∧ ¬ 𝜑 )    ▶    ∃ 𝑥 ¬ 𝜑    )
39 hbe1 ⊢ ( ∃ 𝑥 ¬ 𝜑 → ∀ 𝑥 ∃ 𝑥 ¬ 𝜑 )
40 6 38 25 39 exinst01 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ∃ 𝑥 ¬ 𝜑    )
41 notnot ⊢ ( ∃ 𝑥 ¬ 𝜑 → ¬ ¬ ∃ 𝑥 ¬ 𝜑 )
42 40 41 e1a ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ¬ ¬ ∃ 𝑥 ¬ 𝜑    )
43 pm2.53 ⊢ ( ( ¬ ∃ 𝑥 ¬ 𝜑 ∨ ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) → ( ¬ ¬ ∃ 𝑥 ¬ 𝜑 → ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ) )
44 34 42 43 e01 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 )    )
45 exanali ⊢ ( ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) ↔ ¬ ∀ 𝑥 ( 𝜓 → 𝜒 ) )
46 45 con5i ⊢ ( ¬ ∃ 𝑥 ( 𝜓 ∧ ¬ 𝜒 ) → ∀ 𝑥 ( 𝜓 → 𝜒 ) )
47 44 46 e1a ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ∀ 𝑥 ( 𝜓 → 𝜒 )    )
48 sp ⊢ ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( 𝜓 → 𝜒 ) )
49 47 48 e1a ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ( 𝜓 → 𝜒 )    )
50 con3 ⊢ ( ( 𝜓 → 𝜒 ) → ( ¬ 𝜒 → ¬ 𝜓 ) )
51 50 com12 ⊢ ( ¬ 𝜒 → ( ( 𝜓 → 𝜒 ) → ¬ 𝜓 ) )
52 32 49 51 e21 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ¬ 𝜒    ▶    ¬ 𝜓    )
53 19.8a ⊢ ( ¬ 𝜓 → ∃ 𝑥 ¬ 𝜓 )
54 52 53 e2 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ,    ¬ 𝜒    ▶    ∃ 𝑥 ¬ 𝜓    )
55 hbe1 ⊢ ( ∃ 𝑥 ¬ 𝜓 → ∀ 𝑥 ∃ 𝑥 ¬ 𝜓 )
56 31 54 25 55 exinst11 ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ∃ 𝑥 ¬ 𝜓    )
57 exnal ⊢ ( ∃ 𝑥 ¬ 𝜓 ↔ ¬ ∀ 𝑥 𝜓 )
58 57 biimpi ⊢ ( ∃ 𝑥 ¬ 𝜓 → ¬ ∀ 𝑥 𝜓 )
59 56 58 e1a ⊢ (    ¬ ∃ 𝑥 ¬ 𝜃    ▶    ¬ ∀ 𝑥 𝜓    )
60 59 in1 ⊢ ( ¬ ∃ 𝑥 ¬ 𝜃 → ¬ ∀ 𝑥 𝜓 )