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

Theorem suctrALTcfVD 32014
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 31637) using conjunction-form virtual hypothesis collections. The conjunction-form version of completeusersproof.cmd. It allows the User to avoid superflous virtual hypotheses. This proof was completed automatically by a tools program which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. suctrALTcf 32013 is suctrALTcfVD 32014 without virtual deductions and was derived automatically from suctrALTcfVD 32014. The version of completeusersproof.cmd used is capable of only generating conjunction-form unification theorems, not unification deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. Tr  A  ->.  Tr  A ).
2::  |-  (..........  ( z  e.  y  /\  y  e.  suc  A )  ->.  ( z  e.  y  /\  y  e.  suc  A ) ).
3:2:  |-  (..........  ( z  e.  y  /\  y  e.  suc  A )  ->.  z  e.  y ).
4::  |-  (.................................... .......  y  e.  A  ->.  y  e.  A ).
5:1,3,4:  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A )  ,  y  e.  A ).  ->.  z  e.  A ).
6::  |-  A  C_  suc  A
7:5,6:  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A )  ,  y  e.  A ).  ->.  z  e.  suc  A ).
8:7:  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A )  ).  ->.  ( y  e.  A  ->  z  e.  suc  A ) ).
9::  |-  (.................................... ......  y  =  A  ->.  y  =  A ).
10:3,9:  |-  (.........  (. ( z  e.  y  /\  y  e.  suc  A ) ,  y  =  A ).  ->.  z  e.  A ).
11:10,6:  |-  (.........  (. ( z  e.  y  /\  y  e.  suc  A ) ,  y  =  A ).  ->.  z  e.  suc  A ).
12:11:  |-  (...........  ( z  e.  y  /\  y  e.  suc  A )  ->.  ( y  =  A  ->  z  e.  suc  A ) ).
13:2:  |-  (...........  ( z  e.  y  /\  y  e.  suc  A )  ->.  y  e.  suc  A ).
14:13:  |-  (...........  ( z  e.  y  /\  y  e.  suc  A )  ->.  ( y  e.  A  \/  y  =  A ) ).
15:8,12,14:  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A )  ).  ->.  z  e.  suc  A ).
16:15:  |-  (. Tr  A  ->.  ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  suc  A ) ).
17:16:  |-  (. Tr  A  ->.  A. z A. y ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  suc  A ) ).
18:17:  |-  (. Tr  A  ->.  Tr  suc  A ).
qed:18:  |-  ( Tr  A  ->  Tr  suc  A )
Assertion
Ref Expression
suctrALTcfVD  |-  ( Tr  A  ->  Tr  suc  A
)

Proof of Theorem suctrALTcfVD
Dummy variables  z 
y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sssucid 4907 . . . . . . . 8  |-  A  C_  suc  A
2 idn1 31642 . . . . . . . . 9  |-  (. Tr  A 
->.  Tr  A ).
3 idn1 31642 . . . . . . . . . 10  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( z  e.  y  /\  y  e.  suc  A ) ).
4 simpl 457 . . . . . . . . . 10  |-  ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  y )
53, 4el1 31705 . . . . . . . . 9  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  z  e.  y ).
6 idn1 31642 . . . . . . . . 9  |-  (. y  e.  A  ->.  y  e.  A ).
7 trel 4503 . . . . . . . . . 10  |-  ( Tr  A  ->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
873impib 1186 . . . . . . . . 9  |-  ( ( Tr  A  /\  z  e.  y  /\  y  e.  A )  ->  z  e.  A )
92, 5, 6, 8el123 31852 . . . . . . . 8  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ,. y  e.  A ).  ->.  z  e.  A ).
10 ssel2 3462 . . . . . . . 8  |-  ( ( A  C_  suc  A  /\  z  e.  A )  ->  z  e.  suc  A
)
111, 9, 10el0321old 31803 . . . . . . 7  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ,. y  e.  A ).  ->.  z  e.  suc  A ).
1211int3 31689 . . . . . 6  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ).  ->.  ( y  e.  A  ->  z  e.  suc  A
) ).
13 idn1 31642 . . . . . . . . 9  |-  (. y  =  A  ->.  y  =  A ).
14 eleq2 2527 . . . . . . . . . 10  |-  ( y  =  A  ->  (
z  e.  y  <->  z  e.  A ) )
1514biimpac 486 . . . . . . . . 9  |-  ( ( z  e.  y  /\  y  =  A )  ->  z  e.  A )
165, 13, 15el12 31814 . . . . . . . 8  |-  (. (. ( z  e.  y  /\  y  e.  suc  A ) ,. y  =  A ).  ->.  z  e.  A ).
171, 16, 10el021old 31778 . . . . . . 7  |-  (. (. ( z  e.  y  /\  y  e.  suc  A ) ,. y  =  A ).  ->.  z  e.  suc  A ).
1817int2 31683 . . . . . 6  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( y  =  A  ->  z  e.  suc  A ) ).
19 simpr 461 . . . . . . . 8  |-  ( ( z  e.  y  /\  y  e.  suc  A )  ->  y  e.  suc  A )
203, 19el1 31705 . . . . . . 7  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  y  e.  suc  A ).
21 elsuci 4896 . . . . . . 7  |-  ( y  e.  suc  A  -> 
( y  e.  A  \/  y  =  A
) )
2220, 21el1 31705 . . . . . 6  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( y  e.  A  \/  y  =  A
) ).
23 jao 512 . . . . . . 7  |-  ( ( y  e.  A  -> 
z  e.  suc  A
)  ->  ( (
y  =  A  -> 
z  e.  suc  A
)  ->  ( (
y  e.  A  \/  y  =  A )  ->  z  e.  suc  A
) ) )
24233imp 1182 . . . . . 6  |-  ( ( ( y  e.  A  ->  z  e.  suc  A
)  /\  ( y  =  A  ->  z  e. 
suc  A )  /\  ( y  e.  A  \/  y  =  A
) )  ->  z  e.  suc  A )
2512, 18, 22, 24el2122old 31805 . . . . 5  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ).  ->.  z  e.  suc  A ).
2625int2 31683 . . . 4  |-  (. Tr  A 
->.  ( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) ).
2726gen12 31695 . . 3  |-  (. Tr  A 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) ).
28 dftr2 4498 . . . 4  |-  ( Tr 
suc  A  <->  A. z A. y
( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) )
2928biimpri 206 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  suc  A )  ->  Tr  suc  A
)
3027, 29el1 31705 . 2  |-  (. Tr  A 
->.  Tr  suc  A ).
3130in1 31639 1  |-  ( Tr  A  ->  Tr  suc  A
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    /\ wa 369   A.wal 1368    = wceq 1370    e. wcel 1758    C_ wss 3439   Tr wtr 4496   suc csuc 4832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-un 3444  df-in 3446  df-ss 3453  df-sn 3989  df-uni 4203  df-tr 4497  df-suc 4836  df-vd1 31638  df-vhc2 31649  df-vhc3 31657
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator