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 29100
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 O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. vk15.4j 28686 is vk15.4jVD 29100 without virtual deductions and was automatically derived from vk15.4jVD 29100. 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 1596 . . . . . . . 8  |-  ( E. x ( ta  /\  -.  ph )  <->  -.  A. x
( ta  ->  ph )
)
32biimpri 199 . . . . . . 7  |-  ( -. 
A. x ( ta 
->  ph )  ->  E. x
( ta  /\  -.  ph ) )
41, 3e0_ 28958 . . . . . 6  |-  E. x
( ta  /\  -.  ph )
5 vk15.4jVD.2 . . . . . . 7  |-  ( A. x ch  ->  -.  E. x ( th  /\  ta ) )
6 idn1 28739 . . . . . . . . . . . 12  |-  (.  -.  E. x  -.  th  ->.  -.  E. x  -.  th ).
7 alex 1582 . . . . . . . . . . . . 13  |-  ( A. x th  <->  -.  E. x  -.  th )
87biimpri 199 . . . . . . . . . . . 12  |-  ( -. 
E. x  -.  th  ->  A. x th )
96, 8e1_ 28802 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th  ->.  A. x th ).
10 sp 1764 . . . . . . . . . . 11  |-  ( A. x th  ->  th )
119, 10e1_ 28802 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th  ->.  th ).
12 idn2 28788 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ( ta  /\  -.  ph ) ).
13 simpl 445 . . . . . . . . . . 11  |-  ( ( ta  /\  -.  ph )  ->  ta )
1412, 13e2 28806 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ta ).
15 pm3.2 436 . . . . . . . . . 10  |-  ( th 
->  ( ta  ->  ( th  /\  ta ) ) )
1611, 14, 15e12 28910 . . . . . . . . 9  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ( th  /\  ta ) ).
17 19.8a 1763 . . . . . . . . 9  |-  ( ( th  /\  ta )  ->  E. x ( th 
/\  ta ) )
1816, 17e2 28806 . . . . . . . 8  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  E. x ( th 
/\  ta ) ).
19 notnot1 117 . . . . . . . 8  |-  ( E. x ( th  /\  ta )  ->  -.  -.  E. x ( th  /\  ta ) )
2018, 19e2 28806 . . . . . . 7  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  -.  E. x
( th  /\  ta ) ).
21 con3 129 . . . . . . 7  |-  ( ( A. x ch  ->  -. 
E. x ( th 
/\  ta ) )  -> 
( -.  -.  E. x ( th  /\  ta )  ->  -.  A. x ch ) )
225, 20, 21e02 28872 . . . . . 6  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  A. x ch
).
23 hbe1 1747 . . . . . . 7  |-  ( E. x  -.  th  ->  A. x E. x  -.  th )
2423hbn 1802 . . . . . 6  |-  ( -. 
E. x  -.  th  ->  A. x  -.  E. x  -.  th )
25 hba1 1805 . . . . . . 7  |-  ( A. x ch  ->  A. x A. x ch )
2625hbn 1802 . . . . . 6  |-  ( -. 
A. x ch  ->  A. x  -.  A. x ch )
274, 22, 24, 26exinst01 28800 . . . . 5  |-  (.  -.  E. x  -.  th  ->.  -.  A. x ch ).
28 exnal 1584 . . . . . 6  |-  ( E. x  -.  ch  <->  -.  A. x ch )
2928biimpri 199 . . . . 5  |-  ( -. 
A. x ch  ->  E. x  -.  ch )
3027, 29e1_ 28802 . . . 4  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ch ).
31 idn2 28788 . . . . . 6  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  -.  ch ).
32 vk15.4jVD.1 . . . . . . . . . 10  |-  -.  ( E. x  -.  ph  /\  E. x ( ps  /\  -.  ch ) )
33 pm3.13 489 . . . . . . . . . 10  |-  ( -.  ( E. x  -.  ph 
/\  E. x ( ps 
/\  -.  ch )
)  ->  ( -.  E. x  -.  ph  \/  -.  E. x ( ps 
/\  -.  ch )
) )
3432, 33e0_ 28958 . . . . . . . . 9  |-  ( -. 
E. x  -.  ph  \/  -.  E. x ( ps  /\  -.  ch ) )
35 simpr 449 . . . . . . . . . . . . 13  |-  ( ( ta  /\  -.  ph )  ->  -.  ph )
3612, 35e2 28806 . . . . . . . . . . . 12  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  ph ).
37 19.8a 1763 . . . . . . . . . . . 12  |-  ( -. 
ph  ->  E. x  -.  ph )
3836, 37e2 28806 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  E. x  -.  ph ).
39 hbe1 1747 . . . . . . . . . . 11  |-  ( E. x  -.  ph  ->  A. x E. x  -.  ph )
404, 38, 24, 39exinst01 28800 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ph ).
41 notnot1 117 . . . . . . . . . 10  |-  ( E. x  -.  ph  ->  -. 
-.  E. x  -.  ph )
4240, 41e1_ 28802 . . . . . . . . 9  |-  (.  -.  E. x  -.  th  ->.  -.  -.  E. x  -.  ph ).
43 pm2.53 364 . . . . . . . . 9  |-  ( ( -.  E. x  -.  ph  \/  -.  E. x
( ps  /\  -.  ch ) )  ->  ( -.  -.  E. x  -.  ph 
->  -.  E. x ( ps  /\  -.  ch ) ) )
4434, 42, 43e01 28866 . . . . . . . 8  |-  (.  -.  E. x  -.  th  ->.  -.  E. x
( ps  /\  -.  ch ) ).
45 exanali 1596 . . . . . . . . 9  |-  ( E. x ( ps  /\  -.  ch )  <->  -.  A. x
( ps  ->  ch ) )
4645con5i 28681 . . . . . . . 8  |-  ( -. 
E. x ( ps 
/\  -.  ch )  ->  A. x ( ps 
->  ch ) )
4744, 46e1_ 28802 . . . . . . 7  |-  (.  -.  E. x  -.  th  ->.  A. x
( ps  ->  ch ) ).
48 sp 1764 . . . . . . 7  |-  ( A. x ( ps  ->  ch )  ->  ( ps  ->  ch ) )
4947, 48e1_ 28802 . . . . . 6  |-  (.  -.  E. x  -.  th  ->.  ( ps  ->  ch ) ).
50 con3 129 . . . . . . 7  |-  ( ( ps  ->  ch )  ->  ( -.  ch  ->  -. 
ps ) )
5150com12 30 . . . . . 6  |-  ( -. 
ch  ->  ( ( ps 
->  ch )  ->  -.  ps ) )
5231, 49, 51e21 28916 . . . . 5  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  -.  ps ).
53 19.8a 1763 . . . . 5  |-  ( -. 
ps  ->  E. x  -.  ps )
5452, 53e2 28806 . . . 4  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  E. x  -.  ps ).
55 hbe1 1747 . . . 4  |-  ( E. x  -.  ps  ->  A. x E. x  -.  ps )
5630, 54, 24, 55exinst11 28801 . . 3  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ps ).
57 exnal 1584 . . . 4  |-  ( E. x  -.  ps  <->  -.  A. x ps )
5857biimpi 188 . . 3  |-  ( E. x  -.  ps  ->  -. 
A. x ps )
5956, 58e1_ 28802 . 2  |-  (.  -.  E. x  -.  th  ->.  -.  A. x ps ).
6059in1 28736 1  |-  ( -. 
E. x  -.  th  ->  -.  A. x ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 359    /\ wa 360   A.wal 1550   E.wex 1551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-ex 1552  df-nf 1555  df-vd1 28735  df-vd2 28744
  Copyright terms: Public domain W3C validator