Theorem suctrALT

Description: The successor of a transitive class is transitive. The proof of https://us.metamath.org/other/completeusersproof/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctrALT using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/suctrro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr for the original proof. (Contributed by Alan Sare, 11-Apr-2009) (Revised by Alan Sare, 12-Jun-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	suctrALT	|- ( 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		trel	|- ( Tr A -> ( ( z e. y /\ y e. A ) -> z e. A ) )
7	6	3impib	|- ( ( Tr A /\ z e. y /\ y e. A ) -> z e. A )
8	7	idiALT	|- ( ( Tr A /\ z e. y /\ y e. A ) -> z e. A )
9	2 4 5 8	syl3an	|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) /\ y e. A ) -> z e. A )
10	1 9	sselid	|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) /\ y e. A ) -> z e. suc A )
11	10	3expia	|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) )
12	4	adantr	|- ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> z e. y )
13		id	|- ( y = A -> y = A )
14	13	adantl	|- ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> y = A )
15	12 14	eleqtrd	|- ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> z e. A )
16	1 15	sselid	|- ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> z e. suc A )
17	16	ex	|- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) )
18	17	adantl	|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y = A -> z e. suc A ) )
19	3	simprd	|- ( ( z e. y /\ y e. suc A ) -> y e. suc A )
20		elsuci	|- ( y e. suc A -> ( y e. A \/ y = A ) )
21	19 20	syl	|- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) )
22	21	adantl	|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A \/ y = A ) )
23	11 18 22	mpjaod	|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A )
24	23	ex	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
25	24	alrimivv	|- ( Tr A -> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
26		dftr2	|- ( Tr suc A <-> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
27	26	biimpri	|- ( A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) -> Tr suc A )
28	25 27	syl	|- ( Tr A -> Tr suc A )