Metamath Proof Explorer


Theorem suctrALT3

Description: The successor of a transitive class is transitive. suctrALT3 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/suctralt3vd.html . It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 19 used jaoded ). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 24 used dftr2 ) . (Contributed by Alan Sare, 3-Dec-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion suctrALT3 Tr A Tr suc A

Proof

Step Hyp Ref Expression
1 sssucid A suc A
2 id Tr A Tr A
3 id z y y suc A z y y suc A
4 3 simpld z y y suc A z y
5 id y A y A
6 2 4 5 trelded Tr A z y y suc A y A z A
7 1 6 sseldi Tr A z y y suc A y A z suc A
8 7 3expia Tr A z y y suc A y A z suc A
9 id y = A y = A
10 eleq2 y = A z y z A
11 10 biimpac z y y = A z A
12 4 9 11 syl2an z y y suc A y = A z A
13 1 12 sseldi z y y suc A y = A z suc A
14 13 ex z y y suc A y = A z suc A
15 3 simprd z y y suc A y suc A
16 elsuci y suc A y A y = A
17 15 16 syl z y y suc A y A y = A
18 8 14 17 jaoded Tr A z y y suc A z y y suc A z y y suc A z suc A
19 18 un2122 Tr A z y y suc A z suc A
20 19 ex Tr A z y y suc A z suc A
21 20 alrimivv Tr A z y z y y suc A z suc A
22 dftr2 Tr suc A z y z y y suc A z suc A
23 22 biimpri z y z y y suc A z suc A Tr suc A
24 21 23 syl Tr A Tr suc A
25 24 idiALT Tr A Tr suc A