This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( 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 )