Metamath Proof Explorer


Theorem suctr

Description: The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009) (Proof shortened by JJ, 24-Sep-2021)

Ref Expression
Assertion suctr TrATrsucA

Proof

Step Hyp Ref Expression
1 elsuci ysucAyAy=A
2 trel TrAzyyAzA
3 2 expdimp TrAzyyAzA
4 eleq2 y=AzyzA
5 4 biimpcd zyy=AzA
6 5 adantl TrAzyy=AzA
7 3 6 jaod TrAzyyAy=AzA
8 1 7 syl5 TrAzyysucAzA
9 8 expimpd TrAzyysucAzA
10 elelsuc zAzsucA
11 9 10 syl6 TrAzyysucAzsucA
12 11 alrimivv TrAzyzyysucAzsucA
13 dftr2 TrsucAzyzyysucAzsucA
14 12 13 sylibr TrATrsucA