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	|- ( Tr A -> Tr suc A )

Proof

Step	Hyp	Ref	Expression
1		elsuci	|- ( y e. suc A -> ( y e. A \/ y = A ) )
2		trel	|- ( Tr A -> ( ( z e. y /\ y e. A ) -> z e. A ) )
3	2	expdimp	|- ( ( Tr A /\ z e. y ) -> ( y e. A -> z e. A ) )
4		eleq2	|- ( y = A -> ( z e. y <-> z e. A ) )
5	4	biimpcd	|- ( z e. y -> ( y = A -> z e. A ) )
6	5	adantl	|- ( ( Tr A /\ z e. y ) -> ( y = A -> z e. A ) )
7	3 6	jaod	|- ( ( Tr A /\ z e. y ) -> ( ( y e. A \/ y = A ) -> z e. A ) )
8	1 7	syl5	|- ( ( Tr A /\ z e. y ) -> ( y e. suc A -> z e. A ) )
9	8	expimpd	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> z e. A ) )
10		elelsuc	|- ( z e. A -> z e. suc A )
11	9 10	syl6	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
12	11	alrimivv	|- ( Tr A -> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
13		dftr2	|- ( Tr suc A <-> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
14	12 13	sylibr	|- ( Tr A -> Tr suc A )