Theorem trsuc

Description: A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003) (Proof shortened by Andrew Salmon, 12-Aug-2011)

	Ref	Expression
Assertion	trsuc	|- ( ( Tr A /\ suc B e. A ) -> B e. A )

Proof

Step	Hyp	Ref	Expression
1		trel	|- ( Tr A -> ( ( B e. suc B /\ suc B e. A ) -> B e. A ) )
2		sssucid	|- B C_ suc B
3		ssexg	|- ( ( B C_ suc B /\ suc B e. A ) -> B e. _V )
4	2 3	mpan	|- ( suc B e. A -> B e. _V )
5		sucidg	|- ( B e. _V -> B e. suc B )
6	4 5	syl	|- ( suc B e. A -> B e. suc B )
7	6	ancri	|- ( suc B e. A -> ( B e. suc B /\ suc B e. A ) )
8	1 7	impel	|- ( ( Tr A /\ suc B e. A ) -> B e. A )