This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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