Metamath Proof Explorer


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