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

Theorem suctrALTcfVD 29035
Description: The following User's Proof is a Virtual Deduction proof ( see: wvd1 28660) 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 29034 is suctrALTcfVD 29035 without virtual deductions and was derived automatically from suctrALTcfVD 29035. 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 4658 . . . . . . . 8  |-  A  C_  suc  A
2 idn1 28665 . . . . . . . . 9  |-  (. Tr  A 
->.  Tr  A ).
3 idn1 28665 . . . . . . . . . 10  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( z  e.  y  /\  y  e.  suc  A ) ).
4 simpl 444 . . . . . . . . . 10  |-  ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  y )
53, 4el1 28729 . . . . . . . . 9  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  z  e.  y ).
6 idn1 28665 . . . . . . . . 9  |-  (. y  e.  A  ->.  y  e.  A ).
7 trel 4309 . . . . . . . . . 10  |-  ( Tr  A  ->  ( (
z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
873impib 1151 . . . . . . . . 9  |-  ( ( Tr  A  /\  z  e.  y  /\  y  e.  A )  ->  z  e.  A )
92, 5, 6, 8el123 28876 . . . . . . . 8  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ,. y  e.  A ).  ->.  z  e.  A ).
10 ssel2 3343 . . . . . . . 8  |-  ( ( A  C_  suc  A  /\  z  e.  A )  ->  z  e.  suc  A
)
111, 9, 10el0321old 28827 . . . . . . 7  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ,. y  e.  A ).  ->.  z  e.  suc  A ).
1211int3 28713 . . . . . 6  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ).  ->.  ( y  e.  A  ->  z  e.  suc  A
) ).
13 idn1 28665 . . . . . . . . 9  |-  (. y  =  A  ->.  y  =  A ).
14 eleq2 2497 . . . . . . . . . 10  |-  ( y  =  A  ->  (
z  e.  y  <->  z  e.  A ) )
1514biimpac 473 . . . . . . . . 9  |-  ( ( z  e.  y  /\  y  =  A )  ->  z  e.  A )
165, 13, 15el12 28838 . . . . . . . 8  |-  (. (. ( z  e.  y  /\  y  e.  suc  A ) ,. y  =  A ).  ->.  z  e.  A ).
171, 16, 10el021old 28802 . . . . . . 7  |-  (. (. ( z  e.  y  /\  y  e.  suc  A ) ,. y  =  A ).  ->.  z  e.  suc  A ).
1817int2 28707 . . . . . 6  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( y  =  A  ->  z  e.  suc  A ) ).
19 simpr 448 . . . . . . . 8  |-  ( ( z  e.  y  /\  y  e.  suc  A )  ->  y  e.  suc  A )
203, 19el1 28729 . . . . . . 7  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  y  e.  suc  A ).
21 elsuci 4647 . . . . . . 7  |-  ( y  e.  suc  A  -> 
( y  e.  A  \/  y  =  A
) )
2220, 21el1 28729 . . . . . 6  |-  (. (
z  e.  y  /\  y  e.  suc  A )  ->.  ( y  e.  A  \/  y  =  A
) ).
23 jao 499 . . . . . . 7  |-  ( ( y  e.  A  -> 
z  e.  suc  A
)  ->  ( (
y  =  A  -> 
z  e.  suc  A
)  ->  ( (
y  e.  A  \/  y  =  A )  ->  z  e.  suc  A
) ) )
24233imp 1147 . . . . . 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 28829 . . . . 5  |-  (. (. Tr  A ,. ( z  e.  y  /\  y  e.  suc  A ) ).  ->.  z  e.  suc  A ).
2625int2 28707 . . . 4  |-  (. Tr  A 
->.  ( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) ).
2726gen12 28719 . . 3  |-  (. Tr  A 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) ).
28 dftr2 4304 . . . 4  |-  ( Tr 
suc  A  <->  A. z A. y
( ( z  e.  y  /\  y  e. 
suc  A )  -> 
z  e.  suc  A
) )
2928biimpri 198 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  suc  A )  ->  z  e.  suc  A )  ->  Tr  suc  A
)
3027, 29el1 28729 . 2  |-  (. Tr  A 
->.  Tr  suc  A ).
3130in1 28662 1  |-  ( Tr  A  ->  Tr  suc  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    /\ wa 359   A.wal 1549    = wceq 1652    e. wcel 1725    C_ wss 3320   Tr wtr 4302   suc csuc 4583
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-un 3325  df-in 3327  df-ss 3334  df-sn 3820  df-uni 4016  df-tr 4303  df-suc 4587  df-vd1 28661  df-vhc2 28673  df-vhc3 28681
  Copyright terms: Public domain W3C validator