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 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 3 simpld
 |-  ( ( z e. y /\ y e. suc A ) -> z e. y )
5 id
 |-  ( y e. A -> y e. A )
6 2 4 5 trelded
 |-  ( ( Tr A /\ ( z e. y /\ y e. suc A ) /\ y e. A ) -> z e. A )
7 1 6 sseldi
 |-  ( ( Tr A /\ ( z e. y /\ y e. suc A ) /\ y e. A ) -> z e. suc A )
8 7 3expia
 |-  ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
9 id
 |-  ( y = A -> y = A )
10 eleq2
 |-  ( y = A -> ( z e. y <-> z e. A ) )
11 10 biimpac
 |-  ( ( z e. y /\ y = A ) -> z e. A )
12 4 9 11 syl2an
 |-  ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> z e. A )
13 1 12 sseldi
 |-  ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> z e. suc A )
14 13 ex
 |-  ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
15 3 simprd
 |-  ( ( z e. y /\ y e. suc A ) -> y e. suc A )
16 elsuci
 |-  ( y e. suc A -> ( y e. A \/ y = A ) )
17 15 16 syl
 |-  ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
18 8 14 17 jaoded
 |-  ( ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) /\ ( z e. y /\ y e. suc A ) /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
19 18 un2122
 |-  ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
20 19 ex
 |-  ( Tr A -> ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
21 20 alrimivv
 |-  ( Tr A -> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
22 dftr2
 |-  ( Tr suc A <-> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
23 22 biimpri
 |-  ( A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) -> Tr suc A )
24 21 23 syl
 |-  ( Tr A -> Tr suc A )
25 24 idiALT
 |-  ( Tr A -> Tr suc A )