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

Metamath Proof Explorer

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