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

Theorem suctrALTcfVD 36960
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 36577) 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 36959 is suctrALTcfVD 36960 without virtual deductions and was derived automatically from suctrALTcfVD 36960. 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 5519 . . . . . . . 8  |-  A  C_  suc  A
2 idn1 36582 . . . . . . . . 9  |-  (. Tr  A 
->.  Tr  A ).
3 idn1 36582 . . . . . . . . . 10  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( z  e.  y  /\  y  e.  suc  A ) ).
4 simpl 458 . . . . . . . . . 10  |-  ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  y )
53, 4el1 36645 . . . . . . . . 9  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  z  e.  y ).
6 idn1 36582 . . . . . . . . 9  |-  (. y  e.  A  ->.  y  e.  A ).
7 trel 4527 . . . . . . . . . 10  |-  ( Tr  A  ->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
873impib 1203 . . . . . . . . 9  |-  ( ( Tr  A  /\  z  e.  y  /\  y  e.  A )  ->  z  e.  A )
92, 5, 6, 8el123 36791 . . . . . . . 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 36742 . . . . . . 7  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ,. y  e.  A ).  ->.  z  e.  suc  A ).
1211int3 36629 . . . . . 6  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ).  ->.  ( y  e.  A  ->  z  e.  suc  A
) ).
13 idn1 36582 . . . . . . . . 9  |-  (. y  =  A  ->.  y  =  A ).
14 eleq2 2502 . . . . . . . . . 10  |-  ( y  =  A  ->  (
z  e.  y  <->  z  e.  A ) )
1514biimpac 488 . . . . . . . . 9  |-  ( ( z  e.  y  /\  y  =  A )  ->  z  e.  A )
165, 13, 15el12 36753 . . . . . . . 8  |-  (. (. ( z  e.  y  /\  y  e.  suc  A ) ,. y  =  A ).  ->.  z  e.  A ).
171, 16, 10el021old 36718 . . . . . . 7  |-  (. (. ( z  e.  y  /\  y  e.  suc  A ) ,. y  =  A ).  ->.  z  e.  suc  A ).
1817int2 36623 . . . . . 6  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( y  =  A  ->  z  e.  suc  A ) ).
19 simpr 462 . . . . . . . 8  |-  ( ( z  e.  y  /\  y  e.  suc  A )  ->  y  e.  suc  A )
203, 19el1 36645 . . . . . . 7  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  y  e.  suc  A ).
21 elsuci 5508 . . . . . . 7  |-  ( y  e.  suc  A  -> 
( y  e.  A  \/  y  =  A
) )
2220, 21el1 36645 . . . . . 6  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( y  e.  A  \/  y  =  A
) ).
23 jao 514 . . . . . . 7  |-  ( ( y  e.  A  -> 
z  e.  suc  A
)  ->  ( (
y  =  A  -> 
z  e.  suc  A
)  ->  ( (
y  e.  A  \/  y  =  A )  ->  z  e.  suc  A
) ) )
24233imp 1199 . . . . . 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 36744 . . . . 5  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ).  ->.  z  e.  suc  A ).
2625int2 36623 . . . 4  |-  (. Tr  A 
->.  ( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) ).
2726gen12 36635 . . 3  |-  (. Tr  A 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) ).
28 dftr2 4522 . . . 4  |-  ( Tr 
suc  A  <->  A. z A. y
( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) )
2928biimpri 209 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  suc  A )  ->  Tr  suc  A
)
3027, 29el1 36645 . 2  |-  (. Tr  A 
->.  Tr  suc  A ).
3130in1 36579 1  |-  ( Tr  A  ->  Tr  suc  A
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 369    /\ wa 370   A.wal 1435    = wceq 1437    e. wcel 1870    C_ wss 3442   Tr wtr 4520   suc csuc 5444
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447  df-in 3449  df-ss 3456  df-sn 4003  df-uni 4223  df-tr 4521  df-suc 5448  df-vd1 36578  df-vhc2 36589  df-vhc3 36597
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator