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

Theorem suctrALTcfVD 37299
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 36916) 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 37298 is suctrALTcfVD 37299 without virtual deductions and was derived automatically from suctrALTcfVD 37299. 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 5525 . . . . . . . 8  |-  A  C_  suc  A
2 idn1 36921 . . . . . . . . 9  |-  (. Tr  A 
->.  Tr  A ).
3 idn1 36921 . . . . . . . . . 10  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( z  e.  y  /\  y  e.  suc  A ) ).
4 simpl 459 . . . . . . . . . 10  |-  ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  y )
53, 4el1 36984 . . . . . . . . 9  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  z  e.  y ).
6 idn1 36921 . . . . . . . . 9  |-  (. y  e.  A  ->.  y  e.  A ).
7 trel 4531 . . . . . . . . . 10  |-  ( Tr  A  ->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
873impib 1204 . . . . . . . . 9  |-  ( ( Tr  A  /\  z  e.  y  /\  y  e.  A )  ->  z  e.  A )
92, 5, 6, 8el123 37130 . . . . . . . 8  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ,. y  e.  A ).  ->.  z  e.  A ).
10 ssel2 3465 . . . . . . . 8  |-  ( ( A  C_  suc  A  /\  z  e.  A )  ->  z  e.  suc  A
)
111, 9, 10el0321old 37081 . . . . . . 7  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ,. y  e.  A ).  ->.  z  e.  suc  A ).
1211int3 36968 . . . . . 6  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ).  ->.  ( y  e.  A  ->  z  e.  suc  A
) ).
13 idn1 36921 . . . . . . . . 9  |-  (. y  =  A  ->.  y  =  A ).
14 eleq2 2497 . . . . . . . . . 10  |-  ( y  =  A  ->  (
z  e.  y  <->  z  e.  A ) )
1514biimpac 489 . . . . . . . . 9  |-  ( ( z  e.  y  /\  y  =  A )  ->  z  e.  A )
165, 13, 15el12 37092 . . . . . . . 8  |-  (. (. ( z  e.  y  /\  y  e.  suc  A ) ,. y  =  A ).  ->.  z  e.  A ).
171, 16, 10el021old 37057 . . . . . . 7  |-  (. (. ( z  e.  y  /\  y  e.  suc  A ) ,. y  =  A ).  ->.  z  e.  suc  A ).
1817int2 36962 . . . . . 6  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( y  =  A  ->  z  e.  suc  A ) ).
19 simpr 463 . . . . . . . 8  |-  ( ( z  e.  y  /\  y  e.  suc  A )  ->  y  e.  suc  A )
203, 19el1 36984 . . . . . . 7  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  y  e.  suc  A ).
21 elsuci 5514 . . . . . . 7  |-  ( y  e.  suc  A  -> 
( y  e.  A  \/  y  =  A
) )
2220, 21el1 36984 . . . . . 6  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( y  e.  A  \/  y  =  A
) ).
23 jao 515 . . . . . . 7  |-  ( ( y  e.  A  -> 
z  e.  suc  A
)  ->  ( (
y  =  A  -> 
z  e.  suc  A
)  ->  ( (
y  e.  A  \/  y  =  A )  ->  z  e.  suc  A
) ) )
24233imp 1200 . . . . . 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 37083 . . . . 5  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ).  ->.  z  e.  suc  A ).
2625int2 36962 . . . 4  |-  (. Tr  A 
->.  ( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) ).
2726gen12 36974 . . 3  |-  (. Tr  A 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) ).
28 dftr2 4526 . . . 4  |-  ( Tr 
suc  A  <->  A. z A. y
( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) )
2928biimpri 210 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  suc  A )  ->  Tr  suc  A
)
3027, 29el1 36984 . 2  |-  (. Tr  A 
->.  Tr  suc  A ).
3130in1 36918 1  |-  ( Tr  A  ->  Tr  suc  A
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 370    /\ wa 371   A.wal 1436    = wceq 1438    e. wcel 1873    C_ wss 3442   Tr wtr 4524   suc csuc 5450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3087  df-un 3447  df-in 3449  df-ss 3456  df-sn 4005  df-uni 4226  df-tr 4525  df-suc 5454  df-vd1 36917  df-vhc2 36928  df-vhc3 36936
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator