Metamath Proof Explorer

Theorem suctrALTcfVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) 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 is suctrALTcfVD without virtual deductions and was derived automatically from suctrALTcfVD . 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 )

Ref Expression
Assertion suctrALTcfVD 
|- ( Tr A -> Tr suc A )

Proof

Step Hyp Ref Expression
1 sssucid 
 |-  A C_ suc A
2 idn1 
 |-  (. Tr A ->. Tr A ).
3 idn1 
 |-  (. ( z e. y /\ y e. suc A ) ->. ( z e. y /\ y e. suc A ) ).
4 simpl 
 |-  ( ( z e. y /\ y e. suc A ) -> z e. y )
5 3 4 el1 
 |-  (. ( z e. y /\ y e. suc A ) ->. z e. y ).
6 idn1 
 |-  (. y e. A ->. y e. A ).
7 trel 
 |-  ( Tr A -> ( ( z e. y /\ y e. A ) -> z e. A ) )
8 7 3impib 
 |-  ( ( Tr A /\ z e. y /\ y e. A ) -> z e. A )
9 2 5 6 8 el123 
 |-  (. (. Tr A ,. ( z e. y /\ y e. suc A ) ,. y e. A ). ->. z e. A ).
10 ssel2 
 |-  ( ( A C_ suc A /\ z e. A ) -> z e. suc A )
11 1 9 10 el0321old 
 |-  (. (. Tr A ,. ( z e. y /\ y e. suc A ) ,. y e. A ). ->. z e. suc A ).
12 11 int3 
 |-  (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. ( y e. A -> z e. suc A ) ).
13 idn1 
 |-  (. y = A ->. y = A ).
14 eleq2 
 |-  ( y = A -> ( z e. y <-> z e. A ) )
15 14 biimpac 
 |-  ( ( z e. y /\ y = A ) -> z e. A )
16 5 13 15 el12 
 |-  (. (. ( z e. y /\ y e. suc A ) ,. y = A ). ->. z e. A ).
17 1 16 10 el021old 
 |-  (. (. ( z e. y /\ y e. suc A ) ,. y = A ). ->. z e. suc A ).
18 17 int2 
 |-  (. ( z e. y /\ y e. suc A ) ->. ( y = A -> z e. suc A ) ).
19 simpr 
 |-  ( ( z e. y /\ y e. suc A ) -> y e. suc A )
20 3 19 el1 
 |-  (. ( z e. y /\ y e. suc A ) ->. y e. suc A ).
21 elsuci 
 |-  ( y e. suc A -> ( y e. A \/ y = A ) )
22 20 21 el1 
 |-  (. ( z e. y /\ y e. suc A ) ->. ( y e. A \/ y = A ) ).
23 jao 
 |-  ( ( y e. A -> z e. suc A ) -> ( ( y = A -> z e. suc A ) -> ( ( y e. A \/ y = A ) -> z e. suc A ) ) )
24 23 3imp 
 |-  ( ( ( y e. A -> z e. suc A ) /\ ( y = A -> z e. suc A ) /\ ( y e. A \/ y = A ) ) -> z e. suc A )
25 12 18 22 24 el2122old 
 |-  (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. z e. suc A ).
26 25 int2 
 |-  (. Tr A ->. ( ( z e. y /\ y e. suc A ) -> z e. suc A ) ).
27 26 gen12 
 |-  (. Tr A ->. A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) ).
28 dftr2 
 |-  ( Tr suc A <-> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
29 28 biimpri 
 |-  ( A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) -> Tr suc A )
30 27 29 el1 
 |-  (. Tr A ->. Tr suc A ).
31 30 in1 
 |-  ( Tr A -> Tr suc A )