Theorem limsuc2

Description: Limit ordinals in the sense inclusive of zero contain all successors of their members. (Contributed by Stefan O'Rear, 20-Jan-2015)

	Ref	Expression
Assertion	limsuc2	|- ( ( Ord A /\ A = U. A ) -> ( B e. A <-> suc B e. A ) )

Proof

Step	Hyp	Ref	Expression
1		ordunisuc2	|- ( Ord A -> ( A = U. A <-> A. x e. A suc x e. A ) )
2	1	biimpa	|- ( ( Ord A /\ A = U. A ) -> A. x e. A suc x e. A )
3		suceq	|- ( x = B -> suc x = suc B )
4	3	eleq1d	|- ( x = B -> ( suc x e. A <-> suc B e. A ) )
5	4	rspccva	|- ( ( A. x e. A suc x e. A /\ B e. A ) -> suc B e. A )
6	2 5	sylan	|- ( ( ( Ord A /\ A = U. A ) /\ B e. A ) -> suc B e. A )
7	6	ex	|- ( ( Ord A /\ A = U. A ) -> ( B e. A -> suc B e. 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	8 10	syl	|- ( Ord A -> ( suc B e. A -> B e. A ) )
12	11	adantr	|- ( ( Ord A /\ A = U. A ) -> ( suc B e. A -> B e. A ) )
13	7 12	impbid	|- ( ( Ord A /\ A = U. A ) -> ( B e. A <-> suc B e. A ) )