Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  vk15.4jVD Structured version   Unicode version

Theorem vk15.4jVD 34115
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 33685 is vk15.4jVD 34115 without virtual deductions and was automatically derived from vk15.4jVD 34115. 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.)
Hypotheses
Ref Expression
vk15.4jVD.1  |-  -.  ( E. x  -.  ph  /\  E. x ( ps  /\  -.  ch ) )
vk15.4jVD.2  |-  ( A. x ch  ->  -.  E. x ( th  /\  ta ) )
vk15.4jVD.3  |-  -.  A. x ( ta  ->  ph )
Assertion
Ref Expression
vk15.4jVD  |-  ( -. 
E. x  -.  th  ->  -.  A. x ps )

Proof of Theorem vk15.4jVD
StepHypRef Expression
1 vk15.4jVD.3 . . . . . . 7  |-  -.  A. x ( ta  ->  ph )
2 exanali 1675 . . . . . . . 8  |-  ( E. x ( ta  /\  -.  ph )  <->  -.  A. x
( ta  ->  ph )
)
32biimpri 206 . . . . . . 7  |-  ( -. 
A. x ( ta 
->  ph )  ->  E. x
( ta  /\  -.  ph ) )
41, 3e0a 33963 . . . . . 6  |-  E. x
( ta  /\  -.  ph )
5 vk15.4jVD.2 . . . . . . 7  |-  ( A. x ch  ->  -.  E. x ( th  /\  ta ) )
6 idn1 33745 . . . . . . . . . . . 12  |-  (.  -.  E. x  -.  th  ->.  -.  E. x  -.  th ).
7 alex 1652 . . . . . . . . . . . . 13  |-  ( A. x th  <->  -.  E. x  -.  th )
87biimpri 206 . . . . . . . . . . . 12  |-  ( -. 
E. x  -.  th  ->  A. x th )
96, 8e1a 33807 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th  ->.  A. x th ).
10 sp 1864 . . . . . . . . . . 11  |-  ( A. x th  ->  th )
119, 10e1a 33807 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th  ->.  th ).
12 idn2 33793 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ( ta  /\  -.  ph ) ).
13 simpl 455 . . . . . . . . . . 11  |-  ( ( ta  /\  -.  ph )  ->  ta )
1412, 13e2 33811 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ta ).
15 pm3.2 445 . . . . . . . . . 10  |-  ( th 
->  ( ta  ->  ( th  /\  ta ) ) )
1611, 14, 15e12 33915 . . . . . . . . 9  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ( th  /\  ta ) ).
17 19.8a 1862 . . . . . . . . 9  |-  ( ( th  /\  ta )  ->  E. x ( th 
/\  ta ) )
1816, 17e2 33811 . . . . . . . 8  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  E. x ( th 
/\  ta ) ).
19 notnot1 122 . . . . . . . 8  |-  ( E. x ( th  /\  ta )  ->  -.  -.  E. x ( th  /\  ta ) )
2018, 19e2 33811 . . . . . . 7  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  -.  E. x
( th  /\  ta ) ).
21 con3 134 . . . . . . 7  |-  ( ( A. x ch  ->  -. 
E. x ( th 
/\  ta ) )  -> 
( -.  -.  E. x ( th  /\  ta )  ->  -.  A. x ch ) )
225, 20, 21e02 33877 . . . . . 6  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  A. x ch
).
23 hbe1 1844 . . . . . . 7  |-  ( E. x  -.  th  ->  A. x E. x  -.  th )
2423hbn 1900 . . . . . 6  |-  ( -. 
E. x  -.  th  ->  A. x  -.  E. x  -.  th )
25 hba1 1901 . . . . . . 7  |-  ( A. x ch  ->  A. x A. x ch )
2625hbn 1900 . . . . . 6  |-  ( -. 
A. x ch  ->  A. x  -.  A. x ch )
274, 22, 24, 26exinst01 33805 . . . . 5  |-  (.  -.  E. x  -.  th  ->.  -.  A. x ch ).
28 exnal 1653 . . . . . 6  |-  ( E. x  -.  ch  <->  -.  A. x ch )
2928biimpri 206 . . . . 5  |-  ( -. 
A. x ch  ->  E. x  -.  ch )
3027, 29e1a 33807 . . . 4  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ch ).
31 idn2 33793 . . . . . 6  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  -.  ch ).
32 vk15.4jVD.1 . . . . . . . . . 10  |-  -.  ( E. x  -.  ph  /\  E. x ( ps  /\  -.  ch ) )
33 pm3.13 499 . . . . . . . . . 10  |-  ( -.  ( E. x  -.  ph 
/\  E. x ( ps 
/\  -.  ch )
)  ->  ( -.  E. x  -.  ph  \/  -.  E. x ( ps 
/\  -.  ch )
) )
3432, 33e0a 33963 . . . . . . . . 9  |-  ( -. 
E. x  -.  ph  \/  -.  E. x ( ps  /\  -.  ch ) )
35 simpr 459 . . . . . . . . . . . . 13  |-  ( ( ta  /\  -.  ph )  ->  -.  ph )
3612, 35e2 33811 . . . . . . . . . . . 12  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  ph ).
37 19.8a 1862 . . . . . . . . . . . 12  |-  ( -. 
ph  ->  E. x  -.  ph )
3836, 37e2 33811 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  E. x  -.  ph ).
39 hbe1 1844 . . . . . . . . . . 11  |-  ( E. x  -.  ph  ->  A. x E. x  -.  ph )
404, 38, 24, 39exinst01 33805 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ph ).
41 notnot1 122 . . . . . . . . . 10  |-  ( E. x  -.  ph  ->  -. 
-.  E. x  -.  ph )
4240, 41e1a 33807 . . . . . . . . 9  |-  (.  -.  E. x  -.  th  ->.  -.  -.  E. x  -.  ph ).
43 pm2.53 371 . . . . . . . . 9  |-  ( ( -.  E. x  -.  ph  \/  -.  E. x
( ps  /\  -.  ch ) )  ->  ( -.  -.  E. x  -.  ph 
->  -.  E. x ( ps  /\  -.  ch ) ) )
4434, 42, 43e01 33871 . . . . . . . 8  |-  (.  -.  E. x  -.  th  ->.  -.  E. x
( ps  /\  -.  ch ) ).
45 exanali 1675 . . . . . . . . 9  |-  ( E. x ( ps  /\  -.  ch )  <->  -.  A. x
( ps  ->  ch ) )
4645con5i 33680 . . . . . . . 8  |-  ( -. 
E. x ( ps 
/\  -.  ch )  ->  A. x ( ps 
->  ch ) )
4744, 46e1a 33807 . . . . . . 7  |-  (.  -.  E. x  -.  th  ->.  A. x
( ps  ->  ch ) ).
48 sp 1864 . . . . . . 7  |-  ( A. x ( ps  ->  ch )  ->  ( ps  ->  ch ) )
4947, 48e1a 33807 . . . . . 6  |-  (.  -.  E. x  -.  th  ->.  ( ps  ->  ch ) ).
50 con3 134 . . . . . . 7  |-  ( ( ps  ->  ch )  ->  ( -.  ch  ->  -. 
ps ) )
5150com12 31 . . . . . 6  |-  ( -. 
ch  ->  ( ( ps 
->  ch )  ->  -.  ps ) )
5231, 49, 51e21 33921 . . . . 5  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  -.  ps ).
53 19.8a 1862 . . . . 5  |-  ( -. 
ps  ->  E. x  -.  ps )
5452, 53e2 33811 . . . 4  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  E. x  -.  ps ).
55 hbe1 1844 . . . 4  |-  ( E. x  -.  ps  ->  A. x E. x  -.  ps )
5630, 54, 24, 55exinst11 33806 . . 3  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ps ).
57 exnal 1653 . . . 4  |-  ( E. x  -.  ps  <->  -.  A. x ps )
5857biimpi 194 . . 3  |-  ( E. x  -.  ps  ->  -. 
A. x ps )
5956, 58e1a 33807 . 2  |-  (.  -.  E. x  -.  th  ->.  -.  A. x ps ).
6059in1 33742 1  |-  ( -. 
E. x  -.  th  ->  -.  A. x ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 366    /\ wa 367   A.wal 1396   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1618  df-nf 1622  df-vd1 33741  df-vd2 33749
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator