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 33195
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 32778 is vk15.4jVD 33195 without virtual deductions and was automatically derived from vk15.4jVD 33195. 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 1647 . . . . . . . 8  |-  ( E. x ( ta  /\  -.  ph )  <->  -.  A. x
( ta  ->  ph )
)
32biimpri 206 . . . . . . 7  |-  ( -. 
A. x ( ta 
->  ph )  ->  E. x
( ta  /\  -.  ph ) )
41, 3e0a 33050 . . . . . 6  |-  E. x
( ta  /\  -.  ph )
5 vk15.4jVD.2 . . . . . . 7  |-  ( A. x ch  ->  -.  E. x ( th  /\  ta ) )
6 idn1 32832 . . . . . . . . . . . 12  |-  (.  -.  E. x  -.  th  ->.  -.  E. x  -.  th ).
7 alex 1627 . . . . . . . . . . . . 13  |-  ( A. x th  <->  -.  E. x  -.  th )
87biimpri 206 . . . . . . . . . . . 12  |-  ( -. 
E. x  -.  th  ->  A. x th )
96, 8e1a 32894 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th  ->.  A. x th ).
10 sp 1808 . . . . . . . . . . 11  |-  ( A. x th  ->  th )
119, 10e1a 32894 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th  ->.  th ).
12 idn2 32880 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ( ta  /\  -.  ph ) ).
13 simpl 457 . . . . . . . . . . 11  |-  ( ( ta  /\  -.  ph )  ->  ta )
1412, 13e2 32898 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ta ).
15 pm3.2 447 . . . . . . . . . 10  |-  ( th 
->  ( ta  ->  ( th  /\  ta ) ) )
1611, 14, 15e12 33002 . . . . . . . . 9  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ( th  /\  ta ) ).
17 19.8a 1806 . . . . . . . . 9  |-  ( ( th  /\  ta )  ->  E. x ( th 
/\  ta ) )
1816, 17e2 32898 . . . . . . . 8  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  E. x ( th 
/\  ta ) ).
19 notnot1 122 . . . . . . . 8  |-  ( E. x ( th  /\  ta )  ->  -.  -.  E. x ( th  /\  ta ) )
2018, 19e2 32898 . . . . . . 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 32964 . . . . . 6  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  A. x ch
).
23 hbe1 1788 . . . . . . 7  |-  ( E. x  -.  th  ->  A. x E. x  -.  th )
2423hbn 1843 . . . . . 6  |-  ( -. 
E. x  -.  th  ->  A. x  -.  E. x  -.  th )
25 hba1 1844 . . . . . . 7  |-  ( A. x ch  ->  A. x A. x ch )
2625hbn 1843 . . . . . 6  |-  ( -. 
A. x ch  ->  A. x  -.  A. x ch )
274, 22, 24, 26exinst01 32892 . . . . 5  |-  (.  -.  E. x  -.  th  ->.  -.  A. x ch ).
28 exnal 1628 . . . . . 6  |-  ( E. x  -.  ch  <->  -.  A. x ch )
2928biimpri 206 . . . . 5  |-  ( -. 
A. x ch  ->  E. x  -.  ch )
3027, 29e1a 32894 . . . 4  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ch ).
31 idn2 32880 . . . . . 6  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  -.  ch ).
32 vk15.4jVD.1 . . . . . . . . . 10  |-  -.  ( E. x  -.  ph  /\  E. x ( ps  /\  -.  ch ) )
33 pm3.13 501 . . . . . . . . . 10  |-  ( -.  ( E. x  -.  ph 
/\  E. x ( ps 
/\  -.  ch )
)  ->  ( -.  E. x  -.  ph  \/  -.  E. x ( ps 
/\  -.  ch )
) )
3432, 33e0a 33050 . . . . . . . . 9  |-  ( -. 
E. x  -.  ph  \/  -.  E. x ( ps  /\  -.  ch ) )
35 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ta  /\  -.  ph )  ->  -.  ph )
3612, 35e2 32898 . . . . . . . . . . . 12  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  ph ).
37 19.8a 1806 . . . . . . . . . . . 12  |-  ( -. 
ph  ->  E. x  -.  ph )
3836, 37e2 32898 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  E. x  -.  ph ).
39 hbe1 1788 . . . . . . . . . . 11  |-  ( E. x  -.  ph  ->  A. x E. x  -.  ph )
404, 38, 24, 39exinst01 32892 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ph ).
41 notnot1 122 . . . . . . . . . 10  |-  ( E. x  -.  ph  ->  -. 
-.  E. x  -.  ph )
4240, 41e1a 32894 . . . . . . . . 9  |-  (.  -.  E. x  -.  th  ->.  -.  -.  E. x  -.  ph ).
43 pm2.53 373 . . . . . . . . 9  |-  ( ( -.  E. x  -.  ph  \/  -.  E. x
( ps  /\  -.  ch ) )  ->  ( -.  -.  E. x  -.  ph 
->  -.  E. x ( ps  /\  -.  ch ) ) )
4434, 42, 43e01 32958 . . . . . . . 8  |-  (.  -.  E. x  -.  th  ->.  -.  E. x
( ps  /\  -.  ch ) ).
45 exanali 1647 . . . . . . . . 9  |-  ( E. x ( ps  /\  -.  ch )  <->  -.  A. x
( ps  ->  ch ) )
4645con5i 32773 . . . . . . . 8  |-  ( -. 
E. x ( ps 
/\  -.  ch )  ->  A. x ( ps 
->  ch ) )
4744, 46e1a 32894 . . . . . . 7  |-  (.  -.  E. x  -.  th  ->.  A. x
( ps  ->  ch ) ).
48 sp 1808 . . . . . . 7  |-  ( A. x ( ps  ->  ch )  ->  ( ps  ->  ch ) )
4947, 48e1a 32894 . . . . . 6  |-  (.  -.  E. x  -.  th  ->.  ( ps  ->  ch ) ).
50 con3 134 . . . . . . 7  |-  ( ( ps  ->  ch )  ->  ( -.  ch  ->  -. 
ps ) )
5150com12 31 . . . . . 6  |-  ( -. 
ch  ->  ( ( ps 
->  ch )  ->  -.  ps ) )
5231, 49, 51e21 33008 . . . . 5  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  -.  ps ).
53 19.8a 1806 . . . . 5  |-  ( -. 
ps  ->  E. x  -.  ps )
5452, 53e2 32898 . . . 4  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  E. x  -.  ps ).
55 hbe1 1788 . . . 4  |-  ( E. x  -.  ps  ->  A. x E. x  -.  ps )
5630, 54, 24, 55exinst11 32893 . . 3  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ps ).
57 exnal 1628 . . . 4  |-  ( E. x  -.  ps  <->  -.  A. x ps )
5857biimpi 194 . . 3  |-  ( E. x  -.  ps  ->  -. 
A. x ps )
5956, 58e1a 32894 . 2  |-  (.  -.  E. x  -.  th  ->.  -.  A. x ps ).
6059in1 32829 1  |-  ( -. 
E. x  -.  th  ->  -.  A. x ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368    /\ wa 369   A.wal 1377   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1597  df-nf 1600  df-vd1 32828  df-vd2 32836
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator