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

Theorem suctrALTcfVD 29015
Description: The following User's Proof is a Virtual Deduction proof ( see: wvd1 28636) 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 O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. suctrALTcf 29014 is suctrALTcfVD 29015 without virtual deductions and was derived automatically from suctrALTcfVD 29015. 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 4485 . . . . . . . 8  |-  A  C_  suc  A
2 idn1 28641 . . . . . . . . 9  |-  (. Tr  A 
->.  Tr  A ).
3 idn1 28641 . . . . . . . . . 10  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( z  e.  y  /\  y  e.  suc  A ) ).
4 simpl 443 . . . . . . . . . 10  |-  ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  y )
53, 4el1 28705 . . . . . . . . 9  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  z  e.  y ).
6 idn1 28641 . . . . . . . . 9  |-  (. y  e.  A  ->.  y  e.  A ).
7 trel 4136 . . . . . . . . . 10  |-  ( Tr  A  ->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
873impib 1149 . . . . . . . . 9  |-  ( ( Tr  A  /\  z  e.  y  /\  y  e.  A )  ->  z  e.  A )
92, 5, 6, 8el123 28853 . . . . . . . 8  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ,. y  e.  A ).  ->.  z  e.  A ).
10 ssel2 3188 . . . . . . . 8  |-  ( ( A  C_  suc  A  /\  z  e.  A )  ->  z  e.  suc  A
)
111, 9, 10el0321old 28804 . . . . . . 7  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ,. y  e.  A ).  ->.  z  e.  suc  A ).
1211int3 28689 . . . . . 6  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ).  ->.  ( y  e.  A  ->  z  e.  suc  A
) ).
13 idn1 28641 . . . . . . . . 9  |-  (. y  =  A  ->.  y  =  A ).
14 eleq2 2357 . . . . . . . . . 10  |-  ( y  =  A  ->  (
z  e.  y  <->  z  e.  A ) )
1514biimpac 472 . . . . . . . . 9  |-  ( ( z  e.  y  /\  y  =  A )  ->  z  e.  A )
165, 13, 15el12 28815 . . . . . . . 8  |-  (. (. ( z  e.  y  /\  y  e.  suc  A ) ,. y  =  A ).  ->.  z  e.  A ).
171, 16, 10el021old 28779 . . . . . . 7  |-  (. (. ( z  e.  y  /\  y  e.  suc  A ) ,. y  =  A ).  ->.  z  e.  suc  A ).
1817int2 28683 . . . . . 6  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( y  =  A  ->  z  e.  suc  A ) ).
19 simpr 447 . . . . . . . 8  |-  ( ( z  e.  y  /\  y  e.  suc  A )  ->  y  e.  suc  A )
203, 19el1 28705 . . . . . . 7  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  y  e.  suc  A ).
21 elsuci 4474 . . . . . . 7  |-  ( y  e.  suc  A  -> 
( y  e.  A  \/  y  =  A
) )
2220, 21el1 28705 . . . . . 6  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( y  e.  A  \/  y  =  A
) ).
23 jao 498 . . . . . . 7  |-  ( ( y  e.  A  -> 
z  e.  suc  A
)  ->  ( (
y  =  A  -> 
z  e.  suc  A
)  ->  ( (
y  e.  A  \/  y  =  A )  ->  z  e.  suc  A
) ) )
24233imp 1145 . . . . . 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 28806 . . . . 5  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ).  ->.  z  e.  suc  A ).
2625int2 28683 . . . 4  |-  (. Tr  A 
->.  ( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) ).
2726gen12 28695 . . 3  |-  (. Tr  A 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) ).
28 dftr2 4131 . . . 4  |-  ( Tr 
suc  A  <->  A. z A. y
( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) )
2928biimpri 197 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  suc  A )  ->  Tr  suc  A
)
3027, 29el1 28705 . 2  |-  (. Tr  A 
->.  Tr  suc  A ).
3130in1 28638 1  |-  ( Tr  A  ->  Tr  suc  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    /\ wa 358   A.wal 1530    = wceq 1632    e. wcel 1696    C_ wss 3165   Tr wtr 4129   suc csuc 4410
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-sn 3659  df-uni 3844  df-tr 4130  df-suc 4414  df-vd1 28637  df-vhc2 28649  df-vhc3 28657
  Copyright terms: Public domain W3C validator