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