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

Metamath Proof Explorer

Theorem limensuc

Description: A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003)

Ref Expression
Assertion limensuc 
|- ( ( A e. V /\ Lim A ) -> A ~~ suc A )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( A = if ( Lim A , A , On ) -> ( A e. V <-> if ( Lim A , A , On ) e. V ) )
2 id 
 |-  ( A = if ( Lim A , A , On ) -> A = if ( Lim A , A , On ) )
3 suceq 
 |-  ( A = if ( Lim A , A , On ) -> suc A = suc if ( Lim A , A , On ) )
4 2 3 breq12d 
 |-  ( A = if ( Lim A , A , On ) -> ( A ~~ suc A <-> if ( Lim A , A , On ) ~~ suc if ( Lim A , A , On ) ) )
5 1 4 imbi12d 
 |-  ( A = if ( Lim A , A , On ) -> ( ( A e. V -> A ~~ suc A ) <-> ( if ( Lim A , A , On ) e. V -> if ( Lim A , A , On ) ~~ suc if ( Lim A , A , On ) ) ) )
6 limeq 
 |-  ( A = if ( Lim A , A , On ) -> ( Lim A <-> Lim if ( Lim A , A , On ) ) )
7 limeq 
 |-  ( On = if ( Lim A , A , On ) -> ( Lim On <-> Lim if ( Lim A , A , On ) ) )
8 limon 
 |-  Lim On
9 6 7 8 elimhyp 
 |-  Lim if ( Lim A , A , On )
10 9 limensuci 
 |-  ( if ( Lim A , A , On ) e. V -> if ( Lim A , A , On ) ~~ suc if ( Lim A , A , On ) )
11 5 10 dedth 
 |-  ( Lim A -> ( A e. V -> A ~~ suc A ) )
12 11 impcom 
 |-  ( ( A e. V /\ Lim A ) -> A ~~ suc A )