Theorem limsuc

Description: The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003)

	Ref	Expression
Assertion	limsuc	|- ( Lim A -> ( B e. A <-> suc B e. A ) )

Proof

Step	Hyp	Ref	Expression
1		dflim4	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A. x e. A suc x e. A ) )
2		suceq	|- ( x = B -> suc x = suc B )
3	2	eleq1d	|- ( x = B -> ( suc x e. A <-> suc B e. A ) )
4	3	rspccv	|- ( A. x e. A suc x e. A -> ( B e. A -> suc B e. A ) )
5	4	3ad2ant3	|- ( ( Ord A /\ (/) e. A /\ A. x e. A suc x e. A ) -> ( B e. A -> suc B e. A ) )
6	1 5	sylbi	|- ( Lim A -> ( B e. A -> suc B e. A ) )
7		limord	|- ( Lim A -> Ord A )
8		ordtr	|- ( Ord A -> Tr A )
9		trsuc	|- ( ( Tr A /\ suc B e. A ) -> B e. A )
10	9	ex	|- ( Tr A -> ( suc B e. A -> B e. A ) )
11	7 8 10	3syl	|- ( Lim A -> ( suc B e. A -> B e. A ) )
12	6 11	impbid	|- ( Lim A -> ( B e. A <-> suc B e. A ) )