Metamath Proof Explorer

Theorem suctrALTcf

Description: The sucessor of a transitive class is transitive. suctrALTcf , using conventional notation, was translated from virtual deduction form, suctrALTcfVD , using a translation program. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 sssucid 
 |-  A C_ suc A
2 id 
 |-  ( Tr A -> Tr A )
3 id 
 |-  ( ( 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 syl 
 |-  ( ( z e. y /\ y e. suc A ) -> z e. y )
6 id 
 |-  ( 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 syl3an 
 |-  ( ( 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 eel0321old 
 |-  ( ( Tr A /\ ( z e. y /\ y e. suc A ) /\ y e. A ) -> z e. suc A )
12 11 3expia 
 |-  ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
13 id 
 |-  ( 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 syl2an 
 |-  ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> z e. A )
17 1 16 10 eel021old 
 |-  ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> z e. suc A )
18 17 ex 
 |-  ( ( 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 syl 
 |-  ( ( 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 syl 
 |-  ( ( 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 eel2122old 
 |-  ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
26 25 ex 
 |-  ( Tr A -> ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
27 26 alrimivv 
 |-  ( 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 syl 
 |-  ( Tr A -> Tr suc A )
31 30 iin1 
 |-  ( Tr A -> Tr suc A )