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 37178
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 36749 is vk15.4jVD 37178 without virtual deductions and was automatically derived from vk15.4jVD 37178. 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 1716 . . . . . . . 8  |-  ( E. x ( ta  /\  -.  ph )  <->  -.  A. x
( ta  ->  ph )
)
32biimpri 210 . . . . . . 7  |-  ( -. 
A. x ( ta 
->  ph )  ->  E. x
( ta  /\  -.  ph ) )
41, 3e0a 37026 . . . . . 6  |-  E. x
( ta  /\  -.  ph )
5 vk15.4jVD.2 . . . . . . 7  |-  ( A. x ch  ->  -.  E. x ( th  /\  ta ) )
6 idn1 36809 . . . . . . . . . . . 12  |-  (.  -.  E. x  -.  th  ->.  -.  E. x  -.  th ).
7 alex 1695 . . . . . . . . . . . . 13  |-  ( A. x th  <->  -.  E. x  -.  th )
87biimpri 210 . . . . . . . . . . . 12  |-  ( -. 
E. x  -.  th  ->  A. x th )
96, 8e1a 36871 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th  ->.  A. x th ).
10 sp 1911 . . . . . . . . . . 11  |-  ( A. x th  ->  th )
119, 10e1a 36871 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th  ->.  th ).
12 idn2 36857 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ( ta  /\  -.  ph ) ).
13 simpl 459 . . . . . . . . . . 11  |-  ( ( ta  /\  -.  ph )  ->  ta )
1412, 13e2 36875 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ta ).
15 pm3.2 449 . . . . . . . . . 10  |-  ( th 
->  ( ta  ->  ( th  /\  ta ) ) )
1611, 14, 15e12 36978 . . . . . . . . 9  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  ( th  /\  ta ) ).
17 19.8a 1909 . . . . . . . . 9  |-  ( ( th  /\  ta )  ->  E. x ( th 
/\  ta ) )
1816, 17e2 36875 . . . . . . . 8  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  E. x ( th 
/\  ta ) ).
19 notnot1 126 . . . . . . . 8  |-  ( E. x ( th  /\  ta )  ->  -.  -.  E. x ( th  /\  ta ) )
2018, 19e2 36875 . . . . . . 7  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  -.  E. x
( th  /\  ta ) ).
21 con3 140 . . . . . . 7  |-  ( ( A. x ch  ->  -. 
E. x ( th 
/\  ta ) )  -> 
( -.  -.  E. x ( th  /\  ta )  ->  -.  A. x ch ) )
225, 20, 21e02 36941 . . . . . 6  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  A. x ch
).
23 hbe1 1890 . . . . . . 7  |-  ( E. x  -.  th  ->  A. x E. x  -.  th )
2423hbn 1951 . . . . . 6  |-  ( -. 
E. x  -.  th  ->  A. x  -.  E. x  -.  th )
25 hba1 1952 . . . . . . 7  |-  ( A. x ch  ->  A. x A. x ch )
2625hbn 1951 . . . . . 6  |-  ( -. 
A. x ch  ->  A. x  -.  A. x ch )
274, 22, 24, 26exinst01 36869 . . . . 5  |-  (.  -.  E. x  -.  th  ->.  -.  A. x ch ).
28 exnal 1696 . . . . . 6  |-  ( E. x  -.  ch  <->  -.  A. x ch )
2928biimpri 210 . . . . 5  |-  ( -. 
A. x ch  ->  E. x  -.  ch )
3027, 29e1a 36871 . . . 4  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ch ).
31 idn2 36857 . . . . . 6  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  -.  ch ).
32 vk15.4jVD.1 . . . . . . . . . 10  |-  -.  ( E. x  -.  ph  /\  E. x ( ps  /\  -.  ch ) )
33 pm3.13 504 . . . . . . . . . 10  |-  ( -.  ( E. x  -.  ph 
/\  E. x ( ps 
/\  -.  ch )
)  ->  ( -.  E. x  -.  ph  \/  -.  E. x ( ps 
/\  -.  ch )
) )
3432, 33e0a 37026 . . . . . . . . 9  |-  ( -. 
E. x  -.  ph  \/  -.  E. x ( ps  /\  -.  ch ) )
35 simpr 463 . . . . . . . . . . . . 13  |-  ( ( ta  /\  -.  ph )  ->  -.  ph )
3612, 35e2 36875 . . . . . . . . . . . 12  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  -.  ph ).
37 19.8a 1909 . . . . . . . . . . . 12  |-  ( -. 
ph  ->  E. x  -.  ph )
3836, 37e2 36875 . . . . . . . . . . 11  |-  (.  -.  E. x  -.  th ,. ( ta  /\  -.  ph ) 
->.  E. x  -.  ph ).
39 hbe1 1890 . . . . . . . . . . 11  |-  ( E. x  -.  ph  ->  A. x E. x  -.  ph )
404, 38, 24, 39exinst01 36869 . . . . . . . . . 10  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ph ).
41 notnot1 126 . . . . . . . . . 10  |-  ( E. x  -.  ph  ->  -. 
-.  E. x  -.  ph )
4240, 41e1a 36871 . . . . . . . . 9  |-  (.  -.  E. x  -.  th  ->.  -.  -.  E. x  -.  ph ).
43 pm2.53 375 . . . . . . . . 9  |-  ( ( -.  E. x  -.  ph  \/  -.  E. x
( ps  /\  -.  ch ) )  ->  ( -.  -.  E. x  -.  ph 
->  -.  E. x ( ps  /\  -.  ch ) ) )
4434, 42, 43e01 36935 . . . . . . . 8  |-  (.  -.  E. x  -.  th  ->.  -.  E. x
( ps  /\  -.  ch ) ).
45 exanali 1716 . . . . . . . . 9  |-  ( E. x ( ps  /\  -.  ch )  <->  -.  A. x
( ps  ->  ch ) )
4645con5i 36744 . . . . . . . 8  |-  ( -. 
E. x ( ps 
/\  -.  ch )  ->  A. x ( ps 
->  ch ) )
4744, 46e1a 36871 . . . . . . 7  |-  (.  -.  E. x  -.  th  ->.  A. x
( ps  ->  ch ) ).
48 sp 1911 . . . . . . 7  |-  ( A. x ( ps  ->  ch )  ->  ( ps  ->  ch ) )
4947, 48e1a 36871 . . . . . 6  |-  (.  -.  E. x  -.  th  ->.  ( ps  ->  ch ) ).
50 con3 140 . . . . . . 7  |-  ( ( ps  ->  ch )  ->  ( -.  ch  ->  -. 
ps ) )
5150com12 33 . . . . . 6  |-  ( -. 
ch  ->  ( ( ps 
->  ch )  ->  -.  ps ) )
5231, 49, 51e21 36984 . . . . 5  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  -.  ps ).
53 19.8a 1909 . . . . 5  |-  ( -. 
ps  ->  E. x  -.  ps )
5452, 53e2 36875 . . . 4  |-  (.  -.  E. x  -.  th ,.  -.  ch  ->.  E. x  -.  ps ).
55 hbe1 1890 . . . 4  |-  ( E. x  -.  ps  ->  A. x E. x  -.  ps )
5630, 54, 24, 55exinst11 36870 . . 3  |-  (.  -.  E. x  -.  th  ->.  E. x  -.  ps ).
57 exnal 1696 . . . 4  |-  ( E. x  -.  ps  <->  -.  A. x ps )
5857biimpi 198 . . 3  |-  ( E. x  -.  ps  ->  -. 
A. x ps )
5956, 58e1a 36871 . 2  |-  (.  -.  E. x  -.  th  ->.  -.  A. x ps ).
6059in1 36806 1  |-  ( -. 
E. x  -.  th  ->  -.  A. x ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 370    /\ wa 371   A.wal 1436   E.wex 1660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-12 1906
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1661  df-nf 1665  df-vd1 36805  df-vd2 36813
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator